2007-08-24 haftmann [Fri, 24 Aug 2007 14:14:20 +0200] rev 24423
overloaded definitions accompanied by explicit constants
src/HOL/Complex/ex/ReflectedFerrack.thy src/HOL/Complex/ex/linreif.ML src/HOL/Complex/ex/mireif.ML src/HOL/Lambda/WeakNorm.thy src/HOL/Library/Efficient_Nat.thy src/HOL/Library/Eval.thy src/HOL/Library/Executable_Set.thy src/HOL/Library/Graphs.thy src/HOL/Library/ML_Int.thy src/HOL/Library/Pretty_Int.thy src/HOL/Library/SCT_Implementation.thy src/HOL/Tools/datatype_abs_proofs.ML src/HOL/Tools/datatype_codegen.ML src/HOL/Tools/datatype_package.ML src/HOL/ex/Classpackage.thy src/HOL/ex/Codegenerator.thy src/HOL/ex/Eval_Examples.thy src/HOL/ex/ExecutableContent.thy src/HOL/ex/coopereif.ML src/Pure/Isar/ROOT.ML src/Pure/Isar/class.ML src/Pure/Isar/code.ML src/Pure/Isar/code_unit.ML src/Pure/Isar/isar_syn.ML src/Tools/code/code_funcgr.ML src/Tools/code/code_name.ML src/Tools/code/code_package.ML src/Tools/code/code_target.ML src/Tools/nbe.ML

2007-08-24 haftmann [Fri, 24 Aug 2007 14:14:18 +0200] rev 24422
moved class dense_linear_order to Orderings.thy
NEWS src/HOL/Dense_Linear_Order.thy src/HOL/Orderings.thy src/HOL/Real/PReal.thy src/HOL/Ring_and_Field.thy

2007-08-24 haftmann [Fri, 24 Aug 2007 14:14:17 +0200] rev 24421
updated
doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs doc-src/IsarAdvanced/Codegen/Thy/examples/bool_infix.ML doc-src/IsarAdvanced/Codegen/Thy/examples/bool_literal.ML doc-src/IsarAdvanced/Codegen/Thy/examples/bool_mlbool.ML doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML doc-src/IsarAdvanced/Codegen/Thy/examples/class.ocaml doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML doc-src/IsarAdvanced/Codegen/Thy/examples/fac.ML doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML doc-src/IsarAdvanced/Codegen/Thy/examples/pick2.ML doc-src/IsarAdvanced/Codegen/Thy/examples/set_list.ML doc-src/IsarAdvanced/Codegen/Thy/examples/tree.ML

2007-08-24 haftmann [Fri, 24 Aug 2007 14:14:16 +0200] rev 24420
made sets executable
src/HOL/Set.thy

2007-08-24 huffman [Fri, 24 Aug 2007 00:37:12 +0200] rev 24419
remove unused lemmas
src/HOL/Word/BinGeneral.thy

2007-08-24 huffman [Fri, 24 Aug 2007 00:23:51 +0200] rev 24418
bin_sc_nth proof
src/HOL/Word/BinOperations.thy

2007-08-23 huffman [Thu, 23 Aug 2007 23:37:51 +0200] rev 24417
remove lemma bin_rec_PM
src/HOL/Word/BinGeneral.thy

2007-08-23 huffman [Thu, 23 Aug 2007 23:34:51 +0200] rev 24416
avoid use of bin_rec_PM
src/HOL/Word/BinOperations.thy

2007-08-23 huffman [Thu, 23 Aug 2007 20:15:45 +0200] rev 24415
new instance proofs
src/HOL/Word/WordArith.thy src/HOL/Word/WordDefinition.thy

2007-08-23 huffman [Thu, 23 Aug 2007 18:53:53 +0200] rev 24414
remove unused lemmas
src/HOL/Word/Num_Lemmas.thy