2009-06-23 haftmann [Tue, 23 Jun 2009 14:50:34 +0200] rev 31781
add_datatype interface yields type names and less rules
src/HOL/Nominal/nominal.ML src/HOL/Nominal/nominal_atoms.ML src/HOL/Tools/Datatype/datatype.ML src/HOL/Tools/inductive_realizer.ML

2009-06-23 wenzelm [Tue, 23 Jun 2009 21:05:51 +0200] rev 31780
non-public representation;
src/Pure/Thy/completion.scala

2009-06-23 wenzelm [Tue, 23 Jun 2009 21:00:18 +0200] rev 31779
fixed abbrev !! for \<And>;
etc/symbols

2009-06-23 wenzelm [Tue, 23 Jun 2009 20:14:40 +0200] rev 31778
merged

2009-06-23 haftmann [Tue, 23 Jun 2009 14:33:35 +0200] rev 31777
merged
src/HOL/Tools/datatype_package/datatype.ML src/HOL/Tools/datatype_package/datatype_abs_proofs.ML src/HOL/Tools/datatype_package/datatype_aux.ML src/HOL/Tools/datatype_package/datatype_case.ML src/HOL/Tools/datatype_package/datatype_codegen.ML src/HOL/Tools/datatype_package/datatype_prop.ML src/HOL/Tools/datatype_package/datatype_realizer.ML src/HOL/Tools/datatype_package/datatype_rep_proofs.ML src/HOL/Tools/function_package/auto_term.ML src/HOL/Tools/function_package/context_tree.ML src/HOL/Tools/function_package/decompose.ML src/HOL/Tools/function_package/descent.ML src/HOL/Tools/function_package/fundef.ML src/HOL/Tools/function_package/fundef_common.ML src/HOL/Tools/function_package/fundef_core.ML src/HOL/Tools/function_package/fundef_datatype.ML src/HOL/Tools/function_package/fundef_lib.ML src/HOL/Tools/function_package/induction_scheme.ML src/HOL/Tools/function_package/inductive_wrap.ML src/HOL/Tools/function_package/lexicographic_order.ML src/HOL/Tools/function_package/measure_functions.ML src/HOL/Tools/function_package/mutual.ML src/HOL/Tools/function_package/pattern_split.ML src/HOL/Tools/function_package/scnp_reconstruct.ML src/HOL/Tools/function_package/scnp_solve.ML src/HOL/Tools/function_package/size.ML src/HOL/Tools/function_package/sum_tree.ML src/HOL/Tools/function_package/termination.ML src/HOLCF/IOA/meta_theory/ioa.ML src/Tools/code/code_haskell.ML src/Tools/code/code_ml.ML src/Tools/code/code_preproc.ML src/Tools/code/code_printer.ML src/Tools/code/code_target.ML src/Tools/code/code_thingol.ML

2009-06-23 haftmann [Tue, 23 Jun 2009 14:24:58 +0200] rev 31776
simplified proof
src/HOL/Library/Formal_Power_Series.thy

2009-06-23 haftmann [Tue, 23 Jun 2009 12:09:30 +0200] rev 31775
uniformly capitialized names for subdirectories
src/HOL/Fun.thy src/HOL/FunDef.thy src/HOL/Inductive.thy src/HOL/Product_Type.thy src/HOL/Tools/Datatype/datatype.ML src/HOL/Tools/Datatype/datatype_abs_proofs.ML src/HOL/Tools/Datatype/datatype_aux.ML src/HOL/Tools/Datatype/datatype_case.ML src/HOL/Tools/Datatype/datatype_codegen.ML src/HOL/Tools/Datatype/datatype_prop.ML src/HOL/Tools/Datatype/datatype_realizer.ML src/HOL/Tools/Datatype/datatype_rep_proofs.ML src/HOL/Tools/Function/auto_term.ML src/HOL/Tools/Function/context_tree.ML src/HOL/Tools/Function/decompose.ML src/HOL/Tools/Function/descent.ML src/HOL/Tools/Function/fundef.ML src/HOL/Tools/Function/fundef_common.ML src/HOL/Tools/Function/fundef_core.ML src/HOL/Tools/Function/fundef_datatype.ML src/HOL/Tools/Function/fundef_lib.ML src/HOL/Tools/Function/induction_scheme.ML src/HOL/Tools/Function/inductive_wrap.ML src/HOL/Tools/Function/lexicographic_order.ML src/HOL/Tools/Function/measure_functions.ML src/HOL/Tools/Function/mutual.ML src/HOL/Tools/Function/pattern_split.ML src/HOL/Tools/Function/scnp_reconstruct.ML src/HOL/Tools/Function/scnp_solve.ML src/HOL/Tools/Function/size.ML src/HOL/Tools/Function/sum_tree.ML src/HOL/Tools/Function/termination.ML src/HOL/Tools/datatype_package/datatype.ML src/HOL/Tools/datatype_package/datatype_abs_proofs.ML src/HOL/Tools/datatype_package/datatype_aux.ML src/HOL/Tools/datatype_package/datatype_case.ML src/HOL/Tools/datatype_package/datatype_codegen.ML src/HOL/Tools/datatype_package/datatype_prop.ML src/HOL/Tools/datatype_package/datatype_realizer.ML src/HOL/Tools/datatype_package/datatype_rep_proofs.ML src/HOL/Tools/function_package/auto_term.ML src/HOL/Tools/function_package/context_tree.ML src/HOL/Tools/function_package/decompose.ML src/HOL/Tools/function_package/descent.ML src/HOL/Tools/function_package/fundef.ML src/HOL/Tools/function_package/fundef_common.ML src/HOL/Tools/function_package/fundef_core.ML src/HOL/Tools/function_package/fundef_datatype.ML src/HOL/Tools/function_package/fundef_lib.ML src/HOL/Tools/function_package/induction_scheme.ML ...

2009-06-23 haftmann [Tue, 23 Jun 2009 12:09:14 +0200] rev 31774
renamed ioa to automaton
src/HOLCF/IOA/meta_theory/automaton.ML src/HOLCF/IOA/meta_theory/ioa.ML

2009-06-23 haftmann [Tue, 23 Jun 2009 12:08:35 +0200] rev 31773
renamed ioa to automaton
src/HOLCF/IOA/meta_theory/Abstraction.thy src/HOLCF/IsaMakefile

2009-06-23 haftmann [Tue, 23 Jun 2009 12:08:34 +0200] rev 31772
dropped duplicated lemmas, tuned header
src/HOL/NewNumberTheory/MiscAlgebra.thy