| Tue, 21 Feb 2012 17:09:17 +0100 |
tuned proofs;
|
file | diff | annotate |
| Wed, 30 Nov 2011 16:27:10 +0100 |
prefer typedef without extra definition and alternative name;
|
file | diff | annotate |
| Sun, 20 Nov 2011 21:05:23 +0100 |
eliminated obsolete "standard";
|
file | diff | annotate |
| Wed, 12 May 2010 16:44:49 +0200 |
modernized specifications;
|
file | diff | annotate |
| Mon, 01 Mar 2010 13:40:23 +0100 |
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
|
file | diff | annotate |
| Sat, 17 Oct 2009 14:43:18 +0200 |
eliminated hard tabulators, guessing at each author's individual tab-width;
|
file | diff | annotate |
| Mon, 02 Mar 2009 16:53:55 +0100 |
name changes
|
file | diff | annotate |
| Fri, 03 Aug 2007 20:19:41 +0200 |
misc cleanup of ML bindings (for multihreading);
|
file | diff | annotate |
| Fri, 17 Jun 2005 16:12:49 +0200 |
migrated theory headers to new format
|
file | diff | annotate |
| Thu, 02 Jun 2005 13:47:08 +0200 |
renamed "constrains" to "safety" to avoid keyword clash
|
file | diff | annotate |
| Thu, 22 Apr 2004 12:11:17 +0200 |
constdefs: proper order;
|
file | diff | annotate |
| Fri, 15 Aug 2003 13:07:01 +0200 |
A document for UNITY
|
file | diff | annotate |
| Tue, 18 Mar 2003 18:07:06 +0100 |
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
|
file | diff | annotate |
| Fri, 14 Mar 2003 10:30:46 +0100 |
Proved the main lemma on progress sets
|
file | diff | annotate |
| Sat, 08 Feb 2003 16:05:33 +0100 |
converting HOL/UNITY to use unconditional fairness
|
file | diff | annotate |
| Tue, 04 Feb 2003 18:12:40 +0100 |
some x-symbols
|
file | diff | annotate |
| Fri, 31 Jan 2003 20:12:44 +0100 |
conversion to new-style theories and tidying
|
file | diff | annotate |
| Thu, 30 Jan 2003 18:08:09 +0100 |
conversion of UNITY theories to new-style
|
file | diff | annotate |
| Tue, 09 Jan 2001 15:32:27 +0100 |
*** empty log message ***
|
file | diff | annotate |
| Fri, 05 Jan 2001 18:48:18 +0100 |
^^ -> ```
|
file | diff | annotate |
| Sat, 23 Sep 2000 16:02:01 +0200 |
added compatibility relation: AllowedActs, Allowed, ok,
|
file | diff | annotate |
| Wed, 24 May 2000 18:40:01 +0200 |
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
|
file | diff | annotate |
| Sun, 13 Jun 1999 13:53:33 +0200 |
new-style infix directives
|
file | diff | annotate |
| Mon, 24 May 1999 15:50:53 +0200 |
increasing makes sense only for partial orderings
|
file | diff | annotate |
| Thu, 29 Apr 1999 10:51:58 +0200 |
made many specification operators infix
|
file | diff | annotate |
| Wed, 28 Apr 1999 13:36:31 +0200 |
eliminated theory UNITY/Traces
|
file | diff | annotate |
| Fri, 06 Nov 1998 13:20:29 +0100 |
Revising the Client proof as suggested by Michel Charpentier. New lemmas
|
file | diff | annotate |
| Thu, 15 Oct 1998 11:35:07 +0200 |
specifications as sets of programs
|
file | diff | annotate |
| Wed, 05 Aug 1998 10:57:25 +0200 |
New record type of programs
|
file | diff | annotate |
| Mon, 13 Jul 1998 16:41:30 +0200 |
renamed mutex to Acts
|
file | diff | annotate |
| Fri, 03 Apr 1998 12:34:33 +0200 |
New UNITY theory
|
file | diff | annotate |