| Sat, 07 Jan 2006 11:36:58 +0100 | urbanc | changed PRO_RED proof to conform with the new induction rules | changeset | files |
| Fri, 06 Jan 2006 18:18:16 +0100 | wenzelm | prep_meta_eq: reuse mk_rews of local simpset; | changeset | files |
| Fri, 06 Jan 2006 18:18:15 +0100 | wenzelm | removed obsolete eqrule_HOL_data.ML; | changeset | files |
| Fri, 06 Jan 2006 18:18:14 +0100 | wenzelm | removed obsolete eqrule_FOL_data.ML; | changeset | files |
| Fri, 06 Jan 2006 18:18:13 +0100 | wenzelm | simplified EqSubst setup; | changeset | files |
| Fri, 06 Jan 2006 18:18:12 +0100 | wenzelm | obsolete, reuse mk_rews of local simpset; | changeset | files |
| Fri, 06 Jan 2006 15:18:22 +0100 | wenzelm | Toplevel.theory_to_proof; | changeset | files |
| Fri, 06 Jan 2006 15:18:21 +0100 | wenzelm | transactions now always see quasi-functional intermediate checkpoint; | changeset | files |