| #
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;
|
| #
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;
|
| #
5dae23be |
|
01-Mar-2010 |
wenzelm <none@none> |
tuned final whitespace;
|
| #
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;
|
| #
f9ce79eb |
|
21-Sep-2009 |
haftmann <none@none> |
tuned proofs
|
| #
7e8dd8a3 |
|
11-Jul-2007 |
berghofe <none@none> |
Adapted to new inductive definition package.
|
| #
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
|
| #
2a98d8d4 |
|
15-Jul-2004 |
nipkow <none@none> |
Moved to new m<..<n syntax for set intervals.
|
| #
5125b879 |
|
15-Aug-2003 |
paulson <none@none> |
A document for UNITY
|
| #
402829d8 |
|
15-Jul-2003 |
paulson <none@none> |
tidying
|
| #
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
|
| #
9434f141 |
|
23-Oct-2000 |
paulson <none@none> |
quantifiers now allowed in inductive defs
|
| #
0ec6027f |
|
23-Aug-2000 |
paulson <none@none> |
xsymbols for leads-to and Join
|
| #
3117c03a |
|
11-Nov-1999 |
paulson <none@none> |
tidied
|
| #
e468abb1 |
|
25-Aug-1999 |
paulson <none@none> |
arguably clearer definition of the inductive case of
leads-to.
No proofs had to be changed...
|
| #
d00c2f56 |
|
08-Jun-1999 |
paulson <none@none> |
renamed the underlying relation of leadsTo from "leadsto"
to "leads" to reduce the risk of confusion
|
| #
e545cd68 |
|
29-Apr-1999 |
paulson <none@none> |
made many specification operators infix
|
| #
8147eefa |
|
18-Nov-1998 |
paulson <none@none> |
Finally removing "Compl" from HOL
|
| #
42a66263 |
|
21-Oct-1998 |
berghofe <none@none> |
Changed interface of inductive.
|
| #
f8e376a9 |
|
15-Oct-1998 |
paulson <none@none> |
specifications as sets of programs
|
| #
bc92c072 |
|
19-Aug-1998 |
paulson <none@none> |
Misc changes
|
| #
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
|
| #
ffb63340 |
|
04-Aug-1998 |
paulson <none@none> |
Tidying
|
| #
adabc854 |
|
17-Jul-1998 |
paulson <none@none> |
added comments
|
| #
7ca6d8f9 |
|
02-Apr-1998 |
paulson <none@none> |
New UNITY theory
|