| Tue, 31 Aug 2010 10:51:03 +0200 |
bulwahn |
renaming
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Thu, 26 Aug 2010 16:56:45 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 19 Aug 2010 12:11:57 +0200 |
haftmann |
use HOLogic.boolT and @{typ bool} more pervasively
|
file |
diff |
annotate
|
| Mon, 28 Jun 2010 15:03:07 +0200 |
haftmann |
merged constants "split" and "prod_case"
|
file |
diff |
annotate
|
| Wed, 26 May 2010 16:05:25 +0200 |
haftmann |
normalized references to constant "split"
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Wed, 21 Apr 2010 12:10:52 +0200 |
bulwahn |
replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Mon, 29 Mar 2010 17:30:55 +0200 |
bulwahn |
tuned
|
file |
diff |
annotate
|
| 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
|