| #
e5238d11 |
|
28-Jan-2019 |
nipkow <none@none> |
more canonical and less specialized syntax
|
| #
504acaca |
|
14-Jan-2019 |
haftmann <none@none> |
tuned proofs
|
| #
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
|
| #
f67d856d |
|
25-Mar-2015 |
wenzelm <none@none> |
prefer local fixes;
|
| #
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
|
| #
548fd697 |
|
13-Mar-2012 |
wenzelm <none@none> |
tuned proofs;
|
| #
ad9e459c |
|
11-Sep-2011 |
nipkow <none@none> |
new fastforce replacing fastsimp - less confusing name
|
| #
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)
|
| #
f9ce79eb |
|
21-Sep-2009 |
haftmann <none@none> |
tuned proofs
|
| #
02f1fc44 |
|
16-Sep-2009 |
haftmann <none@none> |
Inter and Union are mere abbreviations for Inf and Sup
|
| #
13866ee3 |
|
24-Apr-2009 |
haftmann <none@none> |
funpow and relpow with shared "^^" syntax
|
| #
39f27693 |
|
20-Apr-2009 |
haftmann <none@none> |
power operation on functions with syntax o^; power operation on relations with syntax ^^
|
| #
ce8fb085 |
|
07-May-2008 |
berghofe <none@none> |
Adapted to encoding of sets as predicates
|
| #
1a780cb0 |
|
20-Aug-2007 |
haftmann <none@none> |
Sup now explicit parameter of complete_lattice
|
| #
7e8dd8a3 |
|
11-Jul-2007 |
berghofe <none@none> |
Adapted to new inductive definition package.
|
| #
04d897fa |
|
09-Dec-2006 |
nipkow <none@none> |
Modified lattice locale
|
| #
ff13c87f |
|
12-Nov-2006 |
nipkow <none@none> |
started reorgnization of lattice theories
|
| #
e7f7aeb8 |
|
13-Oct-2006 |
berghofe <none@none> |
Adapted to changes in FixedPoint theory.
|
| #
a7060872 |
|
17-Jun-2005 |
haftmann <none@none> |
migrated theory headers to new format
|
| #
34bbf13d |
|
10-Oct-2004 |
nipkow <none@none> |
Proofs needed to be updated because induction now preserves name of
induction variable.
|
| #
da2ac1c7 |
|
03-Aug-2004 |
paulson <none@none> |
new simprules Int_subset_iff and Un_subset_iff
|
| #
14459920 |
|
21-Mar-2003 |
paulson <none@none> |
More on progress sets
|
| #
64b1b57f |
|
17-Mar-2003 |
paulson <none@none> |
More "progress set" material
|
| #
db7b0190 |
|
14-Mar-2003 |
paulson <none@none> |
Proved the main lemma on progress sets
|
| #
e1ced77a |
|
10-Mar-2003 |
paulson <none@none> |
New theory ProgressSets. Definition of closure sets
|
| #
048181da |
|
06-Mar-2003 |
paulson <none@none> |
new UNITY examples theory
|
| #
c34ddf4c |
|
26-Feb-2003 |
paulson <none@none> |
completed proofs for programs consisting of a single assignment
|
| #
23e3bd2b |
|
18-Feb-2003 |
paulson <none@none> |
new theory Transformers: Meier-Sanders non-interference theory
|