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
Mon, 07 Nov 2005 23:30:49 +0100 huffman add case syntax for type one
Mon, 07 Nov 2005 19:23:53 +0100 huffman remove syntax for as-patterns
Mon, 07 Nov 2005 19:03:02 +0100 wenzelm avoid 'as' as identifier;
Mon, 07 Nov 2005 18:50:53 +0100 wenzelm avoid 'as' as identifier;
Mon, 07 Nov 2005 18:32:54 +0100 berghofe Added strong induction theorem (currently only axiomatized!).
Mon, 07 Nov 2005 15:19:03 +0100 urbanc Initial commit.
Mon, 07 Nov 2005 15:12:13 +0100 urbanc Initial commit of the theory "Weakening".
Mon, 07 Nov 2005 14:35:25 +0100 urbanc added thms perm, distinct and fresh to the simplifier.
Mon, 07 Nov 2005 12:06:11 +0100 haftmann added proper fillin_mixfix
Mon, 07 Nov 2005 11:39:24 +0100 haftmann added fillin_mixfix, replace_quote
Mon, 07 Nov 2005 11:28:34 +0100 berghofe New function store_thmss_atts.
Mon, 07 Nov 2005 11:17:45 +0100 urbanc used the function Library.product for the cprod from Stefan
Mon, 07 Nov 2005 10:47:25 +0100 urbanc fixed bug with nominal induct
Mon, 07 Nov 2005 09:34:51 +0100 haftmann added fillin_mixfix' needed by serializer
Sun, 06 Nov 2005 01:21:37 +0100 huffman add case syntax stuff
Sun, 06 Nov 2005 00:35:24 +0100 huffman use consts for infix syntax
Sun, 06 Nov 2005 00:22:03 +0100 huffman add proof of Bekic's theorem: fix_cprod
Sat, 05 Nov 2005 21:56:45 +0100 huffman simplify definitions
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip