| #
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
|
| #
6fc0f068 |
|
28-Dec-2015 |
wenzelm <none@none> |
prefer symbols for "Union", "Inter";
|
| #
6820dd05 |
|
10-Dec-2015 |
paulson <lp15@cam.ac.uk> |
not_leE -> not_le_imp_less and other tidying
|
| #
f55b23fd |
|
23-Jul-2015 |
wenzelm <none@none> |
more symbols by default, without xsymbols mode;
|
| #
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
| #
f4961062 |
|
20-Nov-2011 |
wenzelm <none@none> |
eliminated obsolete "standard";
|
| #
6337ab39 |
|
12-Nov-2011 |
wenzelm <none@none> |
tuned proofs;
|
| #
1ec48f36 |
|
09-Aug-2011 |
haftmann <none@none> |
tuned proofs
|
| #
deac04eb |
|
22-Jul-2010 |
wenzelm <none@none> |
updated some headers;
|
| #
baea5702 |
|
01-Mar-2010 |
haftmann <none@none> |
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
|
| #
942a6e5f |
|
24-Feb-2010 |
wenzelm <none@none> |
modernized syntax declarations, and make them actually work with authentic syntax;
|
| #
5f9d11da |
|
05-Jun-2006 |
krauss <none@none> |
Added [simp]-lemmas "in_inv_image" and "in_lex_prod" in the spirit of "in_measure".
This simplifies some proofs.
|
| #
a7060872 |
|
17-Jun-2005 |
haftmann <none@none> |
migrated theory headers to new format
|
| #
5125b879 |
|
15-Aug-2003 |
paulson <none@none> |
A document for UNITY
|
| #
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
|
| #
06317d69 |
|
30-Jan-2003 |
paulson <none@none> |
converting more UNITY theories to new-style
|
| #
0ec6027f |
|
23-Aug-2000 |
paulson <none@none> |
xsymbols for leads-to and Join
|
| #
808483ad |
|
13-Jan-2000 |
paulson <none@none> |
working version, with Alloc now working on the same state space as the whole
system. Partial removal of ELT.
|
| #
35a6290a |
|
30-Nov-1999 |
paulson <none@none> |
working version with new theory ELT
|
| #
63864756 |
|
04-May-1999 |
paulson <none@none> |
new definitions of Co and LeadsTo
|
| #
e545cd68 |
|
29-Apr-1999 |
paulson <none@none> |
made many specification operators infix
|
| #
f8e376a9 |
|
15-Oct-1998 |
paulson <none@none> |
specifications as sets of programs
|
| #
bfd9c441 |
|
07-Oct-1998 |
paulson <none@none> |
tidying and renaming
|
| #
69fe247a |
|
13-Aug-1998 |
paulson <none@none> |
Constrains, Stable, Invariant...more of the substitution axiom, but Union
does not work well with them
|
| #
3ae293aa |
|
06-Aug-1998 |
paulson <none@none> |
A higher-level treatment of LeadsTo, minimizing use of "reachable"
|
| #
753e936b |
|
05-Aug-1998 |
paulson <none@none> |
New record type of programs
|
| #
ccab53f5 |
|
02-Jul-1998 |
paulson <none@none> |
Uncurried functions LeadsTo and reach
Deleted leading parameters thanks to new Goal command
|
| #
7ca6d8f9 |
|
02-Apr-1998 |
paulson <none@none> |
New UNITY theory
|