src/Pure/thm.ML
Wed, 25 Nov 2009 09:13:46 +0100 haftmann normalized uncurry take/drop
Tue, 24 Nov 2009 17:28:25 +0100 haftmann curried take/drop
Sat, 21 Nov 2009 15:49:29 +0100 wenzelm explicitly mark some legacy freeze operations;
Mon, 16 Nov 2009 21:57:16 +0100 wenzelm generalized procs for rewrite_proof: allow skeleton;
Sun, 15 Nov 2009 15:14:28 +0100 wenzelm tuned;
Sun, 08 Nov 2009 18:43:42 +0100 wenzelm adapted Theory_Data;
Sun, 25 Oct 2009 13:04:06 +0100 wenzelm make SML/NJ happy;
Sat, 24 Oct 2009 20:54:08 +0200 wenzelm maintain explicit name space kind;
Sat, 24 Oct 2009 19:47:37 +0200 wenzelm renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
Sat, 24 Oct 2009 19:20:03 +0200 wenzelm eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
Wed, 21 Oct 2009 12:09:37 +0200 haftmann curried inter as canonical list operation (beware of argument order)
Wed, 21 Oct 2009 08:14:38 +0200 haftmann dropped redundant gen_ prefix
Tue, 20 Oct 2009 16:13:01 +0200 haftmann replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
Thu, 01 Oct 2009 14:27:50 +0200 wenzelm back to simple fold_body_thms and fulfill_proof/thm_proof (reverting a900d3cd47cc) -- the cycle check is implicit in the future computation of join_proofs;
Wed, 30 Sep 2009 22:20:58 +0200 wenzelm eliminated redundant bindings;
Mon, 28 Sep 2009 20:52:05 +0200 wenzelm fold_body_thms: pass pthm identifier;
Mon, 28 Sep 2009 12:09:55 +0200 wenzelm tuned internal source structure;
Wed, 16 Sep 2009 21:14:08 +0200 wenzelm replaced opaque signature matching by plain old abstype (again, cf. ac4498f95d1c) -- this recovers pretty printing in SML/NJ and Poly/ML 5.3;
Sun, 26 Jul 2009 13:12:53 +0200 wenzelm lambda/cabs/all: named variants;
Tue, 21 Jul 2009 20:37:32 +0200 wenzelm simultaneous join_proofs;
Tue, 21 Jul 2009 10:24:57 +0200 wenzelm prefer simultaneous join -- for improved scheduling;
Sun, 19 Jul 2009 18:42:05 +0200 wenzelm support for arbitrarity nested future proofs -- replaced crude order by explicit normalization (which might loop for bad dependencies);
Fri, 17 Jul 2009 23:11:40 +0200 wenzelm tuned/modernized Envir.subst_XXX;
Fri, 17 Jul 2009 21:33:00 +0200 wenzelm tuned/modernized Envir operations;
Thu, 16 Jul 2009 22:58:45 +0200 wenzelm tuned incr_indexes;
Thu, 09 Jul 2009 22:48:12 +0200 wenzelm renamed structure TermSubst to Term_Subst;
Mon, 06 Jul 2009 22:42:27 +0200 wenzelm clarified strip_shyps: proper type witnesses for present sorts;
Mon, 06 Jul 2009 21:24:30 +0200 wenzelm structure Thm: less pervasive names;
Mon, 06 Jul 2009 20:36:38 +0200 wenzelm clarified Thm.of_class/of_sort/class_triv;
Mon, 06 Jul 2009 19:58:52 +0200 wenzelm renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
less more (0) -300 -100 -50 -30 tip