| Thu, 12 Oct 2000 18:38:23 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Mon, 09 Oct 2000 19:49:58 +0200 |
nipkow |
added rtranclIs
|
file |
diff |
annotate
|
| Thu, 29 Jun 2000 12:19:27 +0200 |
paulson |
tidied proofs using default rule equalityCE
|
file |
diff |
annotate
|
| Fri, 03 Mar 2000 18:26:19 +0100 |
paulson |
Added Tanja's Detects and Reachability theories. Also
|
file |
diff |
annotate
|
| Wed, 01 Sep 1999 11:16:02 +0200 |
paulson |
tidied some proofs
|
file |
diff |
annotate
|
| Fri, 21 May 1999 10:56:46 +0200 |
paulson |
preferring generic rules to specific ones...
|
file |
diff |
annotate
|
| Tue, 04 May 1999 10:26:00 +0200 |
paulson |
Invariant -> Always and other tidying
|
file |
diff |
annotate
|
| Thu, 29 Apr 1999 10:51:58 +0200 |
paulson |
made many specification operators infix
|
file |
diff |
annotate
|
| Fri, 23 Oct 1998 20:44:34 +0200 |
oheimb |
corrected auto_tac (applications of unsafe wrappers)
|
file |
diff |
annotate
|
| Thu, 15 Oct 1998 11:35:07 +0200 |
paulson |
specifications as sets of programs
|
file |
diff |
annotate
|
| Fri, 09 Oct 1998 11:16:52 +0200 |
nipkow |
renamed Suc_card_Diff or something
|
file |
diff |
annotate
|
| Wed, 23 Sep 1998 10:11:18 +0200 |
paulson |
tidying and deleting needless parentheses
|
file |
diff |
annotate
|
| Mon, 21 Sep 1998 23:12:31 +0200 |
oheimb |
added wrapper for bspec
|
file |
diff |
annotate
|
| Tue, 15 Sep 1998 15:04:07 +0200 |
paulson |
From Compl(A) to -A
|
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
|
| Wed, 02 Sep 1998 10:37:13 +0200 |
paulson |
modified proofs for new constrains_tac and ensures_tac
|
file |
diff |
annotate
|
| Thu, 13 Aug 1998 18:06:40 +0200 |
paulson |
Constrains, Stable, Invariant...more of the substitution axiom, but Union
|
file |
diff |
annotate
|
| Wed, 05 Aug 1998 10:57:25 +0200 |
paulson |
New record type of programs
|
file |
diff |
annotate
|
| Tue, 04 Aug 1998 10:50:33 +0200 |
paulson |
Constant "invariant" and new constrains_tac, ensures_tac
|
file |
diff |
annotate
|
| Fri, 31 Jul 1998 18:46:55 +0200 |
paulson |
Tidied; uses records
|
file |
diff |
annotate
|
| Fri, 24 Jul 1998 17:20:55 +0200 |
nipkow |
update -> fun_upd
|
file |
diff |
annotate
|
| Thu, 02 Jul 1998 16:53:55 +0200 |
paulson |
Uncurried functions LeadsTo and reach
|
file |
diff |
annotate
|
| Tue, 23 Jun 1998 18:07:45 +0200 |
nipkow |
Consequences of the change from [ := ] to ( := ) in theory Update.
|
file |
diff |
annotate
|
| Mon, 22 Jun 1998 17:26:46 +0200 |
wenzelm |
isatool fixgoal;
|
file |
diff |
annotate
|
| Tue, 05 May 1998 17:28:22 +0200 |
paulson |
New syntax for function update; moved to main HOL directory
|
file |
diff |
annotate
|
| Fri, 03 Apr 1998 12:34:33 +0200 |
paulson |
New UNITY theory
|
file |
diff |
annotate
|