Wed, 16 Nov 2005 17:45:28 +0100 | wenzelm | tuned interfaces to support incremental match/unify (cf. versions in type.ML); | changeset | files |
Wed, 16 Nov 2005 17:45:27 +0100 | wenzelm | tuned; | changeset | files |
Wed, 16 Nov 2005 17:45:26 +0100 | wenzelm | norm_hhf: no normalization of protected props; | changeset | files |
Wed, 16 Nov 2005 17:45:25 +0100 | wenzelm | added protect_cong, cong_mono_thm; | changeset | files |
Wed, 16 Nov 2005 17:45:24 +0100 | wenzelm | induct: support local definitions to be passed through the induction; | changeset | files |
Wed, 16 Nov 2005 17:45:23 +0100 | wenzelm | Trueprop: use ObjectLogic.judgment etc.; | changeset | files |
Wed, 16 Nov 2005 17:45:22 +0100 | wenzelm | Term.betapply; | changeset | files |