| Wed, 25 May 2016 11:50:58 +0200 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 21:51:56 +0100 |
haftmann |
prefer abbreviations for compound operators INFIMUM and SUPREMUM
|
file |
diff |
annotate
|
| Mon, 28 Dec 2015 17:43:30 +0100 |
wenzelm |
prefer symbols for "Union", "Inter";
|
file |
diff |
annotate
|
| Thu, 10 Dec 2015 13:38:40 +0000 |
paulson |
not_leE -> not_le_imp_less and other tidying
|
file |
diff |
annotate
|
| Thu, 23 Jul 2015 22:13:42 +0200 |
wenzelm |
more symbols by default, without xsymbols mode;
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| Sun, 20 Nov 2011 21:05:23 +0100 |
wenzelm |
eliminated obsolete "standard";
|
file |
diff |
annotate
|
| Sat, 12 Nov 2011 21:10:56 +0100 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Tue, 09 Aug 2011 20:24:48 +0200 |
haftmann |
tuned proofs
|
file |
diff |
annotate
|
| Thu, 22 Jul 2010 18:08:39 +0200 |
wenzelm |
updated some headers;
|
file |
diff |
annotate
|
| Mon, 01 Mar 2010 17:45:19 +0100 |
wenzelm |
tuned final whitespace;
|
file |
diff |
annotate
|
| Mon, 01 Mar 2010 13:42:31 +0100 |
haftmann |
merged
|
file |
diff |
annotate
|
| Mon, 01 Mar 2010 13:40:23 +0100 |
haftmann |
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
|
file |
diff |
annotate
|
| Wed, 24 Feb 2010 22:09:50 +0100 |
wenzelm |
modernized syntax declarations, and make them actually work with authentic syntax;
|
file |
diff |
annotate
|
| Mon, 21 Sep 2009 15:35:15 +0200 |
haftmann |
tuned proofs
|
file |
diff |
annotate
|
| Wed, 11 Jul 2007 11:46:44 +0200 |
berghofe |
Adapted to new inductive definition package.
|
file |
diff |
annotate
|
| 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
|