| Mon, 19 Aug 1996 13:03:17 +0200 |
paulson |
Tidied up the proofs
|
changeset |
files
|
| Mon, 19 Aug 1996 11:51:39 +0200 |
paulson |
Added impOfSubs
|
changeset |
files
|
| Mon, 19 Aug 1996 11:49:31 +0200 |
paulson |
Now less_zeroE is a Safe Elim rule
|
changeset |
files
|
| Mon, 19 Aug 1996 11:33:08 +0200 |
paulson |
Improved comment
|
changeset |
files
|
| Mon, 19 Aug 1996 11:25:04 +0200 |
paulson |
Added proof of Un_insert_right
|
changeset |
files
|
| Mon, 19 Aug 1996 11:23:25 +0200 |
paulson |
Changed precedences to remove ambiguities in r^+ notation
|
changeset |
files
|
| Mon, 19 Aug 1996 11:22:16 +0200 |
paulson |
Improved the proof of Problem 38
|
changeset |
files
|
| Mon, 19 Aug 1996 11:20:37 +0200 |
paulson |
Added a lot of basic laws, from HOL/simpdata
|
changeset |
files
|
| Mon, 19 Aug 1996 11:19:55 +0200 |
paulson |
Renaming of functions, and tidying
|
changeset |
files
|
| Mon, 19 Aug 1996 11:19:16 +0200 |
paulson |
Now starts with set_current_thy
|
changeset |
files
|
| Mon, 19 Aug 1996 11:18:36 +0200 |
paulson |
Tidied some proofs
|
changeset |
files
|
| Mon, 19 Aug 1996 11:17:20 +0200 |
paulson |
Tidied some proofs, maybe using less_SucE
|
changeset |
files
|
| Mon, 19 Aug 1996 11:15:44 +0200 |
paulson |
Removal of less_SucE as default SE rule
|
changeset |
files
|
| Mon, 19 Aug 1996 11:12:38 +0200 |
paulson |
Renamed setOfList to set_of_list
|
changeset |
files
|