2014-11-02 wenzelm [Sun, 02 Nov 2014 18:21:14 +0100] rev 58888
prefer \setisabellecontext;
src/HOL/document/root.tex

2014-11-02 wenzelm [Sun, 02 Nov 2014 18:16:19 +0100] rev 58887
modernized header;
src/HOL/Bali/AxCompl.thy src/HOL/Bali/AxExample.thy src/HOL/Bali/AxSem.thy src/HOL/Bali/AxSound.thy src/HOL/Bali/Basis.thy src/HOL/Bali/Conform.thy src/HOL/Bali/Decl.thy src/HOL/Bali/DeclConcepts.thy src/HOL/Bali/DefiniteAssignment.thy src/HOL/Bali/DefiniteAssignmentCorrect.thy src/HOL/Bali/Eval.thy src/HOL/Bali/Evaln.thy src/HOL/Bali/Example.thy src/HOL/Bali/Name.thy src/HOL/Bali/State.thy src/HOL/Bali/Table.thy src/HOL/Bali/Term.thy src/HOL/Bali/Type.thy src/HOL/Bali/TypeRel.thy src/HOL/Bali/TypeSafe.thy src/HOL/Bali/Value.thy src/HOL/Bali/WellForm.thy src/HOL/Bali/WellType.thy src/HOL/Bali/document/root.tex

2014-11-02 wenzelm [Sun, 02 Nov 2014 17:58:35 +0100] rev 58886
modernized header;
src/HOL/MicroJava/BV/Altern.thy src/HOL/MicroJava/BV/BVExample.thy src/HOL/MicroJava/BV/BVNoTypeError.thy src/HOL/MicroJava/BV/BVSpec.thy src/HOL/MicroJava/BV/BVSpecTypeSafe.thy src/HOL/MicroJava/BV/Correct.thy src/HOL/MicroJava/BV/Effect.thy src/HOL/MicroJava/BV/EffectMono.thy src/HOL/MicroJava/BV/JType.thy src/HOL/MicroJava/BV/JVM.thy src/HOL/MicroJava/BV/JVMType.thy src/HOL/MicroJava/BV/LBVJVM.thy src/HOL/MicroJava/BV/Typing_Framework_JVM.thy src/HOL/MicroJava/Comp/CorrCompTp.thy src/HOL/MicroJava/DFA/Abstract_BV.thy src/HOL/MicroJava/DFA/Err.thy src/HOL/MicroJava/DFA/Kildall.thy src/HOL/MicroJava/DFA/LBVComplete.thy src/HOL/MicroJava/DFA/LBVCorrect.thy src/HOL/MicroJava/DFA/LBVSpec.thy src/HOL/MicroJava/DFA/Listn.thy src/HOL/MicroJava/DFA/Opt.thy src/HOL/MicroJava/DFA/Product.thy src/HOL/MicroJava/DFA/Semilat.thy src/HOL/MicroJava/DFA/SemilatAlg.thy src/HOL/MicroJava/DFA/Semilattices.thy src/HOL/MicroJava/DFA/Typing_Framework.thy src/HOL/MicroJava/DFA/Typing_Framework_err.thy src/HOL/MicroJava/J/Conform.thy src/HOL/MicroJava/J/Decl.thy src/HOL/MicroJava/J/Eval.thy src/HOL/MicroJava/J/Example.thy src/HOL/MicroJava/J/JBasis.thy src/HOL/MicroJava/J/JListExample.thy src/HOL/MicroJava/J/JTypeSafe.thy src/HOL/MicroJava/J/State.thy src/HOL/MicroJava/J/SystemClasses.thy src/HOL/MicroJava/J/Term.thy src/HOL/MicroJava/J/Type.thy src/HOL/MicroJava/J/TypeRel.thy src/HOL/MicroJava/J/Value.thy src/HOL/MicroJava/J/WellForm.thy src/HOL/MicroJava/J/WellType.thy src/HOL/MicroJava/JVM/JVMDefensive.thy src/HOL/MicroJava/JVM/JVMExceptions.thy src/HOL/MicroJava/JVM/JVMExec.thy src/HOL/MicroJava/JVM/JVMExecInstr.thy src/HOL/MicroJava/JVM/JVMInstructions.thy src/HOL/MicroJava/JVM/JVMListExample.thy src/HOL/MicroJava/JVM/JVMState.thy ...

2014-11-02 wenzelm [Sun, 02 Nov 2014 17:39:52 +0100] rev 58885
obsolete;
src/Doc/Prog_Prove/document/prelude.tex

2014-11-02 wenzelm [Sun, 02 Nov 2014 17:36:52 +0100] rev 58884
modernized header;
src/HOL/Hoare_Parallel/Gar_Coll.thy src/HOL/Hoare_Parallel/Graph.thy src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy src/HOL/Hoare_Parallel/OG_Com.thy src/HOL/Hoare_Parallel/OG_Examples.thy src/HOL/Hoare_Parallel/OG_Hoare.thy src/HOL/Hoare_Parallel/OG_Tactics.thy src/HOL/Hoare_Parallel/OG_Tran.thy src/HOL/Hoare_Parallel/Quote_Antiquote.thy src/HOL/Hoare_Parallel/RG_Com.thy src/HOL/Hoare_Parallel/RG_Examples.thy src/HOL/Hoare_Parallel/RG_Hoare.thy src/HOL/Hoare_Parallel/RG_Syntax.thy src/HOL/Hoare_Parallel/RG_Tran.thy src/HOL/Hoare_Parallel/document/root.tex

