| #
ed7a971e |
|
05-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
| #
5abaa1a1 |
|
17-Oct-2018 |
paulson <lp15@cam.ac.uk> |
new theory Abstract_Topology with lots of stuff from HOL Light's metric.sml
|
| #
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;
|
| #
4f5ebd94 |
|
16-Mar-2014 |
haftmann <none@none> |
normalising simp rules for compound operators
|
| #
7abed3fd |
|
23-Mar-2013 |
haftmann <none@none> |
tuned proof
|
| #
6337ab39 |
|
12-Nov-2011 |
wenzelm <none@none> |
tuned proofs;
|
| #
a3372eca |
|
13-Sep-2011 |
noschinl <none@none> |
tune simpset for Complete_Lattices
|
| #
1ec48f36 |
|
09-Aug-2011 |
haftmann <none@none> |
tuned proofs
|
| #
baea5702 |
|
01-Mar-2010 |
haftmann <none@none> |
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
|
| #
079cde2d |
|
17-Oct-2009 |
wenzelm <none@none> |
eliminated hard tabulators, guessing at each author's individual tab-width;
tuned headers;
|
| #
f9ce79eb |
|
21-Sep-2009 |
haftmann <none@none> |
tuned proofs
|
| #
4c4a113a |
|
18-Sep-2009 |
haftmann <none@none> |
partially isarified proof
|
| #
7411135a |
|
22-Jul-2009 |
haftmann <none@none> |
moved complete_lattice &c. into separate theory
--HG--
rename : src/HOL/Set.thy => src/HOL/Complete_Lattice.thy
|
| #
121e82fb |
|
04-Mar-2009 |
blanchet <none@none> |
Merge.
|
| #
bb2d682e |
|
02-Mar-2009 |
nipkow <none@none> |
name changes
|
| #
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
|
| #
da2ac1c7 |
|
03-Aug-2004 |
paulson <none@none> |
new simprules Int_subset_iff and Un_subset_iff
|
| #
5125b879 |
|
15-Aug-2003 |
paulson <none@none> |
A document for UNITY
|
| #
7a7aaac2 |
|
30-Mar-2003 |
paulson <none@none> |
more comments and tweaks
|
| #
d16759d3 |
|
25-Mar-2003 |
paulson <none@none> |
Proofs for section 4.5.3
|
| #
14459920 |
|
21-Mar-2003 |
paulson <none@none> |
More on progress sets
|
| #
f9fdae1b |
|
18-Mar-2003 |
paulson <none@none> |
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
to the new Group setup.
Deleted Ring, Module from GroupTheory
Minor UNITY changes
|
| #
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
|