2008-06-26 huffman [Thu, 26 Jun 2008 17:54:05 +0200] rev 27373
remove cset theory; define ideal completions using typedef instead of cpodef
src/HOLCF/CompactBasis.thy src/HOLCF/ConvexPD.thy src/HOLCF/LowerPD.thy src/HOLCF/UpperPD.thy

2008-06-26 wenzelm [Thu, 26 Jun 2008 15:06:30 +0200] rev 27372
Args.theory;
src/Tools/code/code_target.ML

2008-06-26 wenzelm [Thu, 26 Jun 2008 15:06:28 +0200] rev 27371
added context/theory scanner;
src/Pure/Isar/args.ML

2008-06-26 wenzelm [Thu, 26 Jun 2008 15:06:25 +0200] rev 27370
Args.context;
src/HOL/Nominal/nominal_induct.ML src/Pure/ML/ml_antiquote.ML src/Tools/induct.ML

2008-06-26 krauss [Thu, 26 Jun 2008 11:58:27 +0200] rev 27369
fix: need to beta/eta normalize
src/HOL/Tools/function_package/induction_scheme.ML

2008-06-26 haftmann [Thu, 26 Jun 2008 10:07:01 +0200] rev 27368
established Plain theory and image
src/HOL/ATP_Linkup.thy src/HOL/Complex/Complex_Main.thy src/HOL/Complex/ex/MIR.thy src/HOL/Complex/ex/ReflectedFerrack.thy src/HOL/Dense_Linear_Order.thy src/HOL/Hyperreal/Poly.thy src/HOL/IsaMakefile src/HOL/Library/Abstract_Rat.thy src/HOL/Library/AssocList.thy src/HOL/Library/BigO.thy src/HOL/Library/Binomial.thy src/HOL/Library/Boolean_Algebra.thy src/HOL/Library/Char_nat.thy src/HOL/Library/Char_ord.thy src/HOL/Library/Code_Char.thy src/HOL/Library/Code_Char_chr.thy src/HOL/Library/Code_Index.thy src/HOL/Library/Code_Integer.thy src/HOL/Library/Code_Message.thy src/HOL/Library/Coinductive_List.thy src/HOL/Library/Commutative_Ring.thy src/HOL/Library/Continuity.thy src/HOL/Library/Countable.thy src/HOL/Library/Dense_Linear_Order.thy src/HOL/Library/Efficient_Nat.thy src/HOL/Library/Enum.thy src/HOL/Library/Eval.thy src/HOL/Library/Eval_Witness.thy src/HOL/Library/Executable_Set.thy src/HOL/Library/FuncSet.thy src/HOL/Library/GCD.thy src/HOL/Library/Heap.thy src/HOL/Library/Infinite_Set.thy src/HOL/Library/LaTeXsugar.thy src/HOL/Library/Library.thy src/HOL/Library/ListVector.thy src/HOL/Library/List_Prefix.thy src/HOL/Library/List_lexord.thy src/HOL/Library/Multiset.thy src/HOL/Library/NatPair.thy src/HOL/Library/Nat_Infinity.thy src/HOL/Library/Nested_Environment.thy src/HOL/Library/Numeral_Type.thy src/HOL/Library/Option_ord.thy src/HOL/Library/Order_Relation.thy src/HOL/Library/Parity.thy src/HOL/Library/Permutation.thy src/HOL/Library/Pocklington.thy src/HOL/Library/Primes.thy src/HOL/Library/Product_ord.thy ...

2008-06-26 haftmann [Thu, 26 Jun 2008 10:06:54 +0200] rev 27367
added dummy citiation
src/HOL/Main.thy src/HOL/document/root.bib

2008-06-26 haftmann [Thu, 26 Jun 2008 10:06:53 +0200] rev 27366
dropped recdef
src/HOL/Isar_examples/Fibonacci.thy src/HOL/Real/Float.thy

2008-06-26 haftmann [Thu, 26 Jun 2008 10:06:51 +0200] rev 27365
class theory name lookup improved
src/Tools/code/code_name.ML

2008-06-25 wenzelm [Wed, 25 Jun 2008 22:11:17 +0200] rev 27364
modernized specifications;
src/HOL/IMPP/Hoare.thy