Wed, 16 Nov 2005 17:45:29 +0100 wenzelm added betapplys;
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;
Wed, 16 Nov 2005 15:29:23 +0100 paulson new version of "tryres" allowing multiple unifiers (apparently needed for
Wed, 16 Nov 2005 14:05:41 +0100 wenzelm pgmlsymbolson: append Symbol.xsymbolsN at end!
Tue, 15 Nov 2005 14:08:32 +0100 wenzelm better no -d option;
Tue, 15 Nov 2005 10:11:52 +0100 haftmann added generic transformators
Mon, 14 Nov 2005 18:25:34 +0100 paulson removal of is_hol
Mon, 14 Nov 2005 16:26:40 +0100 haftmann added module system
Mon, 14 Nov 2005 15:23:33 +0100 haftmann added modules for code generator generation two, not operational yet
Mon, 14 Nov 2005 15:15:34 +0100 haftmann class_package - operational view on type classes
Mon, 14 Nov 2005 15:15:07 +0100 haftmann string_of_alist - convenient q'n'd printout function
Mon, 14 Nov 2005 15:14:59 +0100 wenzelm support for polyml-4.2.0;
Mon, 14 Nov 2005 15:14:32 +0100 haftmann new syntax for class_package
Mon, 14 Nov 2005 14:37:48 +0100 wenzelm added const_instance;
Mon, 14 Nov 2005 14:37:38 +0100 wenzelm added instance;
Mon, 14 Nov 2005 14:37:15 +0100 wenzelm added ML-Systems/polyml-4.1.4-patch.ML, ML-Systems/polyml-4.2.0.ML;
Mon, 14 Nov 2005 14:36:46 +0100 wenzelm Compatibility wrapper for Poly/ML 4.2.0.
Mon, 14 Nov 2005 14:36:29 +0100 wenzelm tuned;
Mon, 14 Nov 2005 13:59:58 +0100 urbanc added a few equivariance lemmas (they need to be automated
Sun, 13 Nov 2005 22:36:30 +0100 urbanc changed the HOL_basic_ss back and selectively added
Sun, 13 Nov 2005 20:33:36 +0100 urbanc exchanged HOL_ss for HOL_basic_ss in the simplification
Fri, 11 Nov 2005 10:50:43 +0100 chaieb a proof step corrected due to the changement in the presburger method.
Fri, 11 Nov 2005 10:49:59 +0100 chaieb old argument "abs" is replaced by "no_abs". Abstraction is turned on by default.
Fri, 11 Nov 2005 00:09:37 +0100 huffman add header
Thu, 10 Nov 2005 21:14:05 +0100 wenzelm tuned proofs;
Thu, 10 Nov 2005 20:57:22 +0100 wenzelm moved find_free to term.ML;
Thu, 10 Nov 2005 20:57:21 +0100 wenzelm guess: Seq.hd;
Thu, 10 Nov 2005 20:57:20 +0100 wenzelm guess: Toplevel.proof;
Thu, 10 Nov 2005 20:57:19 +0100 wenzelm added find_free (from Isar/proof_context.ML);
Thu, 10 Nov 2005 20:57:18 +0100 wenzelm curried multiply;
Thu, 10 Nov 2005 20:57:17 +0100 wenzelm induct method: fixes;
Thu, 10 Nov 2005 20:57:16 +0100 wenzelm uncurried Consts.typargs;
Thu, 10 Nov 2005 20:57:11 +0100 wenzelm renamed Thm.cgoal_of to Thm.cprem_of;
Thu, 10 Nov 2005 17:33:14 +0100 paulson duplicate axioms in ATP linkup, and general fixes
Thu, 10 Nov 2005 17:31:44 +0100 paulson tidying
Thu, 10 Nov 2005 00:36:26 +0100 urbanc called the induction principle "unsafe" instead of "test".
Wed, 09 Nov 2005 18:01:33 +0100 paulson Skolemization by inference, but not quite finished
Wed, 09 Nov 2005 16:26:55 +0100 wenzelm Explicit data structures for some Isar language elements.
Wed, 09 Nov 2005 16:26:54 +0100 wenzelm tuned;
Wed, 09 Nov 2005 16:26:53 +0100 wenzelm tvars_intr_list: natural argument order;
Wed, 09 Nov 2005 16:26:52 +0100 wenzelm moved datatype elem to element.ML;
Wed, 09 Nov 2005 16:26:51 +0100 wenzelm P.context_element, P.locale_element;
Wed, 09 Nov 2005 16:26:50 +0100 wenzelm Element.context;
Wed, 09 Nov 2005 16:26:49 +0100 wenzelm use existing exeption Empty;
Wed, 09 Nov 2005 16:26:48 +0100 wenzelm avoid code redundancy;
Wed, 09 Nov 2005 16:26:47 +0100 wenzelm tuned comments;
Wed, 09 Nov 2005 16:26:46 +0100 wenzelm removed obsolete term set operations;
Wed, 09 Nov 2005 16:26:45 +0100 wenzelm P.locale_element;
Wed, 09 Nov 2005 16:26:44 +0100 wenzelm added fold_terms;
Wed, 09 Nov 2005 16:26:43 +0100 wenzelm added Isar/element.ML;
Wed, 09 Nov 2005 16:26:41 +0100 wenzelm Thm.varifyT': natural argument order;
Wed, 09 Nov 2005 12:21:05 +0100 haftmann added join function
Tue, 08 Nov 2005 15:26:35 +0100 haftmann allowing indentation of 'theory' keyword
Tue, 08 Nov 2005 10:44:40 +0100 wenzelm simplified after_qed;
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip