Changes

Summary

prefer formal comments;
prefer formal text;
prefer formal comments;
prefer formal comments;
isabelle update_cartouches -c;

Changeset 67410:64d928bacddd by wenzelm: prefer formal comments;
The file was modified	`src/HOL/Hoare/Examples.thy` (diff)
The file was modified	`src/HOL/Hoare/Hoare_Logic_Abort.thy` (diff)
The file was modified	`src/HOL/Hoare/SchorrWaite.thy` (diff)
The file was modified	`src/HOL/Hoare/Separation.thy` (diff)
Changeset 67409:060efe532189 by wenzelm: prefer formal text;
The file was modified	`src/HOL/Library/Going_To_Filter.thy` (diff)
Changeset 67408:4a4c14b24800 by wenzelm: prefer formal comments;
The file was modified	`src/HOL/Library/Bourbaki_Witt_Fixpoint.thy` (diff)
The file was modified	`src/HOL/Library/DAList_Multiset.thy` (diff)
The file was modified	`src/HOL/Library/Extended_Nonnegative_Real.thy` (diff)
The file was modified	`src/HOL/Library/Extended_Real.thy` (diff)
The file was modified	`src/HOL/Library/FSet.thy` (diff)
The file was modified	`src/HOL/Library/Infinite_Set.thy` (diff)
The file was modified	`src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy` (diff)
The file was modified	`src/HOL/Library/Permutations.thy` (diff)
The file was modified	`src/HOL/Library/RBT_Impl.thy` (diff)
The file was modified	`src/HOL/Library/RBT_Set.thy` (diff)
The file was modified	`src/HOL/Library/Stream.thy` (diff)
The file was modified	`src/HOL/Word/Bits_Int.thy` (diff)
The file was modified	`src/HOL/Word/Bool_List_Representation.thy` (diff)
The file was modified	`src/HOL/Word/Misc_Typedef.thy` (diff)
The file was modified	`src/HOL/Word/Word.thy` (diff)
The file was modified	`src/HOL/Word/Word_Miscellaneous.thy` (diff)
Changeset 67407:dbaa38bd223a by wenzelm: prefer formal comments;
The file was modified	`src/HOL/SPARK/Examples/RIPEMD-160/RMD.thy` (diff)
The file was modified	`src/HOL/SPARK/Examples/RIPEMD-160/RMD_Specification.thy` (diff)
The file was modified	`src/HOL/SPARK/Examples/RIPEMD-160/Round.thy` (diff)
Changeset 67406:23307fd33906 by wenzelm: isabelle update_cartouches -c;
The file was modified	`src/Doc/Classes/Classes.thy` (diff)
The file was modified	`src/Doc/Functions/Functions.thy` (diff)
The file was modified	`src/Doc/How_to_Prove_it/How_to_Prove_it.thy` (diff)
The file was modified	`src/Doc/Logics_ZF/FOL_examples.thy` (diff)
The file was modified	`src/Doc/Logics_ZF/IFOL_examples.thy` (diff)
The file was modified	`src/Doc/Logics_ZF/If.thy` (diff)
The file was modified	`src/Doc/Logics_ZF/ZF_Isar.thy` (diff)
The file was modified	`src/Doc/Logics_ZF/ZF_examples.thy` (diff)
The file was modified	`src/Doc/Prog_Prove/Basics.thy` (diff)
The file was modified	`src/Doc/Prog_Prove/Bool_nat_list.thy` (diff)
The file was modified	`src/Doc/Prog_Prove/Isar.thy` (diff)
The file was modified	`src/Doc/Prog_Prove/LaTeXsugar.thy` (diff)
The file was modified	`src/Doc/Prog_Prove/Logic.thy` (diff)
The file was modified	`src/Doc/Prog_Prove/Types_and_funs.thy` (diff)
The file was modified	`src/Doc/Sugar/Sugar.thy` (diff)
The file was modified	`src/Doc/Tutorial/Advanced/Partial.thy` (diff)
The file was modified	`src/Doc/Tutorial/Advanced/WFrec.thy` (diff)
The file was modified	`src/Doc/Tutorial/Advanced/simp2.thy` (diff)
The file was modified	`src/Doc/Tutorial/CTL/Base.thy` (diff)
The file was modified	`src/Doc/Tutorial/CTL/CTL.thy` (diff)
The file was modified	`src/Doc/Tutorial/CTL/CTLind.thy` (diff)
The file was modified	`src/Doc/Tutorial/CTL/PDL.thy` (diff)
The file was modified	`src/Doc/Tutorial/CodeGen/CodeGen.thy` (diff)
The file was modified	`src/Doc/Tutorial/Datatype/ABexpr.thy` (diff)
The file was modified	`src/Doc/Tutorial/Datatype/Fundata.thy` (diff)
The file was modified	`src/Doc/Tutorial/Datatype/Nested.thy` (diff)
The file was modified	`src/Doc/Tutorial/Documents/Documents.thy` (diff)
The file was modified	`src/Doc/Tutorial/Fun/fun0.thy` (diff)
The file was modified	`src/Doc/Tutorial/Ifexpr/Ifexpr.thy` (diff)
The file was modified	`src/Doc/Tutorial/Inductive/AB.thy` (diff)
The file was modified	`src/Doc/Tutorial/Inductive/Advanced.thy` (diff)
The file was modified	`src/Doc/Tutorial/Inductive/Even.thy` (diff)
The file was modified	`src/Doc/Tutorial/Inductive/Mutual.thy` (diff)
The file was modified	`src/Doc/Tutorial/Inductive/Star.thy` (diff)
The file was modified	`src/Doc/Tutorial/Misc/AdvancedInd.thy` (diff)
The file was modified	`src/Doc/Tutorial/Misc/Itrev.thy` (diff)
The file was modified	`src/Doc/Tutorial/Misc/Option2.thy` (diff)
The file was modified	`src/Doc/Tutorial/Misc/Plus.thy` (diff)
The file was modified	`src/Doc/Tutorial/Misc/Tree.thy` (diff)
The file was modified	`src/Doc/Tutorial/Misc/Tree2.thy` (diff)
The file was modified	`src/Doc/Tutorial/Misc/appendix.thy` (diff)
The file was modified	`src/Doc/Tutorial/Misc/case_exprs.thy` (diff)
The file was modified	`src/Doc/Tutorial/Misc/fakenat.thy` (diff)
The file was modified	`src/Doc/Tutorial/Misc/natsum.thy` (diff)
The file was modified	`src/Doc/Tutorial/Misc/pairs2.thy` (diff)
The file was modified	`src/Doc/Tutorial/Misc/prime_def.thy` (diff)
The file was modified	`src/Doc/Tutorial/Misc/simp.thy` (diff)
The file was modified	`src/Doc/Tutorial/Misc/types.thy` (diff)
The file was modified	`src/Doc/Tutorial/Protocol/Event.thy` (diff)
The file was modified	`src/Doc/Tutorial/Protocol/Message.thy` (diff)
The file was modified	`src/Doc/Tutorial/Protocol/NS_Public.thy` (diff)
The file was modified	`src/Doc/Tutorial/Protocol/Public.thy` (diff)
The file was modified	`src/Doc/Tutorial/Recdef/Induction.thy` (diff)
The file was modified	`src/Doc/Tutorial/Recdef/Nested0.thy` (diff)
The file was modified	`src/Doc/Tutorial/Recdef/Nested1.thy` (diff)
The file was modified	`src/Doc/Tutorial/Recdef/Nested2.thy` (diff)
The file was modified	`src/Doc/Tutorial/Recdef/examples.thy` (diff)
The file was modified	`src/Doc/Tutorial/Recdef/simplification.thy` (diff)
The file was modified	`src/Doc/Tutorial/Recdef/termination.thy` (diff)
The file was modified	`src/Doc/Tutorial/Rules/Basic.thy` (diff)
The file was modified	`src/Doc/Tutorial/Rules/Blast.thy` (diff)
The file was modified	`src/Doc/Tutorial/Rules/Force.thy` (diff)
The file was modified	`src/Doc/Tutorial/Rules/Forward.thy` (diff)
The file was modified	`src/Doc/Tutorial/Rules/TPrimes.thy` (diff)
The file was modified	`src/Doc/Tutorial/Rules/Tacticals.thy` (diff)
The file was modified	`src/Doc/Tutorial/Rules/find2.thy` (diff)
The file was modified	`src/Doc/Tutorial/Sets/Examples.thy` (diff)
The file was modified	`src/Doc/Tutorial/Sets/Functions.thy` (diff)
The file was modified	`src/Doc/Tutorial/Sets/Recur.thy` (diff)
The file was modified	`src/Doc/Tutorial/Sets/Relations.thy` (diff)
The file was modified	`src/Doc/Tutorial/ToyList/ToyList.thy` (diff)
The file was modified	`src/Doc/Tutorial/ToyList/ToyList_Test.thy` (diff)
The file was modified	`src/Doc/Tutorial/Trie/Trie.thy` (diff)
The file was modified	`src/Doc/Tutorial/Types/Axioms.thy` (diff)
The file was modified	`src/Doc/Tutorial/Types/Numbers.thy` (diff)
The file was modified	`src/Doc/Tutorial/Types/Overloading.thy` (diff)
The file was modified	`src/Doc/Tutorial/Types/Pairs.thy` (diff)
The file was modified	`src/Doc/Tutorial/Types/Records.thy` (diff)
The file was modified	`src/Doc/Tutorial/Types/Typedefs.thy` (diff)
The file was modified	`src/HOL/Data_Structures/AA_Map.thy` (diff)
The file was modified	`src/HOL/Data_Structures/AA_Set.thy` (diff)
The file was modified	`src/HOL/Data_Structures/AList_Upd_Del.thy` (diff)
The file was modified	`src/HOL/Data_Structures/AVL_Map.thy` (diff)
The file was modified	`src/HOL/Data_Structures/AVL_Set.thy` (diff)
The file was modified	`src/HOL/Data_Structures/Brother12_Map.thy` (diff)
The file was modified	`src/HOL/Data_Structures/Brother12_Set.thy` (diff)
The file was modified	`src/HOL/Data_Structures/Cmp.thy` (diff)
The file was modified	`src/HOL/Data_Structures/Leftist_Heap.thy` (diff)
The file was modified	`src/HOL/Data_Structures/Less_False.thy` (diff)
The file was modified	`src/HOL/Data_Structures/List_Ins_Del.thy` (diff)
The file was modified	`src/HOL/Data_Structures/Map_by_Ordered.thy` (diff)
The file was modified	`src/HOL/Data_Structures/Set_by_Ordered.thy` (diff)
The file was modified	`src/HOL/Data_Structures/Sorted_Less.thy` (diff)
The file was modified	`src/HOL/Data_Structures/Tree234.thy` (diff)
The file was modified	`src/HOL/Data_Structures/Tree234_Set.thy` (diff)
The file was modified	`src/HOL/Data_Structures/Tree23_Set.thy` (diff)
The file was modified	`src/HOL/IMP/ACom.thy` (diff)
The file was modified	`src/HOL/IMP/AExp.thy` (diff)
The file was modified	`src/HOL/IMP/ASM.thy` (diff)
The file was modified	`src/HOL/IMP/Abs_Int0.thy` (diff)
The file was modified	`src/HOL/IMP/Abs_Int1.thy` (diff)
The file was modified	`src/HOL/IMP/Abs_Int1_const.thy` (diff)
The file was modified	`src/HOL/IMP/Abs_Int1_parity.thy` (diff)
The file was modified	`src/HOL/IMP/Abs_Int2.thy` (diff)
The file was modified	`src/HOL/IMP/Abs_Int2_ivl.thy` (diff)
The file was modified	`src/HOL/IMP/Abs_Int3.thy` (diff)
The file was modified	`src/HOL/IMP/Abs_Int_Tests.thy` (diff)
The file was modified	`src/HOL/IMP/Abs_Int_init.thy` (diff)
The file was modified	`src/HOL/IMP/Abs_State.thy` (diff)
The file was modified	`src/HOL/IMP/BExp.thy` (diff)
The file was modified	`src/HOL/IMP/Big_Step.thy` (diff)
The file was modified	`src/HOL/IMP/C_like.thy` (diff)
The file was modified	`src/HOL/IMP/Collecting.thy` (diff)
The file was modified	`src/HOL/IMP/Collecting1.thy` (diff)
The file was modified	`src/HOL/IMP/Collecting_Examples.thy` (diff)
The file was modified	`src/HOL/IMP/Compiler.thy` (diff)
The file was modified	`src/HOL/IMP/Compiler2.thy` (diff)
The file was modified	`src/HOL/IMP/Def_Init_Big.thy` (diff)
The file was modified	`src/HOL/IMP/Def_Init_Small.thy` (diff)
The file was modified	`src/HOL/IMP/Denotational.thy` (diff)
The file was modified	`src/HOL/IMP/Finite_Reachable.thy` (diff)
The file was modified	`src/HOL/IMP/Hoare.thy` (diff)
The file was modified	`src/HOL/IMP/Hoare_Examples.thy` (diff)
The file was modified	`src/HOL/IMP/Hoare_Total.thy` (diff)
The file was modified	`src/HOL/IMP/Hoare_Total_EX.thy` (diff)
The file was modified	`src/HOL/IMP/Hoare_Total_EX2.thy` (diff)
The file was modified	`src/HOL/IMP/Live.thy` (diff)
The file was modified	`src/HOL/IMP/Live_True.thy` (diff)
The file was modified	`src/HOL/IMP/OO.thy` (diff)
The file was modified	`src/HOL/IMP/Poly_Types.thy` (diff)
The file was modified	`src/HOL/IMP/Sec_Type_Expr.thy` (diff)
The file was modified	`src/HOL/IMP/Sec_Typing.thy` (diff)
The file was modified	`src/HOL/IMP/Sec_TypingT.thy` (diff)
The file was modified	`src/HOL/IMP/Sem_Equiv.thy` (diff)
The file was modified	`src/HOL/IMP/Small_Step.thy` (diff)
The file was modified	`src/HOL/IMP/Star.thy` (diff)
The file was modified	`src/HOL/IMP/Types.thy` (diff)
The file was modified	`src/HOL/IMP/VCG.thy` (diff)
The file was modified	`src/HOL/IMP/VCG_Total_EX.thy` (diff)
The file was modified	`src/HOL/IMP/VCG_Total_EX2.thy` (diff)
The file was modified	`src/HOL/IMP/Vars.thy` (diff)