src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
2010-01-22 haftmann 2010-01-22 HOLogic.strip_psplits: types are ordered after syntactic appearance, not after corresponding de-Bruin index (closer correspondence to similar strip operations)
2010-01-20 bulwahn 2010-01-20 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
2009-12-07 haftmann 2009-12-07 split off evaluation mechanisms in separte module Code_Eval
2009-11-30 haftmann 2009-11-30 modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
2009-11-19 bulwahn 2009-11-19 adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
2009-11-19 bulwahn 2009-11-19 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
2009-11-19 bulwahn 2009-11-19 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
2009-11-13 wenzelm 2009-11-13 modernized structure Local_Theory;
2009-11-12 bulwahn 2009-11-12 removed annoying tracing message
2009-11-12 bulwahn 2009-11-12 improving code quality thanks to Florian's code review
2009-11-12 bulwahn 2009-11-12 renaming code_pred_intros to code_pred_intro * * * adopted alternative definitions for the predicate compiler to new attribute name
2009-11-12 bulwahn 2009-11-12 new names for predicate functions in the predicate compiler * * * adopting examples of the predicate compiler
2009-11-12 bulwahn 2009-11-12 changed modes to expected_modes; added UNION to code_pred_inlining; fixed some examples; tuned
2009-11-12 bulwahn 2009-11-12 added interface of user proposals for names of generated constants
2009-11-12 bulwahn 2009-11-12 first steps towards a new mode datastructure; new syntax for mode annotations and new output of modes
2009-11-08 berghofe 2009-11-08 merged
2009-11-08 berghofe 2009-11-08 Repaired handling of comprehensions in "values" command.
2009-11-08 wenzelm 2009-11-08 adapted Theory_Data; tuned;
2009-11-08 wenzelm 2009-11-08 adapted Generic_Data, Proof_Data; tuned;
2009-11-06 bulwahn 2009-11-06 merged
2009-11-06 bulwahn 2009-11-06 made definition of functions generically for the different instances
2009-11-06 bulwahn 2009-11-06 renamed generator to random_function in the predicate compiler
2009-11-06 bulwahn 2009-11-06 improved handling of already defined functions in the predicate compiler; could cause trouble before when no modes for a predicate were infered
2009-11-06 bulwahn 2009-11-06 strictly respecting the line margin in the predicate compiler core
2009-11-06 bulwahn 2009-11-06 added optional mode annotations for parameters in the values command
2009-11-06 bulwahn 2009-11-06 moved values command from core to predicate compile
2009-11-06 bulwahn 2009-11-06 Adopted output of values command
2009-11-06 bulwahn 2009-11-06 made SML/NJ happy; tuned
2009-11-06 bulwahn 2009-11-06 adding tracing function for evaluated code; annotated compilation in the predicate compiler
2009-11-05 wenzelm 2009-11-05 eliminated funny record patterns and made SML/NJ happy;
2009-11-02 bulwahn 2009-11-02 merged
2009-10-31 bulwahn 2009-10-31 predicate compiler creates code equations for predicates with full mode
2009-10-30 bulwahn 2009-10-30 renamed rpred to random
2009-11-01 wenzelm 2009-11-01 modernized structure Rule_Cases;
2009-10-29 wenzelm 2009-10-29 merged
2009-10-29 bulwahn 2009-10-29 encapsulating records with datatype constructors and adding type annotations to make SML/NJ happy
2009-10-28 bulwahn 2009-10-28 moved datatype mode and string functions to the auxillary structure
2009-10-28 bulwahn 2009-10-28 improving mode parsing in the predicate compiler
2009-10-28 bulwahn 2009-10-28 improved handling of alternative rules; added test cases for alternative rules; normalized tracing in the predicate compiler
2009-10-29 wenzelm 2009-10-29 standardized filter/filter_out;
2009-10-28 wenzelm 2009-10-28 eliminated hard tabulators, guessing at each author's individual tab-width;
2009-10-28 wenzelm 2009-10-28 proper headers;
2009-10-27 bulwahn 2009-10-27 adding a prototype of a counter-example generator based on the predicate compiler to HOL/ex
2009-10-27 bulwahn 2009-10-27 added option show_modes to predicate compiler
2009-10-27 bulwahn 2009-10-27 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
2009-10-24 bulwahn 2009-10-24 further changes due to the previous merge in the predicate compiler
2009-10-24 wenzelm 2009-10-24 merge -- imported from bulwahn d759e2728188;
2009-10-24 bulwahn 2009-10-24 removed tuple functions from the predicate compiler
2009-10-24 bulwahn 2009-10-24 improving the compilation with higher-order arguments in the predicate compiler
2009-10-24 bulwahn 2009-10-24 now the predicate compilere handles the predicate without introduction rules better as before
2009-10-24 bulwahn 2009-10-24 removed dead code; added examples
2009-10-24 bulwahn 2009-10-24 removed obsolete GeneratorPrem; clean-up after modularization; tuned
2009-10-24 bulwahn 2009-10-24 modularized the compilation in the predicate compiler
2009-10-24 bulwahn 2009-10-24 modifying the depth-limited compilation to be sound, but now throws an error undefined in case of hitting the depth limit in an negative context; cleaning up the examples
2009-10-24 bulwahn 2009-10-24 cleaning the signature of the predicate compiler core; renaming signature and structures to uniform long names
2009-10-24 bulwahn 2009-10-24 added skip_proof option; playing with compilation of depth-limited predicates
2009-10-24 bulwahn 2009-10-24 reinvestigating the compilation of the random computation in the predicate compiler
2009-10-24 bulwahn 2009-10-24 added option to generate random values to values command in the predicate compiler
2009-10-24 bulwahn 2009-10-24 added option to execute depth-limited computations for the values command in the predicate compiler
2009-10-24 bulwahn 2009-10-24 renamed functions from sizelim to more natural name depth_limited for compilation of depth-limited search in the predicate compiler