2010-02-11 wenzelm [Thu, 11 Feb 2010 21:33:25 +0100] rev 35109
modernized syntax/translations;
doc-src/TutorialI/Protocol/Message.thy src/HOL/Auth/Message.thy src/HOL/Metis_Examples/Message.thy src/HOL/MicroJava/DFA/Product.thy src/HOL/MicroJava/DFA/Semilat.thy src/HOL/MicroJava/DFA/SemilatAlg.thy src/HOL/Modelcheck/MuckeSyn.thy src/HOL/Prolog/Test.thy

2010-02-11 wenzelm [Thu, 11 Feb 2010 21:31:50 +0100] rev 35108
modernized syntax/translations;
tuned headers;
src/HOL/TLA/Action.thy src/HOL/TLA/Init.thy src/HOL/TLA/Intensional.thy src/HOL/TLA/ROOT.ML src/HOL/TLA/Stfun.thy src/HOL/TLA/TLA.thy

2010-02-11 wenzelm [Thu, 11 Feb 2010 13:54:53 +0100] rev 35107
modernized translations;
src/HOL/Hoare_Parallel/OG_Syntax.thy src/HOL/Hoare_Parallel/OG_Tran.thy src/HOL/Hoare_Parallel/Quote_Antiquote.thy src/HOL/Hoare_Parallel/RG_Syntax.thy

2010-02-11 boehmes [Thu, 11 Feb 2010 09:14:34 +0100] rev 35106
merged

2010-02-11 boehmes [Thu, 11 Feb 2010 09:14:08 +0100] rev 35105
use full paths when importing theories
src/HOL/Boogie/Boogie.thy src/HOL/SMT/SMT_Base.thy

2010-02-11 nipkow [Thu, 11 Feb 2010 08:44:41 +0100] rev 35104
merged

2010-02-11 nipkow [Thu, 11 Feb 2010 08:44:19 +0100] rev 35103
inductive vs inductive_set explanation
doc-src/TutorialI/Inductive/Mutual.thy doc-src/TutorialI/Inductive/document/Mutual.tex doc-src/TutorialI/Types/document/Numbers.tex

2010-02-11 wenzelm [Thu, 11 Feb 2010 00:45:02 +0100] rev 35102
modernized translations;
src/HOL/MicroJava/BV/BVExample.thy src/HOL/MicroJava/BV/JType.thy src/HOL/MicroJava/Comp/CorrCompTp.thy src/HOL/MicroJava/Comp/LemmasComp.thy src/HOL/MicroJava/Comp/TranslCompTp.thy src/HOL/MicroJava/DFA/Err.thy src/HOL/MicroJava/DFA/Listn.thy src/HOL/MicroJava/J/Example.thy src/HOL/MicroJava/J/Exceptions.thy src/HOL/MicroJava/J/State.thy src/HOL/MicroJava/J/Type.thy src/HOL/MicroJava/J/WellType.thy src/HOL/MicroJava/JVM/JVMDefensive.thy src/HOL/MicroJava/JVM/JVMExceptions.thy src/HOL/NanoJava/Example.thy src/HOL/NanoJava/TypeRel.thy

2010-02-10 wenzelm [Wed, 10 Feb 2010 23:53:46 +0100] rev 35101
modernized translations;
src/HOL/Hoare/HeapSyntax.thy src/HOL/Hoare/HeapSyntaxAbort.thy src/HOL/Hoare/HoareAbort.thy src/HOL/Hoare/Pointers0.thy src/HOL/Hoare/Separation.thy src/HOL/SET_Protocol/Event_SET.thy

2010-02-10 wenzelm [Wed, 10 Feb 2010 19:37:34 +0100] rev 35100
renamed Library/Quotient.thy to Library/Quotient_Type.thy to avoid clash with new theory Quotient in Main HOL;
NEWS src/HOL/IsaMakefile src/HOL/Library/Library.thy src/HOL/Library/Quotient.thy src/HOL/Library/Quotient_Type.thy