| #
ed7a971e |
|
05-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
| #
f5796e6d |
|
14-Feb-2018 |
wenzelm <none@none> |
more symbols;
|
| #
5385dbfa |
|
16-Jan-2018 |
wenzelm <none@none> |
standardized towards new-style formal comments: isabelle update_comments;
|
| #
ef344a77 |
|
25-May-2016 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
| #
6fc0f068 |
|
28-Dec-2015 |
wenzelm <none@none> |
prefer symbols for "Union", "Inter";
|
| #
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
| #
c82bd4c5 |
|
12-Oct-2012 |
wenzelm <none@none> |
discontinued obsolete typedef (open) syntax;
|
| #
dc6cdd46 |
|
21-Feb-2012 |
wenzelm <none@none> |
tuned proofs;
|
| #
d8e74f87 |
|
30-Nov-2011 |
wenzelm <none@none> |
prefer typedef without extra definition and alternative name;
tuned proofs;
|
| #
f4961062 |
|
20-Nov-2011 |
wenzelm <none@none> |
eliminated obsolete "standard";
|
| #
a5f328ca |
|
12-May-2010 |
wenzelm <none@none> |
modernized specifications;
|
| #
baea5702 |
|
01-Mar-2010 |
haftmann <none@none> |
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
|
| #
079cde2d |
|
17-Oct-2009 |
wenzelm <none@none> |
eliminated hard tabulators, guessing at each author's individual tab-width;
tuned headers;
|
| #
121e82fb |
|
04-Mar-2009 |
blanchet <none@none> |
Merge.
|
| #
bb2d682e |
|
02-Mar-2009 |
nipkow <none@none> |
name changes
|
| #
99b04075 |
|
03-Aug-2007 |
wenzelm <none@none> |
misc cleanup of ML bindings (for multihreading);
|
| #
a7060872 |
|
17-Jun-2005 |
haftmann <none@none> |
migrated theory headers to new format
|
| #
737fdea6 |
|
02-Jun-2005 |
paulson <none@none> |
renamed "constrains" to "safety" to avoid keyword clash
|
| #
04246c0e |
|
21-Apr-2004 |
wenzelm <none@none> |
constdefs: proper order;
|
| #
5125b879 |
|
15-Aug-2003 |
paulson <none@none> |
A document for UNITY
|
| #
f9fdae1b |
|
18-Mar-2003 |
paulson <none@none> |
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
to the new Group setup.
Deleted Ring, Module from GroupTheory
Minor UNITY changes
|
| #
db7b0190 |
|
14-Mar-2003 |
paulson <none@none> |
Proved the main lemma on progress sets
|
| #
5bb51f23 |
|
08-Feb-2003 |
paulson <none@none> |
converting HOL/UNITY to use unconditional fairness
|
| #
2380b71a |
|
04-Feb-2003 |
paulson <none@none> |
some x-symbols
|
| #
1674bc09 |
|
31-Jan-2003 |
paulson <none@none> |
conversion to new-style theories and tidying
|
| #
8671b95c |
|
30-Jan-2003 |
paulson <none@none> |
conversion of UNITY theories to new-style
|
| #
9a40d08d |
|
09-Jan-2001 |
nipkow <none@none> |
*** empty log message ***
|
| #
2c1f2b82 |
|
05-Jan-2001 |
nipkow <none@none> |
^^ -> ```
Univalent -> single_valued
|
| #
ced4250f |
|
23-Sep-2000 |
paulson <none@none> |
added compatibility relation: AllowedActs, Allowed, ok,
OK and changes to "guarantees", etc.
|
| #
ee8f28f8 |
|
24-May-2000 |
paulson <none@none> |
restructuring: LessThan.ML mostly moved to HOL/SetInterval.ML
|
| #
4b11080c |
|
13-Jun-1999 |
paulson <none@none> |
new-style infix directives
|
| #
f02d3cba |
|
24-May-1999 |
paulson <none@none> |
increasing makes sense only for partial orderings
|
| #
e545cd68 |
|
29-Apr-1999 |
paulson <none@none> |
made many specification operators infix
|
| #
a3811982 |
|
28-Apr-1999 |
paulson <none@none> |
eliminated theory UNITY/Traces
|
| #
cc98d9f9 |
|
06-Nov-1998 |
paulson <none@none> |
Revising the Client proof as suggested by Michel Charpentier. New lemmas
about composition (in Union.ML), etc. Also changed "length" to "size"
because it is displayed as "size" in any event.
|
| #
f8e376a9 |
|
15-Oct-1998 |
paulson <none@none> |
specifications as sets of programs
|
| #
753e936b |
|
05-Aug-1998 |
paulson <none@none> |
New record type of programs
|
| #
1828732b |
|
13-Jul-1998 |
paulson <none@none> |
renamed mutex to Acts
|
| #
7ca6d8f9 |
|
02-Apr-1998 |
paulson <none@none> |
New UNITY theory
|