| Sun, 29 Jul 2007 14:30:00 +0200 | wenzelm | avoid ill-defined Simp_tac; | changeset | files |
| Sun, 29 Jul 2007 14:29:59 +0200 | wenzelm | marked some CRITICAL sections; | changeset | files |
| Sun, 29 Jul 2007 14:29:58 +0200 | wenzelm | simplified ResAtpset via NamedThmsFun; | changeset | files |
| Sun, 29 Jul 2007 14:29:57 +0200 | wenzelm | metis_tac: proper context (ProofContext.init it *not* sufficient); | changeset | files |
| Sun, 29 Jul 2007 14:29:56 +0200 | wenzelm | proper simproc_setup for "neq", "let_simp"; | changeset | files |
| Sun, 29 Jul 2007 14:29:54 +0200 | wenzelm | renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms; | changeset | files |
| Sun, 29 Jul 2007 14:29:52 +0200 | wenzelm | replaced make_imp by rev_mp; | changeset | files |
| Sun, 29 Jul 2007 14:29:51 +0200 | wenzelm | proper simproc_setup for "list_neq"; | changeset | files |