Changes

Summary

recovered outer Pretty.block from 30c1639a343a, avoid excessive line breaks due to implicit Pretty.chunks;
merged
more symbols;

Changeset 67615:967213048e55 by wenzelm: recovered outer Pretty.block from 30c1639a343a, avoid excessive line breaks due to implicit Pretty.chunks;
The file was modified	`src/Pure/Isar/named_target.ML` (diff)
Changeset 67614:560fbd6bc047 by wenzelm: merged
Changeset 67613:ce654b0e6d69 by wenzelm: more symbols;
The file was modified	`src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Base.thy` (diff)
The file was modified	`src/Doc/Prog_Prove/Isar.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/CTL/CTL.thy` (diff)
The file was modified	`src/Doc/Tutorial/CTL/PDL.thy` (diff)
The file was modified	`src/Doc/Tutorial/Ifexpr/Ifexpr.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/Plus.thy` (diff)
The file was modified	`src/Doc/Tutorial/Misc/Tree2.thy` (diff)
The file was modified	`src/Doc/Tutorial/Misc/prime_def.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/Public.thy` (diff)
The file was modified	`src/Doc/Tutorial/Rules/TPrimes.thy` (diff)
The file was modified	`src/Doc/Tutorial/Sets/Examples.thy` (diff)
The file was modified	`src/HOL/Algebra/AbelCoset.thy` (diff)
The file was modified	`src/HOL/Algebra/FiniteProduct.thy` (diff)
The file was modified	`src/HOL/Algebra/Group.thy` (diff)
The file was modified	`src/HOL/Algebra/Order.thy` (diff)
The file was modified	`src/HOL/Algebra/Ring.thy` (diff)
The file was modified	`src/HOL/Algebra/RingHom.thy` (diff)
The file was modified	`src/HOL/Algebra/Sylow.thy` (diff)
The file was modified	`src/HOL/Algebra/UnivPoly.thy` (diff)
The file was modified	`src/HOL/Analysis/Arcwise_Connected.thy` (diff)
The file was modified	`src/HOL/Analysis/Cauchy_Integral_Theorem.thy` (diff)
The file was modified	`src/HOL/Analysis/Continuous_Extension.thy` (diff)
The file was modified	`src/HOL/Analysis/Convex_Euclidean_Space.thy` (diff)
The file was modified	`src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy` (diff)
The file was modified	`src/HOL/Analysis/Extended_Real_Limits.thy` (diff)
The file was modified	`src/HOL/Analysis/Polytope.thy` (diff)
The file was modified	`src/HOL/Analysis/Starlike.thy` (diff)
The file was modified	`src/HOL/Analysis/Topology_Euclidean_Space.thy` (diff)
The file was modified	`src/HOL/Auth/CertifiedEmail.thy` (diff)
The file was modified	`src/HOL/Auth/Event.thy` (diff)
The file was modified	`src/HOL/Auth/Guard/Analz.thy` (diff)
The file was modified	`src/HOL/Auth/Guard/Extensions.thy` (diff)
The file was modified	`src/HOL/Auth/Guard/Guard.thy` (diff)
The file was modified	`src/HOL/Auth/Guard/GuardK.thy` (diff)
The file was modified	`src/HOL/Auth/Guard/Guard_NS_Public.thy` (diff)
The file was modified	`src/HOL/Auth/Guard/Guard_OtwayRees.thy` (diff)
The file was modified	`src/HOL/Auth/Guard/Guard_Public.thy` (diff)
The file was modified	`src/HOL/Auth/Guard/Guard_Shared.thy` (diff)
The file was modified	`src/HOL/Auth/Guard/Guard_Yahalom.thy` (diff)
The file was modified	`src/HOL/Auth/Guard/List_Msg.thy` (diff)
The file was modified	`src/HOL/Auth/Guard/P1.thy` (diff)
The file was modified	`src/HOL/Auth/Guard/P2.thy` (diff)
The file was modified	`src/HOL/Auth/Guard/Proto.thy` (diff)
The file was modified	`src/HOL/Auth/KerberosIV.thy` (diff)
The file was modified	`src/HOL/Auth/KerberosIV_Gets.thy` (diff)
The file was modified	`src/HOL/Auth/KerberosV.thy` (diff)
The file was modified	`src/HOL/Auth/Kerberos_BAN.thy` (diff)
The file was modified	`src/HOL/Auth/Kerberos_BAN_Gets.thy` (diff)
The file was modified	`src/HOL/Auth/Message.thy` (diff)
The file was modified	`src/HOL/Auth/NS_Shared.thy` (diff)
The file was modified	`src/HOL/Auth/OtwayRees.thy` (diff)
The file was modified	`src/HOL/Auth/OtwayReesBella.thy` (diff)
The file was modified	`src/HOL/Auth/OtwayRees_AN.thy` (diff)
The file was modified	`src/HOL/Auth/OtwayRees_Bad.thy` (diff)
The file was modified	`src/HOL/Auth/Public.thy` (diff)
The file was modified	`src/HOL/Auth/Recur.thy` (diff)
The file was modified	`src/HOL/Auth/Shared.thy` (diff)
The file was modified	`src/HOL/Auth/Smartcard/Smartcard.thy` (diff)
The file was modified	`src/HOL/Auth/TLS.thy` (diff)
The file was modified	`src/HOL/Auth/WooLam.thy` (diff)
The file was modified	`src/HOL/Auth/Yahalom.thy` (diff)
The file was modified	`src/HOL/Auth/Yahalom2.thy` (diff)
The file was modified	`src/HOL/Auth/Yahalom_Bad.thy` (diff)
The file was modified	`src/HOL/BNF_Cardinal_Arithmetic.thy` (diff)
The file was modified	`src/HOL/BNF_Cardinal_Order_Relation.thy` (diff)
The file was modified	`src/HOL/BNF_Composition.thy` (diff)
The file was modified	`src/HOL/BNF_Def.thy` (diff)
The file was modified	`src/HOL/BNF_Greatest_Fixpoint.thy` (diff)
The file was modified	`src/HOL/BNF_Wellorder_Constructions.thy` (diff)
The file was modified	`src/HOL/BNF_Wellorder_Embedding.thy` (diff)
The file was modified	`src/HOL/Bali/AxCompl.thy` (diff)
The file was modified	`src/HOL/Bali/AxSem.thy` (diff)
The file was modified	`src/HOL/Bali/AxSound.thy` (diff)
The file was modified	`src/HOL/Bali/Basis.thy` (diff)
The file was modified	`src/HOL/Bali/Decl.thy` (diff)
The file was modified	`src/HOL/Bali/DeclConcepts.thy` (diff)
The file was modified	`src/HOL/Bali/Example.thy` (diff)
The file was modified	`src/HOL/Bali/Table.thy` (diff)
The file was modified	`src/HOL/Bali/TypeRel.thy` (diff)
The file was modified	`src/HOL/Bali/WellForm.thy` (diff)
The file was modified	`src/HOL/Cardinals/Cardinal_Order_Relation.thy` (diff)
The file was modified	`src/HOL/Cardinals/Wellorder_Constructions.thy` (diff)
The file was modified	`src/HOL/Complete_Lattices.thy` (diff)
The file was modified	`src/HOL/Computational_Algebra/Primes.thy` (diff)
The file was modified	`src/HOL/Conditionally_Complete_Lattices.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/Brother12_Set.thy` (diff)
The file was modified	`src/HOL/Decision_Procs/MIR.thy` (diff)
The file was modified	`src/HOL/Decision_Procs/approximation.ML` (diff)
The file was modified	`src/HOL/Enum.thy` (diff)
The file was modified	`src/HOL/Filter.thy` (diff)
The file was modified	`src/HOL/Fun_Def.thy` (diff)
The file was modified	`src/HOL/HOLCF/FOCUS/Buffer.thy` (diff)
The file was modified	`src/HOL/HOLCF/FOCUS/Buffer_adm.thy` (diff)
The file was modified	`src/HOL/HOLCF/FOCUS/FOCUS.thy` (diff)
The file was modified	`src/HOL/HOLCF/FOCUS/Fstream.thy` (diff)
The file was modified	`src/HOL/HOLCF/FOCUS/Stream_adm.thy` (diff)
The file was modified	`src/HOL/HOLCF/IMP/Denotational.thy` (diff)
The file was modified	`src/HOL/HOLCF/IOA/ABP/Lemmas.thy` (diff)
The file was modified	`src/HOL/HOLCF/IOA/CompoExecs.thy` (diff)
The file was modified	`src/HOL/HOLCF/IOA/CompoScheds.thy` (diff)
The file was modified	`src/HOL/HOLCF/IOA/CompoTraces.thy` (diff)
The file was modified	`src/HOL/HOLCF/IOA/NTP/Abschannel.thy` (diff)
The file was modified	`src/HOL/HOLCF/IOA/NTP/Correctness.thy` (diff)
The file was modified	`src/HOL/HOLCF/IOA/NTP/Impl.thy` (diff)
The file was modified	`src/HOL/HOLCF/IOA/NTP/Lemmas.thy` (diff)
The file was modified	`src/HOL/HOLCF/IOA/NTP/Multiset.thy` (diff)
The file was modified	`src/HOL/HOLCF/IOA/NTP/Packet.thy` (diff)
The file was modified	`src/HOL/HOLCF/IOA/NTP/Receiver.thy` (diff)
The file was modified	`src/HOL/HOLCF/IOA/NTP/Sender.thy` (diff)
The file was modified	`src/HOL/HOLCF/IOA/NTP/Spec.thy` (diff)
The file was modified	`src/HOL/HOLCF/IOA/RefCorrectness.thy` (diff)
The file was modified	`src/HOL/HOLCF/IOA/SimCorrectness.thy` (diff)
The file was modified	`src/HOL/HOLCF/IOA/Simulations.thy` (diff)
The file was modified	`src/HOL/HOLCF/IOA/Storage/Action.thy` (diff)
The file was modified	`src/HOL/HOLCF/IOA/Storage/Correctness.thy` (diff)
The file was modified	`src/HOL/HOLCF/IOA/Storage/Impl.thy` (diff)
The file was modified	`src/HOL/HOLCF/IOA/Storage/Spec.thy` (diff)
The file was modified	`src/HOL/HOLCF/Library/Stream.thy` (diff)
The file was modified	`src/HOL/HOLCF/Tools/Domain/domain_induction.ML` (diff)
The file was modified	`src/HOL/HOLCF/ex/Loop.thy` (diff)
The file was modified	`src/HOL/Hilbert_Choice.thy` (diff)
The file was modified	`src/HOL/Hoare/Arith2.thy` (diff)
The file was modified	`src/HOL/Hoare/Examples.thy` (diff)
The file was modified	`src/HOL/Hoare/Heap.thy` (diff)
The file was modified	`src/HOL/Hoare/Hoare_Logic.thy` (diff)
The file was modified	`src/HOL/Hoare/Hoare_Logic_Abort.thy` (diff)
The file was modified	`src/HOL/Hoare/Pointer_Examples.thy` (diff)
The file was modified	`src/HOL/Hoare/Pointers0.thy` (diff)
The file was modified	`src/HOL/Hoare_Parallel/RG_Tran.thy` (diff)
The file was modified	`src/HOL/IMP/ACom.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_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_State.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/Complete_Lattice.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/Fold.thy` (diff)
The file was modified	`src/HOL/IMP/Live.thy` (diff)
The file was modified	`src/HOL/IMP/Small_Step.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/IMPP/Com.thy` (diff)
The file was modified	`src/HOL/IMPP/Hoare.thy` (diff)
The file was modified	`src/HOL/IMPP/Misc.thy` (diff)
The file was modified	`src/HOL/IMPP/Natural.thy` (diff)
The file was modified	`src/HOL/IOA/Asig.thy` (diff)
The file was modified	`src/HOL/IOA/IOA.thy` (diff)
The file was modified	`src/HOL/IOA/Solve.thy` (diff)
The file was modified	`src/HOL/Induct/SList.thy` (diff)
The file was modified	`src/HOL/Induct/Sexp.thy` (diff)
The file was modified	`src/HOL/Isar_Examples/Hoare.thy` (diff)
The file was modified	`src/HOL/Lattices_Big.thy` (diff)
The file was modified	`src/HOL/Library/BNF_Corec.thy` (diff)
The file was modified	`src/HOL/Library/Countable_Set.thy` (diff)
The file was modified	`src/HOL/Library/IArray.thy` (diff)
The file was modified	`src/HOL/Library/Lub_Glb.thy` (diff)
The file was modified	`src/HOL/Library/Old_Datatype.thy` (diff)
The file was modified	`src/HOL/Library/Stream.thy` (diff)
The file was modified	`src/HOL/Library/Sublist.thy` (diff)
The file was modified	`src/HOL/Library/While_Combinator.thy` (diff)
The file was modified	`src/HOL/List.thy` (diff)
The file was modified	`src/HOL/Matrix_LP/ComputeFloat.thy` (diff)
The file was modified	`src/HOL/Matrix_LP/Matrix.thy` (diff)
The file was modified	`src/HOL/Matrix_LP/SparseMatrix.thy` (diff)
The file was modified	`src/HOL/Metis_Examples/Big_O.thy` (diff)
The file was modified	`src/HOL/Metis_Examples/Clausification.thy` (diff)
The file was modified	`src/HOL/Metis_Examples/Message.thy` (diff)
The file was modified	`src/HOL/Metis_Examples/Sets.thy` (diff)
The file was modified	`src/HOL/Metis_Examples/Tarski.thy` (diff)
The file was modified	`src/HOL/MicroJava/BV/BVExample.thy` (diff)
The file was modified	`src/HOL/MicroJava/BV/JType.thy` (diff)
The file was modified	`src/HOL/MicroJava/BV/Typing_Framework_JVM.thy` (diff)
The file was modified	`src/HOL/MicroJava/Comp/CorrComp.thy` (diff)
The file was modified	`src/HOL/MicroJava/Comp/LemmasComp.thy` (diff)
The file was modified	`src/HOL/MicroJava/DFA/Err.thy` (diff)
The file was modified	`src/HOL/MicroJava/DFA/Kildall.thy` (diff)
The file was modified	`src/HOL/MicroJava/DFA/Listn.thy` (diff)
The file was modified	`src/HOL/MicroJava/DFA/Opt.thy` (diff)
The file was modified	`src/HOL/MicroJava/DFA/Product.thy` (diff)
The file was modified	`src/HOL/MicroJava/DFA/Semilat.thy` (diff)
The file was modified	`src/HOL/MicroJava/DFA/SemilatAlg.thy` (diff)
The file was modified	`src/HOL/MicroJava/DFA/Typing_Framework.thy` (diff)
The file was modified	`src/HOL/MicroJava/J/Example.thy` (diff)
The file was modified	`src/HOL/MicroJava/J/JBasis.thy` (diff)
The file was modified	`src/HOL/MicroJava/J/TypeRel.thy` (diff)
The file was modified	`src/HOL/MicroJava/J/WellForm.thy` (diff)
The file was modified	`src/HOL/MicroJava/JVM/JVMExec.thy` (diff)
The file was modified	`src/HOL/NanoJava/Equivalence.thy` (diff)
The file was modified	`src/HOL/NanoJava/TypeRel.thy` (diff)
The file was modified	`src/HOL/Nitpick_Examples/Core_Nits.thy` (diff)
The file was modified	`src/HOL/Nitpick_Examples/Mini_Nits.thy` (diff)
The file was modified	`src/HOL/Nitpick_Examples/Refute_Nits.thy` (diff)
The file was modified	`src/HOL/Nominal/Examples/Class1.thy` (diff)
The file was modified	`src/HOL/Nonstandard_Analysis/HyperDef.thy` (diff)
The file was modified	`src/HOL/Nonstandard_Analysis/NSCA.thy` (diff)
The file was modified	`src/HOL/Nonstandard_Analysis/Star.thy` (diff)
The file was modified	`src/HOL/Predicate_Compile.thy` (diff)
The file was modified	`src/HOL/Predicate_Compile_Examples/Hotel_Example.thy` (diff)
The file was modified	`src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy` (diff)
The file was modified	`src/HOL/Presburger.thy` (diff)
The file was modified	`src/HOL/Prolog/Test.thy` (diff)
The file was modified	`src/HOL/Prolog/Type.thy` (diff)
The file was modified	`src/HOL/Proofs/Lambda/Commutation.thy` (diff)
The file was modified	`src/HOL/Proofs/Lambda/Eta.thy` (diff)
The file was modified	`src/HOL/Proofs/Lambda/InductTermi.thy` (diff)
The file was modified	`src/HOL/Proofs/Lambda/Lambda.thy` (diff)
The file was modified	`src/HOL/Proofs/Lambda/ListOrder.thy` (diff)
The file was modified	`src/HOL/Proofs/Lambda/ParRed.thy` (diff)
The file was modified	`src/HOL/Quickcheck_Examples/Hotel_Example.thy` (diff)
The file was modified	`src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy` (diff)
The file was modified	`src/HOL/Quickcheck_Examples/Quickcheck_Narrowing_Examples.thy` (diff)
The file was modified	`src/HOL/SET_Protocol/Cardholder_Registration.thy` (diff)
The file was modified	`src/HOL/SET_Protocol/Event_SET.thy` (diff)
The file was modified	`src/HOL/SET_Protocol/Merchant_Registration.thy` (diff)
The file was modified	`src/HOL/SET_Protocol/Message_SET.thy` (diff)
The file was modified	`src/HOL/SET_Protocol/Public_SET.thy` (diff)
The file was modified	`src/HOL/SET_Protocol/Purchase.thy` (diff)
The file was modified	`src/HOL/SMT_Examples/SMT_Examples.thy` (diff)
The file was modified	`src/HOL/Set.thy` (diff)
The file was modified	`src/HOL/Set_Interval.thy` (diff)
The file was modified	`src/HOL/TLA/Memory/Memory.thy` (diff)
The file was modified	`src/HOL/TLA/Memory/MemoryImplementation.thy` (diff)
The file was modified	`src/HOL/TLA/Memory/MemoryParameters.thy` (diff)
The file was modified	`src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML` (diff)
The file was modified	`src/HOL/TPTP/TPTP_Proof_Reconstruction.thy` (diff)
The file was modified	`src/HOL/Transitive_Closure.thy` (diff)
The file was modified	`src/HOL/UNITY/Comp/Alloc.thy` (diff)
The file was modified	`src/HOL/UNITY/Comp/AllocBase.thy` (diff)
The file was modified	`src/HOL/UNITY/Comp/Handshake.thy` (diff)
The file was modified	`src/HOL/UNITY/Comp/Priority.thy` (diff)
The file was modified	`src/HOL/UNITY/Comp/PriorityAux.thy` (diff)
The file was modified	`src/HOL/UNITY/Comp/TimerArray.thy` (diff)
The file was modified	`src/HOL/UNITY/Constrains.thy` (diff)
The file was modified	`src/HOL/UNITY/ELT.thy` (diff)
The file was modified	`src/HOL/UNITY/Extend.thy` (diff)
The file was modified	`src/HOL/UNITY/FP.thy` (diff)
The file was modified	`src/HOL/UNITY/Guar.thy` (diff)
The file was modified	`src/HOL/UNITY/ListOrder.thy` (diff)
The file was modified	`src/HOL/UNITY/PPROD.thy` (diff)
The file was modified	`src/HOL/UNITY/Simple/NSP_Bad.thy` (diff)
The file was modified	`src/HOL/UNITY/Simple/Reach.thy` (diff)
The file was modified	`src/HOL/UNITY/Simple/Reachability.thy` (diff)
The file was modified	`src/HOL/UNITY/SubstAx.thy` (diff)
The file was modified	`src/HOL/UNITY/Transformers.thy` (diff)
The file was modified	`src/HOL/UNITY/UNITY.thy` (diff)
The file was modified	`src/HOL/UNITY/Union.thy` (diff)
The file was modified	`src/HOL/UNITY/WFair.thy` (diff)
The file was modified	`src/HOL/Word/Misc_Typedef.thy` (diff)
The file was modified	`src/HOL/ZF/Games.thy` (diff)
The file was modified	`src/HOL/ZF/HOLZF.thy` (diff)
The file was modified	`src/HOL/ZF/LProd.thy` (diff)
The file was modified	`src/HOL/ZF/Zet.thy` (diff)
The file was modified	`src/HOL/Zorn.thy` (diff)
The file was modified	`src/HOL/ex/Birthday_Paradox.thy` (diff)
The file was modified	`src/HOL/ex/Dedekind_Real.thy` (diff)
The file was modified	`src/HOL/ex/Executable_Relation.thy` (diff)
The file was modified	`src/HOL/ex/Groebner_Examples.thy` (diff)
The file was modified	`src/HOL/ex/Intuitionistic.thy` (diff)
The file was modified	`src/HOL/ex/LocaleTest2.thy` (diff)
The file was modified	`src/HOL/ex/Refute_Examples.thy` (diff)
The file was modified	`src/HOL/ex/SAT_Examples.thy` (diff)
The file was modified	`src/HOL/ex/Set_Comprehension_Pointfree_Examples.thy` (diff)
The file was modified	`src/HOL/ex/Set_Theory.thy` (diff)
The file was modified	`src/HOL/ex/Tarski.thy` (diff)
The file was modified	`src/HOL/ex/While_Combinator_Example.thy` (diff)