| Wed, 16 Nov 2005 19:34:19 +0100 | wenzelm | tuned document; | changeset | files |
| Wed, 16 Nov 2005 17:50:35 +0100 | wenzelm | tuned; | changeset | files |
| Wed, 16 Nov 2005 17:49:16 +0100 | wenzelm | improved induction proof: local defs/fixes; | changeset | files |
| Wed, 16 Nov 2005 17:45:36 +0100 | wenzelm | tuned Pattern.match/unify; | changeset | files |
| Wed, 16 Nov 2005 17:45:35 +0100 | wenzelm | added deskolem; | changeset | files |
| Wed, 16 Nov 2005 17:45:34 +0100 | wenzelm | added THEN_ALL_NEW_CASES; | changeset | files |
| Wed, 16 Nov 2005 17:45:33 +0100 | wenzelm | added revert_skolem, mk_def, add_def; | changeset | files |
| Wed, 16 Nov 2005 17:45:32 +0100 | wenzelm | ProofContext.mk_def; | changeset | files |
| Wed, 16 Nov 2005 17:45:31 +0100 | wenzelm | Term.betapplys; | changeset | files |
| Wed, 16 Nov 2005 17:45:30 +0100 | wenzelm | tuned Pattern.match/unify; | changeset | files |
| Wed, 16 Nov 2005 17:45:29 +0100 | wenzelm | added betapplys; | changeset | files |
| Wed, 16 Nov 2005 17:45:28 +0100 | wenzelm | tuned interfaces to support incremental match/unify (cf. versions in type.ML); | changeset | files |