| #
ed7a971e |
|
05-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
| #
09859749 |
|
18-Nov-2018 |
haftmann <none@none> |
removed legacy input syntax
|
| #
f5796e6d |
|
14-Feb-2018 |
wenzelm <none@none> |
more symbols;
|
| #
ef344a77 |
|
25-May-2016 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
| #
6688eecc |
|
17-Feb-2016 |
haftmann <none@none> |
prefer abbreviations for compound operators INFIMUM and SUPREMUM
|
| #
c9f3da2d |
|
27-Dec-2015 |
wenzelm <none@none> |
discontinued ASCII replacement syntax <->;
|
| #
f55b23fd |
|
23-Jul-2015 |
wenzelm <none@none> |
more symbols by default, without xsymbols mode;
|
| #
7f5a6758 |
|
26-Jun-2015 |
wenzelm <none@none> |
proper spacing, as for other syntax for these symbols;
|
| #
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
| #
03184bca |
|
22-Mar-2014 |
haftmann <none@none> |
generalized and strengthened cong rules on compound operators, similar to 1ed737a98198
|
| #
dc6cdd46 |
|
21-Feb-2012 |
wenzelm <none@none> |
tuned proofs;
|
| #
f4961062 |
|
20-Nov-2011 |
wenzelm <none@none> |
eliminated obsolete "standard";
|
| #
7e65ae14 |
|
14-Sep-2011 |
hoelzl <none@none> |
renamed Complete_Lattices lemmas, removed legacy names
|
| #
a5f328ca |
|
12-May-2010 |
wenzelm <none@none> |
modernized specifications;
|
| #
31fa3986 |
|
02-Mar-2010 |
wenzelm <none@none> |
notation for xsymbols (cf. ad039d29e01c);
|
| #
db258df9 |
|
02-Mar-2010 |
wenzelm <none@none> |
proper (type_)notation;
|
| #
4818a82c |
|
09-Feb-2010 |
wenzelm <none@none> |
modernized translations;
|
| #
3403212c |
|
08-Feb-2010 |
wenzelm <none@none> |
modernized some syntax translations;
|
| #
079cde2d |
|
17-Oct-2009 |
wenzelm <none@none> |
eliminated hard tabulators, guessing at each author's individual tab-width;
tuned headers;
|
| #
bf255bf9 |
|
05-Mar-2009 |
haftmann <none@none> |
set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
|
| #
0cca26eb |
|
01-Aug-2005 |
wenzelm <none@none> |
no eq_commute;
|
| #
a7060872 |
|
17-Jun-2005 |
haftmann <none@none> |
migrated theory headers to new format
|
| #
5125b879 |
|
15-Aug-2003 |
paulson <none@none> |
A document for UNITY
|
| #
3c4494d5 |
|
15-Feb-2003 |
paulson <none@none> |
minor revisions
|
| #
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
|
| #
b4eac3e6 |
|
29-Jan-2003 |
paulson <none@none> |
converted more UNITY theories to new-style
|
| #
c1694cb4 |
|
08-Nov-2001 |
wenzelm <none@none> |
eliminated old "symbols" syntax, use "xsymbols" instead;
|
| #
ced4250f |
|
23-Sep-2000 |
paulson <none@none> |
added compatibility relation: AllowedActs, Allowed, ok,
OK and changes to "guarantees", etc.
|
| #
0ec6027f |
|
23-Aug-2000 |
paulson <none@none> |
xsymbols for leads-to and Join
|
| #
af066af4 |
|
08-Dec-1999 |
paulson <none@none> |
abolition of localTo: instead "guarantees" has local vars as extra argument
|
| #
9c72ed0f |
|
27-Oct-1999 |
paulson <none@none> |
working again; new treatment of LocalTo
|
| #
582af8ae |
|
22-Oct-1999 |
paulson <none@none> |
ALMOST working version: LocalTo results commented out
|
| #
2289e39b |
|
18-Oct-1999 |
paulson <none@none> |
working version with localTo[C] instead of localTo
|
| #
c3c5e8fb |
|
11-Oct-1999 |
paulson <none@none> |
working shapshot with "projecting" and "extending"
|
| #
972bc043 |
|
26-Aug-1999 |
paulson <none@none> |
extra syntax for JN, making it more like UN
|
| #
a6490db6 |
|
01-Mar-1999 |
paulson <none@none> |
removed the infernal States, eqStates, compatible, etc.
|
| #
76d0cd85 |
|
03-Dec-1998 |
paulson <none@none> |
Addition of the States component; parts of Comp not working
|
| #
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
|
| #
8a914319 |
|
05-Oct-1998 |
paulson <none@none> |
Join now an infix operator
|
| #
cf01c6b7 |
|
01-Oct-1998 |
paulson <none@none> |
abstype of programs
|
| #
a6909c01 |
|
29-Sep-1998 |
paulson <none@none> |
Now id:(Acts prg) is implicit
|
| #
69fe247a |
|
13-Aug-1998 |
paulson <none@none> |
Constrains, Stable, Invariant...more of the substitution axiom, but Union
does not work well with them
|
| #
78659260 |
|
05-Aug-1998 |
paulson <none@none> |
Null program and a few new results
|
| #
ff0bf545 |
|
05-Aug-1998 |
paulson <none@none> |
Union primitives and examples
|