2014-11-02 wenzelm [Sun, 02 Nov 2014 17:27:22 +0100] rev 58883
obsolete;
src/HOL/Hoare/document/root.tex

2014-11-02 wenzelm [Sun, 02 Nov 2014 17:23:48 +0100] rev 58882
modernized header;
src/HOL/Isar_Examples/Basic_Logic.thy src/HOL/Isar_Examples/Cantor.thy src/HOL/Isar_Examples/Drinker.thy src/HOL/Isar_Examples/Expr_Compiler.thy src/HOL/Isar_Examples/Fibonacci.thy src/HOL/Isar_Examples/Group.thy src/HOL/Isar_Examples/Group_Context.thy src/HOL/Isar_Examples/Group_Notepad.thy src/HOL/Isar_Examples/Hoare.thy src/HOL/Isar_Examples/Hoare_Ex.thy src/HOL/Isar_Examples/Knaster_Tarski.thy src/HOL/Isar_Examples/Mutilated_Checkerboard.thy src/HOL/Isar_Examples/Nested_Datatype.thy src/HOL/Isar_Examples/Peirce.thy src/HOL/Isar_Examples/Puzzle.thy src/HOL/Isar_Examples/Summation.thy src/HOL/Isar_Examples/document/style.tex

2014-11-02 wenzelm [Sun, 02 Nov 2014 17:20:45 +0100] rev 58881
modernized header;
src/HOL/Library/AList.thy src/HOL/Library/AList_Mapping.thy src/HOL/Library/BNF_Axiomatization.thy src/HOL/Library/BigO.thy src/HOL/Library/Bit.thy src/HOL/Library/Boolean_Algebra.thy src/HOL/Library/Cardinal_Notations.thy src/HOL/Library/Cardinality.thy src/HOL/Library/Char_ord.thy src/HOL/Library/Code_Abstract_Nat.thy src/HOL/Library/Code_Binary_Nat.thy src/HOL/Library/Code_Char.thy src/HOL/Library/Code_Prolog.thy src/HOL/Library/Code_Target_Int.thy src/HOL/Library/Code_Target_Nat.thy src/HOL/Library/Code_Target_Numeral.thy src/HOL/Library/ContNotDenum.thy src/HOL/Library/Convex.thy src/HOL/Library/Countable.thy src/HOL/Library/Countable_Set.thy src/HOL/Library/Countable_Set_Type.thy src/HOL/Library/DAList.thy src/HOL/Library/DAList_Multiset.thy src/HOL/Library/Debug.thy src/HOL/Library/Diagonal_Subsequence.thy src/HOL/Library/Discrete.thy src/HOL/Library/Dlist.thy src/HOL/Library/Extended_Nat.thy src/HOL/Library/Extended_Real.thy src/HOL/Library/FSet.thy src/HOL/Library/FinFun.thy src/HOL/Library/FinFun_Syntax.thy src/HOL/Library/Float.thy src/HOL/Library/Formal_Power_Series.thy src/HOL/Library/Fraction_Field.thy src/HOL/Library/Fun_Lexorder.thy src/HOL/Library/FuncSet.thy src/HOL/Library/Function_Algebras.thy src/HOL/Library/Function_Division.thy src/HOL/Library/Function_Growth.thy src/HOL/Library/Fundamental_Theorem_Algebra.thy src/HOL/Library/Groups_Big_Fun.thy src/HOL/Library/IArray.thy src/HOL/Library/Indicator_Function.thy src/HOL/Library/Infinite_Set.thy src/HOL/Library/Inner_Product.thy src/HOL/Library/Lattice_Algebras.thy src/HOL/Library/Lattice_Syntax.thy src/HOL/Library/Liminf_Limsup.thy src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy ...

2014-11-02 wenzelm [Sun, 02 Nov 2014 17:16:01 +0100] rev 58880
modernized header;
src/HOL/HOLCF/Adm.thy src/HOL/HOLCF/Algebraic.thy src/HOL/HOLCF/Bifinite.thy src/HOL/HOLCF/Cfun.thy src/HOL/HOLCF/Compact_Basis.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_adm.thy src/HOL/HOLCF/FOCUS/FOCUS.thy src/HOL/HOLCF/FOCUS/Fstream.thy 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/IMP/Denotational.thy src/HOL/HOLCF/IMP/HoareEx.thy 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/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/Packet.thy 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 src/HOL/HOLCF/IOA/NTP/Impl.thy src/HOL/HOLCF/IOA/NTP/Multiset.thy src/HOL/HOLCF/IOA/NTP/Receiver.thy src/HOL/HOLCF/IOA/NTP/Sender.thy src/HOL/HOLCF/IOA/NTP/Spec.thy src/HOL/HOLCF/IOA/Storage/Action.thy src/HOL/HOLCF/IOA/Storage/Correctness.thy src/HOL/HOLCF/IOA/Storage/Impl.thy src/HOL/HOLCF/IOA/Storage/Spec.thy src/HOL/HOLCF/IOA/ex/TrivEx.thy src/HOL/HOLCF/IOA/ex/TrivEx2.thy src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy src/HOL/HOLCF/IOA/meta_theory/Asig.thy ...

2014-11-02 wenzelm [Sun, 02 Nov 2014 17:14:15 +0100] rev 58879
modernized header;
src/HOL/Lattice/Bounds.thy src/HOL/Lattice/CompleteLattice.thy src/HOL/Lattice/Lattice.thy src/HOL/Lattice/Orders.thy src/HOL/Lattice/document/root.tex