Wed, 16 Nov 2005 17:45:28 +0100 wenzelm tuned interfaces to support incremental match/unify (cf. versions in type.ML);
Wed, 16 Nov 2005 17:45:27 +0100 wenzelm tuned;
Wed, 16 Nov 2005 17:45:26 +0100 wenzelm norm_hhf: no normalization of protected props;
Wed, 16 Nov 2005 17:45:25 +0100 wenzelm added protect_cong, cong_mono_thm;
Wed, 16 Nov 2005 17:45:24 +0100 wenzelm induct: support local definitions to be passed through the induction;
Wed, 16 Nov 2005 17:45:23 +0100 wenzelm Trueprop: use ObjectLogic.judgment etc.;
Wed, 16 Nov 2005 17:45:22 +0100 wenzelm Term.betapply;
(0) -10000 -3000 -1000 -300 -100 -30 -10 -7 +7 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip