Hi, Recently I found that, GENL and Q.GENL has different generalization orders:
> GENL [``x``, ``y``, ``z``] (SPEC_ALL EQ_TRANS); val it = |- ∀x y z. (x = y) ∧ (y = z) ⇒ (x = z): thm > Q.GENL [`x`, `y`, `z`] (SPEC_ALL EQ_TRANS); val it = |- ∀z y x. (x = y) ∧ (y = z) ⇒ (x = z): thm see the differences: “!x y z” and “!z y x”. It seems that Q.GENL processes the variable list in a reverted order. But SPECL and Q.SPECL has no such differences when specializing a list of variables: > SPECL [``a``, ``b``, ``c``] EQ_TRANS; val it = |- (a = b) ∧ (b = c) ⇒ (a = c): thm > Q.SPECL [`a`, `b`, `c`] EQ_TRANS; val it = |- (a = b) ∧ (b = c) ⇒ (a = c): thm Q.GENL is not documented currently. But is the behavior desired or not? Regards, Chun Tian
signature.asc
Description: Message signed with OpenPGP using GPGMail
------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
