| Thu, 19 Aug 2010 11:02:14 +0200 |
haftmann |
use antiquotations for remaining unqualified constants in HOL
|
file |
diff |
annotate
|
| Wed, 21 Jul 2010 18:11:51 +0200 |
bulwahn |
putting proof in the right context; adding if rewriting; tuned
|
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
|
| 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 19:29:11 +0100 |
wenzelm |
eliminated old-style Drule.add_axiom in favour of Specification.axiom, with explicit Drule.export_without_context to imitate the old behaviour;
|
file |
diff |
annotate
|
| Mon, 22 Mar 2010 08:30:13 +0100 |
bulwahn |
improving handling of case expressions in predicate rewriting
|
file |
diff |
annotate
|
| Mon, 22 Mar 2010 00:48:56 +0100 |
wenzelm |
replaced PureThy.add_axioms by more basic Drule.add_axiom, which is old-style nonetheless;
|
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
|
| 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, 05 Nov 2009 16:10:49 +0100 |
wenzelm |
eliminated funny record patterns and made SML/NJ happy;
|
file |
diff |
annotate
|
| Tue, 03 Nov 2009 10:24:05 +0100 |
bulwahn |
recursively replacing abstractions by new definitions in the predicate compiler
|
file |
diff |
annotate
|
| Fri, 30 Oct 2009 09:55:15 +0100 |
bulwahn |
renamed rpred to random
|
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
|