src/HOL/ex/Predicate_Compile_ex.thy
Mon, 22 Mar 2010 08:30:13 +0100 bulwahn enabling a previously broken example of the predicate compiler again
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
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: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
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:11:06 +0100 bulwahn added another example to 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:30 +0100 bulwahn adopted predicate compiler examples to new syntax for modes
Thu, 12 Nov 2009 09:10:07 +0100 bulwahn adding more tests for the values command; adding some forbidden constants to inductify
Fri, 06 Nov 2009 08:11:58 +0100 bulwahn disabled upt example because of a problem due to overloaded constants with the predicate compiler
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 added further example of the values command
Fri, 06 Nov 2009 08:11:58 +0100 bulwahn improved handling of overloaded constants; examples with numerals
Fri, 06 Nov 2009 08:11:58 +0100 bulwahn adding tracing function for evaluated code; annotated compilation in the predicate compiler
Tue, 03 Nov 2009 10:36:20 +0100 bulwahn adding testcases for code inlining, sets and numerals to the example files of the predicate compiler and its quickcheck prototype; disabling length example
Fri, 30 Oct 2009 09:55:15 +0100 bulwahn renamed rpred to random
Wed, 28 Oct 2009 12:29:03 +0100 bulwahn improved mode parser; added mode annotations to examples
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
Tue, 27 Oct 2009 09:24:45 +0100 bulwahn disabled test case for predicate compiler due to an problem in the inductive package
Tue, 27 Oct 2009 09:03:56 +0100 bulwahn adding test case for inlining of predicate compiler
Tue, 27 Oct 2009 09:03:56 +0100 bulwahn changes to example file
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 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
Sat, 24 Oct 2009 16:55:42 +0200 bulwahn modularized the compilation in the predicate compiler
Sat, 24 Oct 2009 16:55:42 +0200 bulwahn 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
Sat, 24 Oct 2009 16:55:42 +0200 bulwahn cleaning the signature of the predicate compiler core; renaming signature and structures to uniform long names
Sat, 24 Oct 2009 16:55:42 +0200 bulwahn added skip_proof option; playing with compilation of depth-limited predicates
Sat, 24 Oct 2009 16:55:42 +0200 bulwahn reinvestigating the compilation of the random computation in the predicate compiler
Sat, 24 Oct 2009 16:55:42 +0200 bulwahn added option to generate random values to values command in the predicate compiler
Sat, 24 Oct 2009 16:55:42 +0200 bulwahn commented out the random generator compilation in the example file
Sat, 24 Oct 2009 16:55:42 +0200 bulwahn changed import_intros to handle parameters differently; changed handling of higher-order function compilation; reverted MicroJava change; tuned
Sat, 24 Oct 2009 16:55:42 +0200 bulwahn further cleaning up
Sat, 24 Oct 2009 16:55:42 +0200 bulwahn importing of polymorphic introduction rules with different schematic variable names
Sat, 24 Oct 2009 16:55:42 +0200 bulwahn continued cleaning up; moved tuple expanding to core
Sat, 24 Oct 2009 16:55:42 +0200 bulwahn cleaned up debugging messages; added options to code_pred command
Sat, 24 Oct 2009 16:55:42 +0200 bulwahn cleaned up
Sat, 24 Oct 2009 16:55:42 +0200 bulwahn added theory with alternative definitions for the predicate compiler; cleaned up examples
Sat, 24 Oct 2009 16:55:42 +0200 bulwahn higher-order arguments in different rules are fixed to one name in the predicate compiler
Sat, 24 Oct 2009 16:55:42 +0200 bulwahn changed importing introduction rules to fix the same type variables in all introduction rules; improved mode analysis for partially applied relations; added test case; tuned
Sat, 24 Oct 2009 16:55:42 +0200 bulwahn added further examples; added mode to code_pred command; tuned; some temporary things in Predicate_Compile_ex
Sat, 24 Oct 2009 16:55:42 +0200 bulwahn processing of tuples in introduction rules
Sat, 24 Oct 2009 16:55:42 +0200 bulwahn added a few tricky examples with tuples; added alternative introduction rules for some constants; corrected mode analysis with negation; improved fetching of definitions
Sat, 24 Oct 2009 16:55:42 +0200 bulwahn developing an executable the operator
Sat, 24 Oct 2009 16:55:42 +0200 bulwahn added test for higher-order function inductification; added debug messages
Sat, 24 Oct 2009 16:55:35 +0200 bulwahn added tupled versions of examples for the predicate compiler
Sat, 24 Oct 2009 16:54:32 +0200 bulwahn moved meta_fun_cong lemma into ML-file; tuned
Wed, 23 Sep 2009 16:20:13 +0200 bulwahn replaced sorry by oops; removed old debug functions in predicate compiler
Wed, 23 Sep 2009 16:20:13 +0200 bulwahn added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
Wed, 23 Sep 2009 16:20:12 +0200 bulwahn added a new example for the predicate compiler
Wed, 23 Sep 2009 16:20:12 +0200 bulwahn added context free grammar example; removed dead code; adapted to work without quick and dirty mode; fixed typo
Wed, 23 Sep 2009 16:20:12 +0200 bulwahn added first prototype of the extended predicate compiler
Wed, 23 Sep 2009 16:20:12 +0200 bulwahn extending predicate compiler and proof procedure to support tuples; testing predicate wirh HOL-MicroJava semantics
Tue, 15 Sep 2009 15:22:15 +0200 haftmann added singleton example
Thu, 27 Aug 2009 18:45:39 +0200 nipkow New example: IMP
Wed, 26 Aug 2009 16:13:19 +0200 nipkow new interval lemma
less more (0) -60 tip