Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. Experimental support for rewrite morphisms in locale instances.
  2. tuned signature;
  3. more documentation;
  4. clarified markup;
  5. discontinued old form of marginal comments;
  6. tuned document;
  7. clarified comments;
  8. standardized towards new-style formal comments: isabelle update_comments;
  9. uniform treatment of old-style and new-style comments;
  10. tuned signature;
  11. clarified markup;
  12. more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
  13. clarified modules; more operations;
Changeset 67450:b0ae74b86ef3 by ballarin:
Experimental support for rewrite morphisms in locale instances.
The file was modified src/FOL/ex/Locale_Test/Locale_Test1.thy (diff)
The file was modified src/HOL/Statespace/state_space.ML (diff)
The file was modified src/Pure/Isar/class_declaration.ML (diff)
The file was modified src/Pure/Isar/expression.ML (diff)
The file was modified src/Pure/Isar/interpretation.ML (diff)
The file was modified src/Pure/Isar/parse_spec.ML (diff)
The file was modified src/Pure/Pure.thy (diff)
Changeset 67449:1caeb087d957 by wenzelm:
tuned signature;
The file was modified src/Pure/General/comment.scala (diff)
The file was modified src/Pure/General/symbol.scala (diff)
Changeset 67448:dbb1f02e667d by wenzelm:
more documentation;
The file was modified NEWS (diff)
The file was modified src/Doc/Isar_Ref/Inner_Syntax.thy (diff)
The file was modified src/Doc/Isar_Ref/Outer_Syntax.thy (diff)
Changeset 67447:c98c6eb3dd4c by wenzelm:
clarified markup;
The file was modified src/Tools/jEdit/src/jedit_rendering.scala (diff)
Changeset 67446:1f4d167b6ac9 by wenzelm:
discontinued old form of marginal comments;
The file was modified NEWS (diff)
The file was modified src/Pure/Isar/outer_syntax.ML (diff)
The file was modified src/Pure/Isar/token.ML (diff)
The file was modified src/Pure/Isar/token.scala (diff)
The file was modified src/Pure/PIDE/command.ML (diff)
The file was modified src/Pure/PIDE/command.scala (diff)
The file was modified src/Pure/Pure.thy (diff)
The file was modified src/Pure/Thy/thy_output.ML (diff)
Changeset 67445:4311845b0412 by wenzelm:
tuned document;
The file was modified src/HOL/UNITY/Comp/Alloc.thy (diff)
The file was modified src/ZF/UNITY/Mutex.thy (diff)
Changeset 67444:100247708f31 by wenzelm:
clarified comments;
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/Separation.thy (diff)
Changeset 67443:3abf6a722518 by wenzelm:
standardized towards new-style formal comments: isabelle update_comments;
The file was modified src/CCL/Gfp.thy (diff)
The file was modified src/CCL/Lfp.thy (diff)
The file was modified src/CTT/CTT.thy (diff)
The file was modified src/Doc/Eisbach/Manual.thy (diff)
The file was modified src/Doc/Functions/Functions.thy (diff)
The file was modified src/Doc/Isar_Ref/Synopsis.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_examples.thy (diff)
The file was modified src/Doc/Prog_Prove/Isar.thy (diff)
The file was modified src/Doc/Sugar/Sugar.thy (diff)
The file was modified src/Doc/Tutorial/Documents/Documents.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/Rules/Basic.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/Types/Numbers.thy (diff)
The file was modified src/FOL/ex/Intuitionistic.thy (diff)
The file was modified src/FOL/ex/Locale_Test/Locale_Test1.thy (diff)
The file was modified src/FOLP/ex/Intuitionistic.thy (diff)
The file was modified src/HOL/Algebra/AbelCoset.thy (diff)
The file was modified src/HOL/Algebra/Bij.thy (diff)
The file was modified src/HOL/Algebra/Coset.thy (diff)
The file was modified src/HOL/Algebra/Divisibility.thy (diff)
The file was modified src/HOL/Algebra/Group.thy (diff)
The file was modified src/HOL/Algebra/Ideal.thy (diff)
The file was modified src/HOL/Algebra/IntRing.thy (diff)
The file was modified src/HOL/Algebra/Lattice.thy (diff)
The file was modified src/HOL/Algebra/QuotRing.thy (diff)
The file was modified src/HOL/Algebra/RingHom.thy (diff)
The file was modified src/HOL/Analysis/Brouwer_Fixpoint.thy (diff)
The file was modified src/HOL/Analysis/Cauchy_Integral_Theorem.thy (diff)
The file was modified src/HOL/Analysis/Complex_Transcendental.thy (diff)
The file was modified src/HOL/Analysis/Conformal_Mappings.thy (diff)
The file was modified src/HOL/Analysis/Improper_Integral.thy (diff)
The file was modified src/HOL/Analysis/Linear_Algebra.thy (diff)
The file was modified src/HOL/Analysis/Path_Connected.thy (diff)
The file was modified src/HOL/Analysis/Starlike.thy (diff)
The file was modified src/HOL/Analysis/Tagged_Division.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/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/Message.thy (diff)
The file was modified src/HOL/Auth/OtwayRees.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/Shared.thy (diff)
The file was modified src/HOL/Auth/Smartcard/EventSC.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/Yahalom.thy (diff)
The file was modified src/HOL/Auth/Yahalom2.thy (diff)
The file was modified src/HOL/Auth/ZhouGollmann.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/Decl.thy (diff)
The file was modified src/HOL/Bali/DeclConcepts.thy (diff)
The file was modified src/HOL/Bali/DefiniteAssignment.thy (diff)
The file was modified src/HOL/Bali/Eval.thy (diff)
The file was modified src/HOL/Bali/Evaln.thy (diff)
The file was modified src/HOL/Bali/Name.thy (diff)
The file was modified src/HOL/Bali/State.thy (diff)
The file was modified src/HOL/Bali/Table.thy (diff)
The file was modified src/HOL/Bali/Term.thy (diff)
The file was modified src/HOL/Bali/Trans.thy (diff)
The file was modified src/HOL/Bali/Type.thy (diff)
The file was modified src/HOL/Bali/TypeRel.thy (diff)
The file was modified src/HOL/Bali/TypeSafe.thy (diff)
The file was modified src/HOL/Bali/Value.thy (diff)
The file was modified src/HOL/Bali/WellType.thy (diff)
The file was modified src/HOL/Binomial.thy (diff)
The file was modified src/HOL/Cardinals/Wellorder_Extension.thy (diff)
The file was modified src/HOL/Computational_Algebra/Euclidean_Algorithm.thy (diff)
The file was modified src/HOL/Decision_Procs/ex/Approximation_Quickcheck_Ex.thy (diff)
The file was modified src/HOL/Deriv.thy (diff)
The file was modified src/HOL/Finite_Set.thy (diff)
The file was modified src/HOL/Fun_Def.thy (diff)
The file was modified src/HOL/HOL.thy (diff)
The file was modified src/HOL/HOLCF/Cont.thy (diff)
The file was modified src/HOL/HOLCF/IMP/HoareEx.thy (diff)
The file was modified src/HOL/HOLCF/Tutorial/Domain_ex.thy (diff)
The file was modified src/HOL/Hoare/Hoare_Logic.thy (diff)
The file was modified src/HOL/Hoare/SchorrWaite.thy (diff)
The file was modified src/HOL/Hoare_Parallel/Gar_Coll.thy (diff)
The file was modified src/HOL/Hoare_Parallel/Graph.thy (diff)
The file was modified src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy (diff)
The file was modified src/HOL/Hoare_Parallel/OG_Examples.thy (diff)
The file was modified src/HOL/Hoare_Parallel/OG_Hoare.thy (diff)
The file was modified src/HOL/Hoare_Parallel/RG_Examples.thy (diff)
The file was modified src/HOL/Hoare_Parallel/RG_Hoare.thy (diff)
The file was modified src/HOL/Hoare_Parallel/RG_Tran.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_Int3.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/Big_Step.thy (diff)
The file was modified src/HOL/IMP/Star.thy (diff)
The file was modified src/HOL/Imperative_HOL/Heap.thy (diff)
The file was modified src/HOL/Imperative_HOL/Ref.thy (diff)
The file was modified src/HOL/Induct/ABexp.thy (diff)
The file was modified src/HOL/Induct/Comb.thy (diff)
The file was modified src/HOL/Isar_Examples/Hoare.thy (diff)
The file was modified src/HOL/Library/Cardinality.thy (diff)
The file was modified src/HOL/Library/Code_Test.thy (diff)
The file was modified src/HOL/Library/Extended_Nonnegative_Real.thy (diff)
The file was modified src/HOL/Library/Omega_Words_Fun.thy (diff)
The file was modified src/HOL/List.thy (diff)
The file was modified src/HOL/Metis_Examples/Message.thy (diff)
The file was modified src/HOL/Metis_Examples/Trans_Closure.thy (diff)
The file was modified src/HOL/MicroJava/BV/BVSpec.thy (diff)
The file was modified src/HOL/MicroJava/BV/BVSpecTypeSafe.thy (diff)
The file was modified src/HOL/MicroJava/BV/Effect.thy (diff)
The file was modified src/HOL/MicroJava/BV/JVMType.thy (diff)
The file was modified src/HOL/MicroJava/Comp/CorrCompTp.thy (diff)
The file was modified src/HOL/MicroJava/Comp/LemmasComp.thy (diff)
The file was modified src/HOL/MicroJava/DFA/Kildall.thy (diff)
The file was modified src/HOL/MicroJava/J/Conform.thy (diff)
The file was modified src/HOL/MicroJava/J/Decl.thy (diff)
The file was modified src/HOL/MicroJava/J/Eval.thy (diff)
The file was modified src/HOL/MicroJava/J/Example.thy (diff)
The file was modified src/HOL/MicroJava/J/JTypeSafe.thy (diff)
The file was modified src/HOL/MicroJava/J/State.thy (diff)
The file was modified src/HOL/MicroJava/J/Term.thy (diff)
The file was modified src/HOL/MicroJava/J/Type.thy (diff)
The file was modified src/HOL/MicroJava/J/TypeRel.thy (diff)
The file was modified src/HOL/MicroJava/J/Value.thy (diff)
The file was modified src/HOL/MicroJava/J/WellType.thy (diff)
The file was modified src/HOL/MicroJava/JVM/JVMExec.thy (diff)
The file was modified src/HOL/MicroJava/JVM/JVMExecInstr.thy (diff)
The file was modified src/HOL/MicroJava/JVM/JVMInstructions.thy (diff)
The file was modified src/HOL/MicroJava/JVM/JVMState.thy (diff)
The file was modified src/HOL/Mirabelle/ex/Ex.thy (diff)
The file was modified src/HOL/NanoJava/AxSem.thy (diff)
The file was modified src/HOL/NanoJava/Decl.thy (diff)
The file was modified src/HOL/NanoJava/State.thy (diff)
The file was modified src/HOL/NanoJava/Term.thy (diff)
The file was modified src/HOL/NanoJava/TypeRel.thy (diff)
The file was modified src/HOL/Nominal/Examples/Fsub.thy (diff)
The file was modified src/HOL/Nominal/Examples/SN.thy (diff)
The file was modified src/HOL/Nominal/Nominal.thy (diff)
The file was modified src/HOL/Nonstandard_Analysis/HSEQ.thy (diff)
The file was modified src/HOL/Nonstandard_Analysis/HTranscendental.thy (diff)
The file was modified src/HOL/Nonstandard_Analysis/NSCA.thy (diff)
The file was modified src/HOL/Orderings.thy (diff)
The file was modified src/HOL/Predicate_Compile_Examples/Examples.thy (diff)
The file was modified src/HOL/Probability/ex/Dining_Cryptographers.thy (diff)
The file was modified src/HOL/Product_Type.thy (diff)
The file was modified src/HOL/Proofs/Lambda/NormalForm.thy (diff)
The file was modified src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy (diff)
The file was modified src/HOL/SET_Protocol/Cardholder_Registration.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/Set.thy (diff)
The file was modified src/HOL/Set_Interval.thy (diff)
The file was modified src/HOL/Sum_Type.thy (diff)
The file was modified src/HOL/Transcendental.thy (diff)
The file was modified src/HOL/UNITY/Comp/Alloc.thy (diff)
The file was modified src/HOL/UNITY/Comp/Client.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/ProgressSets.thy (diff)
The file was modified src/HOL/UNITY/Simple/Lift.thy (diff)
The file was modified src/HOL/UNITY/Simple/Token.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/WFair.thy (diff)
The file was modified src/HOL/Unix/Unix.thy (diff)
The file was modified src/HOL/Word/Bool_List_Representation.thy (diff)
The file was modified src/HOL/Word/Word.thy (diff)
The file was modified src/HOL/Word/Word_Miscellaneous.thy (diff)
The file was modified src/HOL/ZF/HOLZF.thy (diff)
The file was modified src/HOL/Zorn.thy (diff)
The file was modified src/HOL/ex/Classical.thy (diff)
The file was modified src/HOL/ex/Dedekind_Real.thy (diff)
The file was modified src/HOL/ex/HarmonicSeries.thy (diff)
The file was modified src/HOL/ex/Meson_Test.thy (diff)
The file was modified src/HOL/ex/NatSum.thy (diff)
The file was modified src/HOL/ex/Records.thy (diff)
The file was modified src/HOL/ex/Set_Theory.thy (diff)
The file was modified src/HOL/ex/Simproc_Tests.thy (diff)
The file was modified src/HOL/ex/Unification.thy (diff)
The file was modified src/ZF/AC/AC_Equiv.thy (diff)
The file was modified src/ZF/Cardinal.thy (diff)
The file was modified src/ZF/CardinalArith.thy (diff)
The file was modified src/ZF/Cardinal_AC.thy (diff)
The file was modified src/ZF/Constructible/AC_in_L.thy (diff)
The file was modified src/ZF/Constructible/DPow_absolute.thy (diff)
The file was modified src/ZF/Constructible/Datatype_absolute.thy (diff)
The file was modified src/ZF/Constructible/Formula.thy (diff)
The file was modified src/ZF/Constructible/Normal.thy (diff)
The file was modified src/ZF/Constructible/Rank.thy (diff)
The file was modified src/ZF/Constructible/Rank_Separation.thy (diff)
The file was modified src/ZF/Constructible/Reflection.thy (diff)
The file was modified src/ZF/Constructible/Relative.thy (diff)
The file was modified src/ZF/Constructible/Satisfies_absolute.thy (diff)
The file was modified src/ZF/Constructible/Separation.thy (diff)
The file was modified src/ZF/Constructible/WF_absolute.thy (diff)
The file was modified src/ZF/Constructible/WFrec.thy (diff)
The file was modified src/ZF/Constructible/Wellorderings.thy (diff)
The file was modified src/ZF/EquivClass.thy (diff)
The file was modified src/ZF/Induct/Binary_Trees.thy (diff)
The file was modified src/ZF/Int_ZF.thy (diff)
The file was modified src/ZF/List_ZF.thy (diff)
The file was modified src/ZF/OrderArith.thy (diff)
The file was modified src/ZF/UNITY/AllocBase.thy (diff)
The file was modified src/ZF/UNITY/Distributor.thy (diff)
The file was modified src/ZF/UNITY/Merge.thy (diff)
The file was modified src/ZF/UNITY/Mutex.thy (diff)
The file was modified src/ZF/UNITY/UNITY.thy (diff)
The file was modified src/ZF/WF.thy (diff)
The file was modified src/ZF/ZF_Base.thy (diff)
The file was modified src/ZF/Zorn.thy (diff)
The file was modified src/ZF/ex/Group.thy (diff)
The file was modified src/ZF/ex/Limit.thy (diff)
The file was modified src/ZF/ex/Primes.thy (diff)
The file was modified src/ZF/ex/Ramsey.thy (diff)
Changeset 67442:f075640b8868 by wenzelm:
uniform treatment of old-style and new-style comments;
The file was modified src/Pure/Tools/update_comments.scala (diff)
Changeset 67441:cafbb63f10e5 by wenzelm:
tuned signature;
The file was modified src/Pure/Isar/token.scala (diff)
Changeset 67440:e5ba0ca1e465 by wenzelm:
clarified markup;
The file was modified src/Pure/Isar/token.ML (diff)
The file was modified src/Pure/Syntax/lexicon.ML (diff)
Changeset 67439:78759a7bd874 by wenzelm:
more uniform support for formal comments in outer syntax, notably \&lt;^cancel&gt; and \&lt;^latex&gt;;
The file was modified src/Pure/Isar/outer_syntax.ML (diff)
The file was modified src/Pure/Isar/token.ML (diff)
The file was modified src/Pure/Isar/token.scala (diff)
The file was modified src/Pure/Thy/thy_output.ML (diff)
The file was modified src/Tools/jEdit/src/jedit_rendering.scala (diff)
Changeset 67438:fdb7b995974d by wenzelm:
clarified modules;<br>more operations;
The file was addedsrc/Pure/General/comment.scala
The file was modified src/Pure/General/scan.scala (diff)
The file was modified src/Pure/General/symbol.scala (diff)
The file was modified src/Pure/ML/ml_lex.scala (diff)
The file was modified src/Pure/build-jars (diff)
The file was modified src/Tools/jEdit/src/jedit_rendering.scala (diff)