2002-08-21 paulson [Wed, 21 Aug 2002 15:57:08 +0200] rev 13512
tweaks and new lemmas
src/ZF/OrderArith.thy

2002-08-21 paulson [Wed, 21 Aug 2002 15:56:37 +0200] rev 13511
new proof needed now
src/ZF/Constructible/Formula.thy

2002-08-21 paulson [Wed, 21 Aug 2002 15:55:59 +0200] rev 13510
proof can be shortened now
src/ZF/UNITY/GenPrefix.ML

2002-08-21 paulson [Wed, 21 Aug 2002 15:55:40 +0200] rev 13509
new lemmas
src/ZF/List.thy

2002-08-21 paulson [Wed, 21 Aug 2002 15:53:30 +0200] rev 13508
Frederic Blanqui's new "guard" examples
src/HOL/Auth/Guard/Analz.thy src/HOL/Auth/Guard/Extensions.thy src/HOL/Auth/Guard/Guard.thy src/HOL/Auth/Guard/GuardK.thy src/HOL/Auth/Guard/Guard_Public.thy src/HOL/Auth/Guard/Guard_Shared.thy src/HOL/Auth/Guard/List_Msg.thy src/HOL/Auth/Guard/NS_Public.thy src/HOL/Auth/Guard/OtwayRees.thy src/HOL/Auth/Guard/P1.thy src/HOL/Auth/Guard/P2.thy src/HOL/Auth/Guard/Proto.thy src/HOL/Auth/Guard/README.html src/HOL/Auth/Guard/Yahalom.thy src/HOL/Auth/README.html src/HOL/Auth/ROOT.ML src/HOL/IsaMakefile src/HOL/List.thy

2002-08-17 paulson [Sat, 17 Aug 2002 14:55:08 +0200] rev 13507
tidying of Isar scripts
src/HOL/Auth/KerberosIV.thy src/HOL/Auth/Kerberos_BAN.thy src/HOL/Auth/NS_Public.thy src/HOL/Auth/NS_Public_Bad.thy src/HOL/Auth/NS_Shared.thy src/HOL/Auth/OtwayRees.thy src/HOL/Auth/OtwayRees_AN.thy src/HOL/Auth/OtwayRees_Bad.thy src/HOL/Auth/Recur.thy src/HOL/Auth/Shared.thy src/HOL/Auth/TLS.thy src/HOL/Auth/WooLam.thy src/HOL/Auth/Yahalom.thy src/HOL/Auth/Yahalom2.thy src/HOL/Auth/Yahalom_Bad.thy

2002-08-16 paulson [Fri, 16 Aug 2002 17:19:43 +0200] rev 13506
Various tweaks of the presentation
src/ZF/Constructible/Internalize.thy src/ZF/Constructible/L_axioms.thy src/ZF/Constructible/Rec_Separation.thy src/ZF/Constructible/WF_absolute.thy src/ZF/Constructible/WFrec.thy

2002-08-16 paulson [Fri, 16 Aug 2002 16:41:48 +0200] rev 13505
Relativized right up to L satisfies V=L!
src/ZF/Constructible/DPow_absolute.thy src/ZF/Constructible/Datatype_absolute.thy src/ZF/Constructible/Formula.thy src/ZF/Constructible/Internalize.thy src/ZF/Constructible/L_axioms.thy src/ZF/Constructible/MetaExists.thy src/ZF/Constructible/Normal.thy src/ZF/Constructible/Rec_Separation.thy src/ZF/Constructible/Reflection.thy src/ZF/Constructible/Relative.thy src/ZF/Constructible/Satisfies_absolute.thy src/ZF/Constructible/Separation.thy src/ZF/Constructible/WF_absolute.thy src/ZF/Constructible/WFrec.thy src/ZF/Constructible/Wellorderings.thy

2002-08-16 paulson [Fri, 16 Aug 2002 12:48:49 +0200] rev 13504
Tidying up
src/ZF/Constructible/DPow_absolute.thy src/ZF/Constructible/Satisfies_absolute.thy

2002-08-15 paulson [Thu, 15 Aug 2002 21:36:26 +0200] rev 13503
Relativization and absoluteness for DPow!!
src/ZF/Constructible/DPow_absolute.thy src/ZF/Constructible/Internalize.thy src/ZF/Constructible/ROOT.ML src/ZF/Constructible/Rec_Separation.thy src/ZF/Constructible/Satisfies_absolute.thy src/ZF/IsaMakefile