src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
Mon, 22 Mar 2010 08:30:13 +0100 bulwahn reviving the classical depth-limited computation in the predicate compiler
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
Sat, 27 Feb 2010 20:57:08 +0100 wenzelm clarified @{const_name} vs. @{const_abbrev};
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
Fri, 19 Feb 2010 14:47:01 +0100 haftmann moved remaning class operations from Algebras.thy to Groups.thy
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, 28 Jan 2010 11:48:49 +0100 haftmann new theory Algebras.thy for generic algebraic structures
Fri, 22 Jan 2010 16:59:21 +0100 haftmann merged
Fri, 22 Jan 2010 16:56:51 +0100 haftmann HOLogic.strip_psplits: types are ordered after syntactic appearance, not after corresponding de-Bruin index (closer correspondence to similar strip operations)
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
Mon, 07 Dec 2009 16:27:48 +0100 haftmann split off evaluation mechanisms in separte module Code_Eval
Mon, 30 Nov 2009 11:42:49 +0100 haftmann modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
Thu, 19 Nov 2009 08:25:53 +0100 bulwahn adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
Thu, 19 Nov 2009 08:25:51 +0100 bulwahn changing the proof procedure for parameters; adding a testcase for negation and parameters; adopting print_tac to the latest function print_tac' in the predicate compiler
Thu, 19 Nov 2009 08:25:47 +0100 bulwahn adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
Fri, 13 Nov 2009 21:11:15 +0100 wenzelm modernized structure Local_Theory;
Thu, 12 Nov 2009 20:38:59 +0100 bulwahn removed annoying tracing message
Thu, 12 Nov 2009 09:11:41 +0100 bulwahn improving code quality thanks to Florian's code review
Thu, 12 Nov 2009 09:11:36 +0100 bulwahn renaming code_pred_intros to code_pred_intro
Thu, 12 Nov 2009 09:11:26 +0100 bulwahn new names for predicate functions in the predicate compiler
Thu, 12 Nov 2009 09:10:42 +0100 bulwahn changed modes to expected_modes; added UNION to code_pred_inlining; fixed some examples; tuned
Thu, 12 Nov 2009 09:10:22 +0100 bulwahn added interface of user proposals for names of generated constants
Thu, 12 Nov 2009 09:10:16 +0100 bulwahn first steps towards a new mode datastructure; new syntax for mode annotations and new output of modes
Sun, 08 Nov 2009 20:50:31 +0100 berghofe merged
Sun, 08 Nov 2009 15:45:09 +0100 berghofe Repaired handling of comprehensions in "values" command.
Sun, 08 Nov 2009 18:43:42 +0100 wenzelm adapted Theory_Data;
Sun, 08 Nov 2009 16:30:41 +0100 wenzelm adapted Generic_Data, Proof_Data;
Fri, 06 Nov 2009 08:47:32 +0100 bulwahn merged
Fri, 06 Nov 2009 08:11:58 +0100 bulwahn made definition of functions generically for the different instances
Fri, 06 Nov 2009 08:11:58 +0100 bulwahn renamed generator to random_function in the predicate compiler
Fri, 06 Nov 2009 08:11:58 +0100 bulwahn improved handling of already defined functions in the predicate compiler; could cause trouble before when no modes for a predicate were infered
Fri, 06 Nov 2009 08:11:58 +0100 bulwahn strictly respecting the line margin in the predicate compiler core
Fri, 06 Nov 2009 08:11:58 +0100 bulwahn added optional mode annotations for parameters in the values command
Fri, 06 Nov 2009 08:11:58 +0100 bulwahn moved values command from core to predicate compile
Fri, 06 Nov 2009 08:11:58 +0100 bulwahn Adopted output of values command
Fri, 06 Nov 2009 08:11:58 +0100 bulwahn made SML/NJ happy; tuned
Fri, 06 Nov 2009 08:11:58 +0100 bulwahn adding tracing function for evaluated code; annotated compilation in the predicate compiler
Thu, 05 Nov 2009 16:10:49 +0100 wenzelm eliminated funny record patterns and made SML/NJ happy;
Mon, 02 Nov 2009 09:01:18 +0100 bulwahn merged
Sat, 31 Oct 2009 10:02:37 +0100 bulwahn predicate compiler creates code equations for predicates with full mode
Fri, 30 Oct 2009 09:55:15 +0100 bulwahn renamed rpred to random
Sun, 01 Nov 2009 15:24:45 +0100 wenzelm modernized structure Rule_Cases;
Thu, 29 Oct 2009 18:17:26 +0100 wenzelm merged
Thu, 29 Oct 2009 13:59:37 +0100 bulwahn encapsulating records with datatype constructors and adding type annotations to make SML/NJ happy
Wed, 28 Oct 2009 12:29:02 +0100 bulwahn moved datatype mode and string functions to the auxillary structure
Wed, 28 Oct 2009 12:29:01 +0100 bulwahn improving mode parsing in the predicate compiler
Wed, 28 Oct 2009 12:29:00 +0100 bulwahn improved handling of alternative rules; added test cases for alternative rules; normalized tracing in the predicate compiler
Thu, 29 Oct 2009 17:58:26 +0100 wenzelm standardized filter/filter_out;
Wed, 28 Oct 2009 00:24:38 +0100 wenzelm eliminated hard tabulators, guessing at each author's individual tab-width;
Wed, 28 Oct 2009 00:07:51 +0100 wenzelm proper headers;
Tue, 27 Oct 2009 09:03:56 +0100 bulwahn adding a prototype of a counter-example generator based on the predicate compiler to HOL/ex
Tue, 27 Oct 2009 09:03:56 +0100 bulwahn added option show_modes to predicate compiler
Tue, 27 Oct 2009 09:02:22 +0100 bulwahn including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
Sat, 24 Oct 2009 20:27:26 +0200 bulwahn further changes due to the previous merge in the predicate compiler
Sat, 24 Oct 2009 23:57:42 +0200 wenzelm merge -- imported from bulwahn d759e2728188;
Sat, 24 Oct 2009 16:55:43 +0200 bulwahn removed tuple functions from the predicate compiler
Sat, 24 Oct 2009 16:55:43 +0200 bulwahn improving the compilation with higher-order arguments in the predicate compiler
Sat, 24 Oct 2009 16:55:43 +0200 bulwahn now the predicate compilere handles the predicate without introduction rules better as before
Sat, 24 Oct 2009 16:55:43 +0200 bulwahn removed dead code; added examples
less more (0) -100 -60 tip