2010-12-19 huffman [Sun, 19 Dec 2010 18:15:21 -0800] rev 41296
switch to transparent ascription, to avoid warning messages
src/HOL/HOLCF/Tools/Domain/domain.ML src/HOL/HOLCF/Tools/Domain/domain_constructors.ML src/HOL/HOLCF/Tools/Domain/domain_induction.ML src/HOL/HOLCF/Tools/cont_proc.ML src/HOL/HOLCF/Tools/cpodef.ML src/HOL/HOLCF/Tools/domaindef.ML src/HOL/HOLCF/Tools/fixrec.ML

2010-12-19 huffman [Sun, 19 Dec 2010 18:11:20 -0800] rev 41295
types -> type_synonym
src/HOL/HOLCF/One.thy src/HOL/HOLCF/Tr.thy src/HOL/HOLCF/Universal.thy

2010-12-19 huffman [Sun, 19 Dec 2010 18:10:54 -0800] rev 41294
fix typo
NEWS

2010-12-19 huffman [Sun, 19 Dec 2010 17:39:20 -0800] rev 41293
merged

2010-12-19 huffman [Sun, 19 Dec 2010 17:37:19 -0800] rev 41292
use deflations over type 'udom u' to represent predomains;
removed now-unnecessary class liftdomain;
src/HOL/HOLCF/Domain.thy src/HOL/HOLCF/Library/Bool_Discrete.thy src/HOL/HOLCF/Library/Char_Discrete.thy src/HOL/HOLCF/Library/Defl_Bifinite.thy src/HOL/HOLCF/Library/Int_Discrete.thy src/HOL/HOLCF/Library/List_Predomain.thy src/HOL/HOLCF/Library/Nat_Discrete.thy src/HOL/HOLCF/Library/Option_Cpo.thy src/HOL/HOLCF/Library/Sum_Cpo.thy src/HOL/HOLCF/Powerdomains.thy src/HOL/HOLCF/Representable.thy src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML src/HOL/HOLCF/Tools/domaindef.ML src/HOL/HOLCF/ex/Domain_Proofs.thy

2010-12-19 huffman [Sun, 19 Dec 2010 10:33:46 -0800] rev 41291
add lemma u_map_oo
src/HOL/HOLCF/Map_Functions.thy

2010-12-19 huffman [Sun, 19 Dec 2010 09:52:33 -0800] rev 41290
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
src/HOL/HOLCF/Algebraic.thy src/HOL/HOLCF/Domain.thy src/HOL/HOLCF/Library/Defl_Bifinite.thy src/HOL/HOLCF/Powerdomains.thy src/HOL/HOLCF/Representable.thy src/HOL/HOLCF/Tools/domaindef.ML src/HOL/HOLCF/ex/Domain_Proofs.thy

2010-12-19 huffman [Sun, 19 Dec 2010 06:59:01 -0800] rev 41289
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
src/HOL/HOLCF/Compact_Basis.thy src/HOL/HOLCF/ConvexPD.thy src/HOL/HOLCF/LowerPD.thy src/HOL/HOLCF/Powerdomains.thy src/HOL/HOLCF/UpperPD.thy

2010-12-19 huffman [Sun, 19 Dec 2010 06:39:19 -0800] rev 41288
powerdomain theories require class 'bifinite' instead of 'domain'
src/HOL/HOLCF/Compact_Basis.thy src/HOL/HOLCF/ConvexPD.thy src/HOL/HOLCF/LowerPD.thy src/HOL/HOLCF/UpperPD.thy

2010-12-19 huffman [Sun, 19 Dec 2010 06:34:41 -0800] rev 41287
type 'defl' takes a type parameter again (cf. b525988432e9)
NEWS src/HOL/HOLCF/Algebraic.thy src/HOL/HOLCF/ConvexPD.thy src/HOL/HOLCF/Domain.thy src/HOL/HOLCF/Library/Defl_Bifinite.thy src/HOL/HOLCF/LowerPD.thy src/HOL/HOLCF/Representable.thy src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML src/HOL/HOLCF/Tools/domaindef.ML src/HOL/HOLCF/UpperPD.thy src/HOL/HOLCF/ex/Domain_Proofs.thy