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;
Tue, 08 Nov 2005 10:43:15 +0100 wenzelm avoid prove_plain, export_plain, simplified after_qed;
Tue, 08 Nov 2005 10:43:13 +0100 wenzelm removed export_plain;
Tue, 08 Nov 2005 10:43:12 +0100 wenzelm renamed assert_prop to ensure_prop;
Tue, 08 Nov 2005 10:43:11 +0100 wenzelm renamed goals.ML to old_goals.ML;
Tue, 08 Nov 2005 10:43:10 +0100 wenzelm export compose_hhf;
Tue, 08 Nov 2005 10:43:09 +0100 wenzelm removed impose_hyps, satisfy_hyps;
Tue, 08 Nov 2005 10:43:08 +0100 wenzelm const args: do not store variable names (unused);
Tue, 08 Nov 2005 10:43:05 +0100 wenzelm renamed goals.ML to old_goals.ML;
Tue, 08 Nov 2005 09:13:22 +0100 haftmann (fix for accidental commit)
Tue, 08 Nov 2005 09:12:02 +0100 haftmann (codegen)
Tue, 08 Nov 2005 02:19:11 +0100 huffman generate pattern combinators for new datatypes
Mon, 07 Nov 2005 23:33:01 +0100 huffman reimplemented Case syntax using print/parse translations; moved as-patterns to separate section
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip