| Wed, 23 Sep 2009 16:20:12 +0200 |
bulwahn |
adapted configuration for DatatypeCase.make_case
|
changeset |
files
|
| Wed, 23 Sep 2009 16:20:12 +0200 |
bulwahn |
added a new example for the predicate compiler
|
changeset |
files
|
| 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
|
changeset |
files
|
| Wed, 23 Sep 2009 16:20:12 +0200 |
bulwahn |
added first prototype of the extended predicate compiler
|
changeset |
files
|
| Wed, 23 Sep 2009 16:20:12 +0200 |
bulwahn |
moved predicate compiler to Tools
|
changeset |
files
|
| Wed, 23 Sep 2009 16:20:12 +0200 |
bulwahn |
removed generation of strange tuple modes in predicate compiler
|
changeset |
files
|
| Wed, 23 Sep 2009 16:20:12 +0200 |
bulwahn |
extending predicate compiler and proof procedure to support tuples; testing predicate wirh HOL-MicroJava semantics
|
changeset |
files
|
| Wed, 23 Sep 2009 16:20:12 +0200 |
bulwahn |
modified predicate compiler further to support tuples
|
changeset |
files
|
| Wed, 23 Sep 2009 16:20:12 +0200 |
bulwahn |
changed preprocessing due to problems with LightweightJava; added transfer of thereoms; changed the type of mode to support tuples in the predicate compiler
|
changeset |
files
|
| Wed, 23 Sep 2009 16:20:12 +0200 |
bulwahn |
handling of definitions
|
changeset |
files
|
| Wed, 23 Sep 2009 16:20:12 +0200 |
bulwahn |
experimenting to add some useful interface for definitions
|
changeset |
files
|
| Wed, 23 Sep 2009 16:20:12 +0200 |
bulwahn |
added predicate compile preprocessing structure for definitional thms -- probably is replaced by hooking the theorem command differently
|
changeset |
files
|
| Wed, 23 Sep 2009 16:20:12 +0200 |
bulwahn |
modified handling of side conditions in proof procedure of predicate compiler
|
changeset |
files
|
| Wed, 23 Sep 2009 15:25:25 +0200 |
haftmann |
merged
|
changeset |
files
|
| Wed, 23 Sep 2009 14:00:12 +0200 |
haftmann |
Code_Eval(uation)
|
changeset |
files
|
| Wed, 23 Sep 2009 13:48:16 +0200 |
blanchet |
merged
|
changeset |
files
|
| Wed, 23 Sep 2009 13:47:08 +0200 |
blanchet |
Added "nitpick_const_simp" tags to lazy list theories.
|
changeset |
files
|
| Wed, 23 Sep 2009 13:48:35 +0200 |
krauss |
atbroy101 is long dead, use atbroy99; comment out broken SML test invocation
|
changeset |
files
|
| Wed, 23 Sep 2009 13:42:53 +0200 |
haftmann |
merged
|
changeset |
files
|
| Wed, 23 Sep 2009 12:03:47 +0200 |
haftmann |
stripped legacy ML bindings
|
changeset |
files
|
| Wed, 23 Sep 2009 13:31:38 +0200 |
hoelzl |
Undo errornous commit of Statespace change
|
changeset |
files
|
| Wed, 23 Sep 2009 13:17:17 +0200 |
hoelzl |
correct variable order in approximate-method
|
changeset |
files
|
| Wed, 23 Sep 2009 11:06:32 +0100 |
paulson |
merged
|
changeset |
files
|
| Wed, 23 Sep 2009 11:05:28 +0100 |
paulson |
Correct chasing of type variable instantiations during type unification.
|
changeset |
files
|