Wed, 31 Jul 2002 16:10:24 +0200 | nipkow | added mk_left_commute to HOL.thy and used it "everywhere" | changeset | files |
Wed, 31 Jul 2002 14:40:40 +0200 | paulson | separate "axioms" proofs: more flexible for locale reasoning | changeset | files |
Wed, 31 Jul 2002 14:39:47 +0200 | paulson | tweaks involving Separation | changeset | files |
Wed, 31 Jul 2002 14:34:08 +0200 | paulson | new theorem eq_commute | changeset | files |
Tue, 30 Jul 2002 11:39:57 +0200 | paulson | better sats rules for higher-order operators | changeset | files |
Tue, 30 Jul 2002 11:38:33 +0200 | paulson | removal of twos_compl.ML, which is not really needed | changeset | files |