2010-11-27 huffman [Sat, 27 Nov 2010 17:14:29 -0800] rev 40775
remove HOLCF from build script, since it no longer works
build

2010-11-27 huffman [Sat, 27 Nov 2010 16:08:10 -0800] rev 40774
moved directory src/HOLCF to src/HOL/HOLCF;
added HOLCF theories to src/HOL/IsaMakefile;
src/HOL/HOLCF/Adm.thy src/HOL/HOLCF/Algebraic.thy src/HOL/HOLCF/Bifinite.thy src/HOL/HOLCF/Cfun.thy src/HOL/HOLCF/CompactBasis.thy src/HOL/HOLCF/Completion.thy src/HOL/HOLCF/Cont.thy src/HOL/HOLCF/ConvexPD.thy src/HOL/HOLCF/Cpodef.thy src/HOL/HOLCF/Cprod.thy src/HOL/HOLCF/Deflation.thy src/HOL/HOLCF/Discrete.thy src/HOL/HOLCF/Domain.thy src/HOL/HOLCF/Domain_Aux.thy src/HOL/HOLCF/FOCUS/Buffer.thy src/HOL/HOLCF/FOCUS/Buffer_adm.thy src/HOL/HOLCF/FOCUS/FOCUS.thy src/HOL/HOLCF/FOCUS/Fstream.thy src/HOL/HOLCF/FOCUS/Fstreams.thy src/HOL/HOLCF/FOCUS/README.html src/HOL/HOLCF/FOCUS/ROOT.ML src/HOL/HOLCF/FOCUS/Stream_adm.thy src/HOL/HOLCF/Fix.thy src/HOL/HOLCF/Fixrec.thy src/HOL/HOLCF/Fun_Cpo.thy src/HOL/HOLCF/HOLCF.thy src/HOL/HOLCF/IMP/Denotational.thy src/HOL/HOLCF/IMP/HoareEx.thy src/HOL/HOLCF/IMP/README.html src/HOL/HOLCF/IMP/ROOT.ML src/HOL/HOLCF/IMP/document/root.bib src/HOL/HOLCF/IMP/document/root.tex src/HOL/HOLCF/IOA/ABP/Abschannel.thy src/HOL/HOLCF/IOA/ABP/Abschannel_finite.thy src/HOL/HOLCF/IOA/ABP/Action.thy src/HOL/HOLCF/IOA/ABP/Check.ML src/HOL/HOLCF/IOA/ABP/Correctness.thy src/HOL/HOLCF/IOA/ABP/Env.thy src/HOL/HOLCF/IOA/ABP/Impl.thy src/HOL/HOLCF/IOA/ABP/Impl_finite.thy src/HOL/HOLCF/IOA/ABP/Lemmas.thy src/HOL/HOLCF/IOA/ABP/Packet.thy src/HOL/HOLCF/IOA/ABP/ROOT.ML src/HOL/HOLCF/IOA/ABP/Read_me src/HOL/HOLCF/IOA/ABP/Receiver.thy src/HOL/HOLCF/IOA/ABP/Sender.thy src/HOL/HOLCF/IOA/ABP/Spec.thy src/HOL/HOLCF/IOA/NTP/Abschannel.thy src/HOL/HOLCF/IOA/NTP/Action.thy src/HOL/HOLCF/IOA/NTP/Correctness.thy ...

2010-11-27 huffman [Sat, 27 Nov 2010 14:34:54 -0800] rev 40773
merged
src/Pure/ML-Systems/bash.ML

2010-11-27 huffman [Sat, 27 Nov 2010 14:09:03 -0800] rev 40772
rename Pcpodef.thy to Cpodef.thy;
rename pcpodef.ML to cpodef.ML;
src/HOLCF/Cfun.thy src/HOLCF/Cpodef.thy src/HOLCF/IsaMakefile src/HOLCF/Pcpodef.thy src/HOLCF/Tools/cpodef.ML src/HOLCF/Tools/domaindef.ML src/HOLCF/Tools/pcpodef.ML

2010-11-27 huffman [Sat, 27 Nov 2010 13:12:10 -0800] rev 40771
renamed several HOLCF theorems (listed in NEWS)
NEWS src/HOLCF/Bifinite.thy src/HOLCF/Cfun.thy src/HOLCF/Completion.thy src/HOLCF/Cont.thy src/HOLCF/FOCUS/Fstream.thy src/HOLCF/FOCUS/Fstreams.thy src/HOLCF/FOCUS/Stream_adm.thy src/HOLCF/Fix.thy src/HOLCF/Fun_Cpo.thy src/HOLCF/HOLCF.thy src/HOLCF/Library/List_Cpo.thy src/HOLCF/Library/Sum_Cpo.thy src/HOLCF/Pcpo.thy src/HOLCF/Pcpodef.thy src/HOLCF/Porder.thy src/HOLCF/Product_Cpo.thy src/HOLCF/Tools/Domain/domain_isomorphism.ML src/HOLCF/Up.thy src/HOLCF/ex/Domain_Proofs.thy

2010-11-27 huffman [Sat, 27 Nov 2010 12:55:12 -0800] rev 40770
rename cpodef theorems: lub_foo -> is_lub_foo, thelub_foo -> lub_foo
src/HOLCF/Cfun.thy src/HOLCF/Pcpodef.thy src/HOLCF/Tools/pcpodef.ML

2010-11-27 huffman [Sat, 27 Nov 2010 12:38:02 -0800] rev 40769
rename rep_contlub lemmas to rep_lub
src/HOLCF/Completion.thy

2010-11-27 huffman [Sat, 27 Nov 2010 12:27:57 -0800] rev 40768
rename function 'match_UU' to 'match_bottom'
src/HOLCF/Fixrec.thy

2010-11-27 huffman [Sat, 27 Nov 2010 12:26:18 -0800] rev 40767
rename function 'strict' to 'seq', which is its name in Haskell
src/HOLCF/Cfun.thy src/HOLCF/Fixrec.thy src/HOLCF/One.thy src/HOLCF/Sprod.thy src/HOLCF/Ssum.thy

2010-11-27 haftmann [Sat, 27 Nov 2010 22:02:16 +0100] rev 40766
merged