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

2002-08-14 paulson [Wed, 14 Aug 2002 14:33:26 +0200] rev 13502
Finished absoluteness of "satisfies"!!
src/ZF/Constructible/Satisfies_absolute.thy

2002-08-13 nipkow [Tue, 13 Aug 2002 22:01:53 +0200] rev 13501
arith_tac should not produce counter example
TFL/post.ML

2002-08-13 nipkow [Tue, 13 Aug 2002 21:59:44 +0200] rev 13500
*** empty log message ***
NEWS

2002-08-13 nipkow [Tue, 13 Aug 2002 21:57:15 +0200] rev 13499
Counter example generation mods.
src/HOL/Integ/int_arith1.ML src/HOL/NatArith.thy src/HOL/arith_data.ML

2002-08-13 nipkow [Tue, 13 Aug 2002 21:55:58 +0200] rev 13498
Added counter example generation.
src/Provers/Arith/fast_lin_arith.ML