| Mon, 24 May 1999 15:56:24 +0200 |
paulson |
renamed Lprg to Lift; simplified proof of Always_nonneg
|
file |
diff |
annotate
|
| Mon, 01 Mar 1999 18:38:43 +0100 |
paulson |
removed the infernal States, eqStates, compatible, etc.
|
file |
diff |
annotate
|
| Fri, 04 Dec 1998 10:42:53 +0100 |
paulson |
locales: assumes and defines may be empty
|
file |
diff |
annotate
|
| Thu, 03 Dec 1998 10:45:06 +0100 |
paulson |
Addition of the States component; parts of Comp not working
|
file |
diff |
annotate
|
| Wed, 18 Nov 1998 15:10:46 +0100 |
paulson |
Finally removing "Compl" from HOL
|
file |
diff |
annotate
|
| Thu, 01 Oct 1998 18:28:18 +0200 |
paulson |
abstype of programs
|
file |
diff |
annotate
|
| Tue, 29 Sep 1998 15:58:47 +0200 |
paulson |
Now id:(Acts prg) is implicit
|
file |
diff |
annotate
|
| Fri, 25 Sep 1998 13:58:24 +0200 |
paulson |
Now uses integers instead of naturals
|
file |
diff |
annotate
|
| Thu, 03 Sep 1998 16:40:02 +0200 |
paulson |
A new approach, using simp_of_act and simp_of_set to activate definitions when
|
file |
diff |
annotate
|
| Thu, 20 Aug 1998 17:43:01 +0200 |
paulson |
New theory Lift
|
file |
diff |
annotate
|
| Wed, 19 Aug 1998 10:34:31 +0200 |
paulson |
Misc changes
|
file |
diff |
annotate
|
| Fri, 14 Aug 1998 13:52:42 +0200 |
paulson |
now trans_tac is part of the claset...
|
file |
diff |
annotate
|
| Thu, 06 Aug 1998 15:47:26 +0200 |
paulson |
A higher-level treatment of LeadsTo, minimizing use of "reachable"
|
file |
diff |
annotate
|