| Mon, 29 Mar 2010 17:30:53 +0200 |
bulwahn |
adding registration of functions in the function flattening
|
file |
diff |
annotate
|
| Mon, 29 Mar 2010 17:30:48 +0200 |
bulwahn |
removing fishing for split thm in the predicate compiler
|
file |
diff |
annotate
|
| Mon, 22 Mar 2010 08:30:13 +0100 |
bulwahn |
cleaning the function flattening
|
file |
diff |
annotate
|
| Mon, 22 Mar 2010 08:30:13 +0100 |
bulwahn |
generalized split transformation in the function flattening
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Mon, 22 Mar 2010 08:30:12 +0100 |
bulwahn |
restructuring function flattening
|
file |
diff |
annotate
|
| Mon, 22 Mar 2010 08:30:12 +0100 |
bulwahn |
renaming mk_prems to flatten in the function flattening
|
file |
diff |
annotate
|
| Mon, 22 Mar 2010 08:30:12 +0100 |
bulwahn |
simplifying function flattening
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Mon, 01 Mar 2010 09:47:44 +0100 |
bulwahn |
made smlnj happy
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Thu, 21 Jan 2010 12:18:41 +0100 |
bulwahn |
adopting predicate compiler to new Spec_Rules and eliminating the use of Nitpick_Simps
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Thu, 19 Nov 2009 08:25:47 +0100 |
bulwahn |
adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
|
file |
diff |
annotate
|
| Tue, 17 Nov 2009 14:51:57 +0100 |
wenzelm |
eliminated slightly odd name space grouping -- now managed by Isar toplevel;
|
file |
diff |
annotate
|
| Fri, 13 Nov 2009 19:57:46 +0100 |
wenzelm |
inductive: eliminated obsolete kind;
|
file |
diff |
annotate
|
| Thu, 12 Nov 2009 22:02:11 +0100 |
wenzelm |
eliminated obsolete "internal" kind -- collapsed to unspecific "";
|
file |
diff |
annotate
|
| Thu, 12 Nov 2009 09:11:46 +0100 |
bulwahn |
removed unnecessary oracle in the predicate compiler
|
file |
diff |
annotate
|
| Sun, 08 Nov 2009 18:43:42 +0100 |
wenzelm |
adapted Theory_Data;
|
file |
diff |
annotate
|
| Wed, 28 Oct 2009 16:25:27 +0100 |
wenzelm |
conceal internal bindings;
|
file |
diff |
annotate
|
| Wed, 28 Oct 2009 00:07:51 +0100 |
wenzelm |
proper headers;
|
file |
diff |
annotate
|
| Tue, 27 Oct 2009 09:02:22 +0100 |
bulwahn |
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
|
file |
diff |
annotate
|