src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
Mon, 04 Nov 2013 17:25:36 +0100 blanchet careful with lists of different lengths
Thu, 31 Oct 2013 16:54:22 +0100 blanchet generate stable names for axioms
Fri, 24 May 2013 17:00:46 +0200 wenzelm tuned signature;
Thu, 28 Feb 2013 18:35:31 +0100 wenzelm provide explicit dummy names (cf. dfe469293eb4);
Mon, 12 Nov 2012 23:24:40 +0100 haftmann dropped dead code
Wed, 12 Sep 2012 13:56:49 +0200 wenzelm standardized ML aliases;
Sat, 14 Jan 2012 21:16:15 +0100 wenzelm discontinued old-style Term.list_abs in favour of plain Term.abs;
Thu, 09 Jun 2011 17:51:49 +0200 wenzelm simplified Name.variant -- discontinued builtin fold_map;
Thu, 09 Jun 2011 16:34:49 +0200 wenzelm discontinued Name.variant to emphasize that this is old-style / indirect;
Sun, 15 May 2011 18:59:27 +0200 wenzelm eliminated obsolete "assert" function, including divergent (unused!?) clone in Predicate_Compile_Proof;
Sat, 16 Apr 2011 16:15:37 +0200 wenzelm modernized structure Proof_Context;
Wed, 01 Dec 2010 15:02:39 +0100 wenzelm tuned;
Thu, 21 Oct 2010 19:13:10 +0200 bulwahn using a signature in core_data and moving some more functions to core_data
Thu, 30 Sep 2010 15:37:11 +0200 bulwahn applying case beta reduction to case term before matching in predicate compile function flattening; moving case beta reduction function to Predicate_Compile_Aux
Thu, 30 Sep 2010 10:48:09 +0200 bulwahn removing dead code
Wed, 29 Sep 2010 11:55:08 +0200 bulwahn removing obsolete distinction between prod_case and other case expressions after merging of split and prod_case (d3daea901123) in predicate compiler
Tue, 31 Aug 2010 10:51:03 +0200 bulwahn renaming
Tue, 31 Aug 2010 08:00:56 +0200 bulwahn changing order of premises generated when flattening functions in premises; adapting example for second attack for hotel key card system
Thu, 26 Aug 2010 16:56:45 +0200 wenzelm tuned;
Thu, 19 Aug 2010 12:11:57 +0200 haftmann use HOLogic.boolT and @{typ bool} more pervasively
Mon, 28 Jun 2010 15:03:07 +0200 haftmann merged constants "split" and "prod_case"
Wed, 26 May 2010 16:05:25 +0200 haftmann normalized references to constant "split"
Mon, 03 May 2010 14:25:56 +0200 wenzelm renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
Wed, 21 Apr 2010 12:10:52 +0200 bulwahn replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
Wed, 31 Mar 2010 16:44:41 +0200 bulwahn improving lookup function to handle overloaded constants more correctly in the function flattening of the predicate compiler
Mon, 29 Mar 2010 17:30:55 +0200 bulwahn tuned
Mon, 29 Mar 2010 17:30:53 +0200 bulwahn adding registration of functions in the function flattening
Mon, 29 Mar 2010 17:30:48 +0200 bulwahn removing fishing for split thm in the predicate compiler
Mon, 22 Mar 2010 08:30:13 +0100 bulwahn cleaning the function flattening
Mon, 22 Mar 2010 08:30:13 +0100 bulwahn generalized split transformation in the function flattening
Mon, 22 Mar 2010 08:30:12 +0100 bulwahn only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
Mon, 22 Mar 2010 08:30:12 +0100 bulwahn restructuring function flattening
Mon, 22 Mar 2010 08:30:12 +0100 bulwahn renaming mk_prems to flatten in the function flattening
Mon, 22 Mar 2010 08:30:12 +0100 bulwahn simplifying function flattening
Sat, 20 Mar 2010 17:33:11 +0100 wenzelm renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
Mon, 01 Mar 2010 09:47:44 +0100 bulwahn made smlnj happy
Tue, 23 Feb 2010 13:36:15 +0100 bulwahn adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
Sun, 07 Feb 2010 19:33:34 +0100 wenzelm renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
Thu, 21 Jan 2010 12:18:41 +0100 bulwahn adopting predicate compiler to new Spec_Rules and eliminating the use of Nitpick_Simps
Wed, 20 Jan 2010 11:56:45 +0100 bulwahn refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
Thu, 19 Nov 2009 08:25:47 +0100 bulwahn adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
Tue, 17 Nov 2009 14:51:57 +0100 wenzelm eliminated slightly odd name space grouping -- now managed by Isar toplevel;
Fri, 13 Nov 2009 19:57:46 +0100 wenzelm inductive: eliminated obsolete kind;
Thu, 12 Nov 2009 22:02:11 +0100 wenzelm eliminated obsolete "internal" kind -- collapsed to unspecific "";
Thu, 12 Nov 2009 09:11:46 +0100 bulwahn removed unnecessary oracle in the predicate compiler
Sun, 08 Nov 2009 18:43:42 +0100 wenzelm adapted Theory_Data;
Wed, 28 Oct 2009 16:25:27 +0100 wenzelm conceal internal bindings;
Wed, 28 Oct 2009 00:07:51 +0100 wenzelm proper headers;
Tue, 27 Oct 2009 09:02:22 +0100 bulwahn including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
less more (0) tip