| 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
|