Thu, 10 Sep 1998 18:06:39 +0200 |
paulson |
well-formed asym rules; also adds less_irrefl, le_refl since order_refl
|
changeset |
files
|
Thu, 10 Sep 1998 17:50:06 +0200 |
paulson |
added proof of final result...
|
changeset |
files
|
Thu, 10 Sep 1998 17:49:36 +0200 |
paulson |
tidied
|
changeset |
files
|
Thu, 10 Sep 1998 17:49:14 +0200 |
paulson |
Now WO1_WO7 has a .thy file
|
changeset |
files
|
Thu, 10 Sep 1998 17:42:44 +0200 |
paulson |
eliminated equals0E
|
changeset |
files
|
Thu, 10 Sep 1998 17:42:02 +0200 |
paulson |
fixed PROOF FAILED
|
changeset |
files
|
Thu, 10 Sep 1998 17:40:03 +0200 |
paulson |
tidied
|
changeset |
files
|
Thu, 10 Sep 1998 17:38:36 +0200 |
paulson |
deleted the bogus equals0E, fixed equals0D
|
changeset |
files
|
Thu, 10 Sep 1998 17:36:42 +0200 |
paulson |
eliminated equals0E
|
changeset |
files
|
Thu, 10 Sep 1998 17:34:43 +0200 |
paulson |
well-formed asym rules
|
changeset |
files
|
Thu, 10 Sep 1998 17:34:01 +0200 |
paulson |
new file AC/WO1_WO7.thy
|
changeset |
files
|
Thu, 10 Sep 1998 17:33:09 +0200 |
paulson |
Allows more backtracking in proof reconstruction, making it slower but more
|
changeset |
files
|
Thu, 10 Sep 1998 17:32:07 +0200 |
paulson |
a step to help a proof
|
changeset |
files
|
Thu, 10 Sep 1998 17:30:50 +0200 |
paulson |
new entries
|
changeset |
files
|