#
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";
|
#
f67d856d |
|
25-Mar-2015 |
wenzelm <none@none> |
prefer local fixes;
|
#
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
#
7f9cbadc |
|
13-Mar-2012 |
wenzelm <none@none> |
tuned context specifications and proofs;
|
#
548fd697 |
|
13-Mar-2012 |
wenzelm <none@none> |
tuned proofs;
|
#
dc6cdd46 |
|
21-Feb-2012 |
wenzelm <none@none> |
tuned proofs;
|
#
f4961062 |
|
20-Nov-2011 |
wenzelm <none@none> |
eliminated obsolete "standard";
|
#
1ec48f36 |
|
09-Aug-2011 |
haftmann <none@none> |
tuned proofs
|
#
a5f328ca |
|
12-May-2010 |
wenzelm <none@none> |
modernized specifications;
|
#
079cde2d |
|
17-Oct-2009 |
wenzelm <none@none> |
eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
|
#
ce8fb085 |
|
07-May-2008 |
berghofe <none@none> |
Adapted to encoding of sets as predicates
|
#
71a3d0fe |
|
19-Mar-2008 |
haftmann <none@none> |
tuned proof
|
#
7e8dd8a3 |
|
11-Jul-2007 |
berghofe <none@none> |
Adapted to new inductive definition package.
|
#
a7060872 |
|
17-Jun-2005 |
haftmann <none@none> |
migrated theory headers to new format
|
#
875e024b |
|
27-Feb-2003 |
paulson <none@none> |
restored some deleted lemmas
|
#
3c4494d5 |
|
15-Feb-2003 |
paulson <none@none> |
minor revisions
|
#
5bb51f23 |
|
08-Feb-2003 |
paulson <none@none> |
converting HOL/UNITY to use unconditional fairness
|
#
1674bc09 |
|
31-Jan-2003 |
paulson <none@none> |
conversion to new-style theories and tidying
|
#
e1895cc3 |
|
29-Jan-2003 |
paulson <none@none> |
converting UNITY to new-style theories
|
#
9a40d08d |
|
09-Jan-2001 |
nipkow <none@none> |
*** empty log message ***
|
#
9434f141 |
|
23-Oct-2000 |
paulson <none@none> |
quantifiers now allowed in inductive defs
|
#
07f81ce6 |
|
13-Jan-2000 |
paulson <none@none> |
still working; a bit of polishing
|
#
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.
|
#
af5cc5fc |
|
22-Dec-1999 |
paulson <none@none> |
removing the "{} : CC" requirement for leadsTo[CC]
|
#
af066af4 |
|
08-Dec-1999 |
paulson <none@none> |
abolition of localTo: instead "guarantees" has local vars as extra argument
|
#
8bc0da8f |
|
01-Dec-1999 |
paulson <none@none> |
new generalized leads-to theory
|