20100608 
haftmann 
20100608 
qualified types "+" and nat; qualified constants Ball, Bex, Suc, curry; modernized some specifications

file  diff  annotate 
20100328 
huffman 
20100328 
use lattice theorems to prove set theorems

file  diff  annotate 
20100318 
blanchet 
20100318 
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"

file  diff  annotate 
20100304 
hoelzl 
20100304 
Added vimage_inter_cong

file  diff  annotate 
20100301 
haftmann 
20100301 
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)

file  diff  annotate 
20100211 
wenzelm 
20100211 
modernized translations;
formal markup of @{syntax_const} and @{const_syntax};
minor tuning;

file  diff  annotate 
20100204 
hoelzl 
20100204 
Changed 'bounded unique existential quantifiers' from a constant to syntax translation.

file  diff  annotate 
20100128 
haftmann 
20100128 
new theory Algebras.thy for generic algebraic structures

file  diff  annotate 
20091230 
krauss 
20091230 
killed a few warnings

file  diff  annotate 
20091127 
berghofe 
20091127 
Removed eq_to_mono2, added not_mono.

file  diff  annotate 
20091109 
paulson 
20091109 
New theory Probability/Borel.thy, and some associated lemmas

file  diff  annotate 
20091021 
paulson 
20091021 
merged

file  diff  annotate 
20091020 
paulson 
20091020 
Some new lemmas concerning sets

file  diff  annotate 
20091021 
haftmann 
20091021 
merged

file  diff  annotate 
20091021 
haftmann 
20091021 
dropped redundant gen_ prefix

file  diff  annotate 
20091020 
haftmann 
20091020 
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions

file  diff  annotate 
20091020 
paulson 
20091020 
Removal of the unused atpset concept, the atp attribute and some related code.

file  diff  annotate 
20091007 
haftmann 
20091007 
tuned proofs

file  diff  annotate 
20090919 
haftmann 
20090919 
inter and union are mere abbreviations for inf and sup

file  diff  annotate 
20090831 
nipkow 
20090831 
tuned the simp rules for Int involving insert and intervals.

file  diff  annotate 
20090728 
haftmann 
20090728 
Set.UNIV and Set.empty are mere abbreviations for top and bot

file  diff  annotate 
20090722 
haftmann 
20090722 
moved complete_lattice &c. into separate theory

file  diff  annotate 
20090722 
haftmann 
20090722 
set intersection and union now named inter and union; closer connection between set and lattice operations; factored out complete lattice

file  diff  annotate 
20090721 
haftmann 
20090721 
attempt for more concise setup of nonetacontracting binders

file  diff  annotate 
20090721 
haftmann 
20090721 
Set.thy: prefer = over == where possible; tuned ML setup; dropped (moved) ML legacy

file  diff  annotate 
20090721 
haftmann 
20090721 
swapped bootstrap order of UNION/Union and INTER/Inter in theory Set

file  diff  annotate 
20090720 
haftmann 
20090720 
less digestible

file  diff  annotate 
20090720 
haftmann 
20090720 
refined outline structure

file  diff  annotate 
20090720 
haftmann 
20090720 
merged

file  diff  annotate 
20090720 
haftmann 
20090720 
closer relation of sets and complete lattices; corresponding consts, defs and syntax at similar places in theory text

file  diff  annotate 
20090720 
haftmann 
20090720 
merged

file  diff  annotate 
20090714 
haftmann 
20090714 
refinement of lattice classes

file  diff  annotate 
20090715 
wenzelm 
20090715 
more antiquotations;

file  diff  annotate 
20090711 
haftmann 
20090711 
added boolean_algebra type class; tuned lattice duals

file  diff  annotate 
20090706 
wenzelm 
20090706 
structure Thm: less pervasive names;

file  diff  annotate 
20090615 
haftmann 
20090615 
authentic syntax for Pow and image

file  diff  annotate 
20090605 
haftmann 
20090605 
merged

file  diff  annotate 
20090604 
haftmann 
20090604 
insert now qualified and with authentic syntax

file  diff  annotate 
20090604 
nipkow 
20090604 
finite lemmas

file  diff  annotate 
20090518 
nipkow 
20090518 
finetuned elimination of comprehensions involving x=t.

file  diff  annotate 
20090516 
nipkow 
20090516 
"{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}"
by the new simproc defColl_regroup. More precisely, the simproc pulls an
equation x=t (or t=x) out of a nest of conjunctions to the front where the
simp rule singleton_conj_conv(2) converts to "if".

file  diff  annotate 
20090331 
wenzelm 
20090331 
tuned;

file  diff  annotate 
20090319 
haftmann 
20090319 
tuned some theorem and attribute bindings

file  diff  annotate 
20090314 
haftmann 
20090314 
reverted to old version of Set.thy  strange effects have to be traced first

file  diff  annotate 
20090307 
haftmann 
20090307 
restructured theory Set.thy

file  diff  annotate 
20090305 
haftmann 
20090305 
set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax

file  diff  annotate 
20090213 
nipkow 
20090213 
finiteness lemmas

file  diff  annotate 
20090129 
berghofe 
20090129 
Added strong congruence rule for UN.

file  diff  annotate 
20081010 
haftmann 
20081010 
`code func` now just `code`

file  diff  annotate 
20080811 
haftmann 
20080811 
rudimentary code setup for set operations

file  diff  annotate 
20080701 
huffman 
20080701 
remove simp attribute from range_composition

file  diff  annotate 
20080610 
haftmann 
20080610 
removed some dubious code lemmas

file  diff  annotate 
20080507 
berghofe 
20080507 
 Now uses Orderings as parent theory
 "'a set" is now just a type abbreviation for "'a => bool"
 The instantiation "set :: (type) ord" and the definition of (p)subset is
no longer needed, since it is subsumed by the order on functions and booleans.
The derived theorems (p)subset_eq can be used as a replacement.
 mem_Collect_eq and Collect_mem_eq can now be derived from the definitions
of mem and Collect.
 Replaced the instantiation "set :: (type) minus" by the two instantiations
"fun :: (type, minus) minus" and "bool :: minus". The theorem set_diff_eq
can be used as a replacement for the definition set_diff_def
 Replaced the instantiation "set :: (type) uminus" by the two instantiations
"fun :: (type, uminus) uminus" and "bool :: uminus". The theorem Compl_eq
can be used as a replacement for the definition Compl_def.
 Variable P in rule split_if must be instantiated manually in proof of
split_if_mem2 due to problems with HO unification
 Moved definition of dense linear orders and proofs about LEAST from
Orderings to Set
 Deleted code setup for sets

file  diff  annotate 
20080422 
haftmann 
20080422 
constant HOL.eq now qualified

file  diff  annotate 
20080402 
haftmann 
20080402 
explicit class "eq" for operational equality

file  diff  annotate 
20080329 
wenzelm 
20080329 
replaced 'ML_setup' by 'ML';

file  diff  annotate 
20080319 
wenzelm 
20080319 
eliminated change_claset/simpset;

file  diff  annotate 
20080226 
haftmann 
20080226 
moved some set lemmas from Set.thy here

file  diff  annotate 
20080125 
haftmann 
20080125 
improved code theorem setup

file  diff  annotate 
20080102 
haftmann 
20080102 
splitted class uminus from class minus

file  diff  annotate 