| Mon, 05 Jun 2006 14:22:58 +0200 |
krauss |
Added [simp]-lemmas "in_inv_image" and "in_lex_prod" in the spirit of "in_measure".
|
file |
diff |
annotate
|
| Fri, 17 Jun 2005 16:12:49 +0200 |
haftmann |
migrated theory headers to new format
|
file |
diff |
annotate
|
| Thu, 15 Jul 2004 13:11:34 +0200 |
nipkow |
Moved to new m<..<n syntax for set intervals.
|
file |
diff |
annotate
|
| Fri, 15 Aug 2003 13:07:01 +0200 |
paulson |
A document for UNITY
|
file |
diff |
annotate
|
| Tue, 15 Jul 2003 15:12:22 +0200 |
paulson |
tidying
|
file |
diff |
annotate
|
| Sat, 08 Feb 2003 16:05:33 +0100 |
paulson |
converting HOL/UNITY to use unconditional fairness
|
file |
diff |
annotate
|
| Tue, 04 Feb 2003 18:12:40 +0100 |
paulson |
some x-symbols
|
file |
diff |
annotate
|
| Fri, 31 Jan 2003 20:12:44 +0100 |
paulson |
conversion to new-style theories and tidying
|
file |
diff |
annotate
|
| Thu, 30 Jan 2003 18:08:09 +0100 |
paulson |
conversion of UNITY theories to new-style
|
file |
diff |
annotate
|
| Tue, 09 Jan 2001 15:32:27 +0100 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Fri, 05 Jan 2001 18:48:18 +0100 |
nipkow |
^^ -> ```
|
file |
diff |
annotate
|
| Mon, 23 Oct 2000 15:20:32 +0200 |
paulson |
quantifiers now allowed in inductive defs
|
file |
diff |
annotate
|
| Thu, 24 Aug 2000 12:39:24 +0200 |
paulson |
xsymbols for leads-to and Join
|
file |
diff |
annotate
|
| Thu, 11 Nov 1999 10:25:29 +0100 |
paulson |
tidied
|
file |
diff |
annotate
|
| Wed, 25 Aug 1999 11:04:28 +0200 |
paulson |
arguably clearer definition of the inductive case of
|
file |
diff |
annotate
|
| Tue, 08 Jun 1999 10:59:02 +0200 |
paulson |
renamed the underlying relation of leadsTo from "leadsto"
|
file |
diff |
annotate
|
| Thu, 29 Apr 1999 10:51:58 +0200 |
paulson |
made many specification operators infix
|
file |
diff |
annotate
|
| Wed, 18 Nov 1998 15:10:46 +0100 |
paulson |
Finally removing "Compl" from HOL
|
file |
diff |
annotate
|
| Wed, 21 Oct 1998 17:57:02 +0200 |
berghofe |
Changed interface of inductive.
|
file |
diff |
annotate
|
| Thu, 15 Oct 1998 11:35:07 +0200 |
paulson |
specifications as sets of programs
|
file |
diff |
annotate
|
| Wed, 19 Aug 1998 10:34:31 +0200 |
paulson |
Misc changes
|
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
|
| Wed, 05 Aug 1998 10:57:25 +0200 |
paulson |
New record type of programs
|
file |
diff |
annotate
|
| Tue, 04 Aug 1998 10:50:04 +0200 |
paulson |
Tidying
|
file |
diff |
annotate
|
| Fri, 17 Jul 1998 10:50:28 +0200 |
paulson |
added comments
|
file |
diff |
annotate
|
| Fri, 03 Apr 1998 12:34:33 +0200 |
paulson |
New UNITY theory
|
file |
diff |
annotate
|