Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. moved some material from Connected.thy to more appropriate places
  2. proper example for inner syntax, not name;
  3. tuned;
  4. tuned document layout;
  5. retain important whitespace (see 1daf07b65385);
  6. merged
  7. isabelle update -u path_cartouches;
  8. isabelle update -u control_cartouches;
  9. support for isabelle update -u path_cartouches;
  10. clarified documentation;
  11. redundant (see isabelle.Dump.make_options);
  12. typed definitions
Changeset 69611:42cc3609fedf by immler:
moved some material from Connected.thy to more appropriate places
The file was modified src/HOL/Analysis/Connected.thy (diff)
The file was modified src/HOL/Analysis/Elementary_Metric_Spaces.thy (diff)
The file was modified src/HOL/Analysis/Elementary_Normed_Spaces.thy (diff)
The file was modified src/HOL/Analysis/Elementary_Topology.thy (diff)
The file was modified src/HOL/Analysis/Topology_Euclidean_Space.thy (diff)
The file was modified src/HOL/Conditionally_Complete_Lattices.thy (diff)
Changeset 69610:10644973cdde by wenzelm:
proper example for inner syntax, not name;
The file was modified src/Doc/System/Sessions.thy (diff)
Changeset 69609:1d2d4ae9ab81 by wenzelm:
tuned;
The file was modified NEWS (diff)
Changeset 69608:2b3a247889f8 by wenzelm:
tuned document layout;
The file was modified src/HOL/Analysis/document/root.tex (diff)
Changeset 69607:7cd977863194 by wenzelm:
retain important whitespace (see 1daf07b65385);
The file was modified src/HOL/Analysis/Operator_Norm.thy (diff)
Changeset 69606:157990515be1 by wenzelm:
merged
Changeset 69605:a96320074298 by wenzelm:
isabelle update -u path_cartouches;
The file was modified src/CTT/CTT.thy (diff)
The file was modified src/Doc/Classes/Setup.thy (diff)
The file was modified src/Doc/Codegen/Introduction.thy (diff)
The file was modified src/Doc/Codegen/Setup.thy (diff)
The file was modified src/Doc/Datatypes/Setup.thy (diff)
The file was modified src/Doc/Eisbach/Base.thy (diff)
The file was modified src/Doc/Implementation/Base.thy (diff)
The file was modified src/Doc/Isar_Ref/Base.thy (diff)
The file was modified src/Doc/JEdit/Base.thy (diff)
The file was modified src/Doc/Logics_ZF/ZF_Isar.thy (diff)
The file was modified src/Doc/System/Base.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/Protocol/Message.thy (diff)
The file was modified src/Doc/Tutorial/Types/Setup.thy (diff)
The file was modified src/Doc/Typeclass_Hierarchy/Setup.thy (diff)
The file was modified src/FOL/FOL.thy (diff)
The file was modified src/FOL/IFOL.thy (diff)
The file was modified src/FOLP/FOLP.thy (diff)
The file was modified src/FOLP/IFOLP.thy (diff)
The file was modified src/HOL/ATP.thy (diff)
The file was modified src/HOL/Algebra/Ring.thy (diff)
The file was modified src/HOL/Analysis/Measurable.thy (diff)
The file was modified src/HOL/Analysis/Norm_Arith.thy (diff)
The file was modified src/HOL/Argo.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_Fixpoint_Base.thy (diff)
The file was modified src/HOL/BNF_Greatest_Fixpoint.thy (diff)
The file was modified src/HOL/BNF_Least_Fixpoint.thy (diff)
The file was modified src/HOL/Basic_BNF_LFPs.thy (diff)
The file was modified src/HOL/Code_Evaluation.thy (diff)
The file was modified src/HOL/Ctr_Sugar.thy (diff)
The file was modified src/HOL/Decision_Procs/Approximation.thy (diff)
The file was modified src/HOL/Decision_Procs/Cooper.thy (diff)
The file was modified src/HOL/Decision_Procs/Dense_Linear_Order.thy (diff)
The file was modified src/HOL/Decision_Procs/Ferrack.thy (diff)
The file was modified src/HOL/Decision_Procs/MIR.thy (diff)
The file was modified src/HOL/Eisbach/Eisbach.thy (diff)
The file was modified src/HOL/Extraction.thy (diff)
The file was modified src/HOL/Fields.thy (diff)
The file was modified src/HOL/Fun.thy (diff)
The file was modified src/HOL/Fun_Def.thy (diff)
The file was modified src/HOL/Fun_Def_Base.thy (diff)
The file was modified src/HOL/Groebner_Basis.thy (diff)
The file was modified src/HOL/Groups.thy (diff)
The file was modified src/HOL/HOL.thy (diff)
The file was modified src/HOL/HOLCF/Cpodef.thy (diff)
The file was modified src/HOL/HOLCF/Domain.thy (diff)
The file was modified src/HOL/HOLCF/Domain_Aux.thy (diff)
The file was modified src/HOL/HOLCF/Fixrec.thy (diff)
The file was modified src/HOL/HOLCF/IOA/ABP/Correctness.thy (diff)
The file was modified src/HOL/Hilbert_Choice.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/Import/Import_Setup.thy (diff)
The file was modified src/HOL/Inductive.thy (diff)
The file was modified src/HOL/Int.thy (diff)
The file was modified src/HOL/Isar_Examples/Hoare.thy (diff)
The file was modified src/HOL/Lattices.thy (diff)
The file was modified src/HOL/Library/Adhoc_Overloading.thy (diff)
The file was modified src/HOL/Library/BNF_Axiomatization.thy (diff)
The file was modified src/HOL/Library/BNF_Corec.thy (diff)
The file was modified src/HOL/Library/Cancellation.thy (diff)
The file was modified src/HOL/Library/Case_Converter.thy (diff)
The file was modified src/HOL/Library/Code_Lazy.thy (diff)
The file was modified src/HOL/Library/Code_Prolog.thy (diff)
The file was modified src/HOL/Library/Code_Test.thy (diff)
The file was modified src/HOL/Library/Conditional_Parametricity.thy (diff)
The file was modified src/HOL/Library/Countable.thy (diff)
The file was modified src/HOL/Library/Datatype_Records.thy (diff)
The file was modified src/HOL/Library/Multiset.thy (diff)
The file was modified src/HOL/Library/Old_Datatype.thy (diff)
The file was modified src/HOL/Library/Old_Recdef.thy (diff)
The file was modified src/HOL/Library/Predicate_Compile_Quickcheck.thy (diff)
The file was modified src/HOL/Library/Realizers.thy (diff)
The file was modified src/HOL/Library/Reflection.thy (diff)
The file was modified src/HOL/Library/Refute.thy (diff)
The file was modified src/HOL/Library/Rewrite.thy (diff)
The file was modified src/HOL/Library/Simps_Case_Conv.thy (diff)
The file was modified src/HOL/Library/Sum_of_Squares.thy (diff)
The file was modified src/HOL/Lifting.thy (diff)
The file was modified src/HOL/Matrix_LP/ComputeFloat.thy (diff)
The file was modified src/HOL/Matrix_LP/Compute_Oracle/Compute_Oracle.thy (diff)
The file was modified src/HOL/Matrix_LP/Cplex.thy (diff)
The file was modified src/HOL/Meson.thy (diff)
The file was modified src/HOL/Metis.thy (diff)
The file was modified src/HOL/Mirabelle/Mirabelle.thy (diff)
The file was modified src/HOL/Mirabelle/Mirabelle_Test.thy (diff)
The file was modified src/HOL/Mutabelle/MutabelleExtra.thy (diff)
The file was modified src/HOL/Nat.thy (diff)
The file was modified src/HOL/Nitpick.thy (diff)
The file was modified src/HOL/Nitpick_Examples/Mini_Nits.thy (diff)
The file was modified src/HOL/Nominal/Nominal.thy (diff)
The file was modified src/HOL/Nonstandard_Analysis/StarDef.thy (diff)
The file was modified src/HOL/Num.thy (diff)
The file was modified src/HOL/Numeral_Simprocs.thy (diff)
The file was modified src/HOL/Nunchaku.thy (diff)
The file was modified src/HOL/Orderings.thy (diff)
The file was modified src/HOL/Partial_Function.thy (diff)
The file was modified src/HOL/Predicate_Compile.thy (diff)
The file was modified src/HOL/Presburger.thy (diff)
The file was modified src/HOL/Product_Type.thy (diff)
The file was modified src/HOL/Prolog/HOHH.thy (diff)
The file was modified src/HOL/Quickcheck_Exhaustive.thy (diff)
The file was modified src/HOL/Quickcheck_Narrowing.thy (diff)
The file was modified src/HOL/Quickcheck_Random.thy (diff)
The file was modified src/HOL/Quotient.thy (diff)
The file was modified src/HOL/Real.thy (diff)
The file was modified src/HOL/Real_Asymp/Manual/Real_Asymp_Doc.thy (diff)
The file was modified src/HOL/Record.thy (diff)
The file was modified src/HOL/Rings.thy (diff)
The file was modified src/HOL/SAT.thy (diff)
The file was modified src/HOL/SMT.thy (diff)
The file was modified src/HOL/SMT_Examples/Boogie.thy (diff)
The file was modified src/HOL/SMT_Examples/SMT_Examples.thy (diff)
The file was modified src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy (diff)
The file was modified src/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy (diff)
The file was modified src/HOL/SPARK/Examples/RIPEMD-160/F.thy (diff)
The file was modified src/HOL/SPARK/Examples/RIPEMD-160/Hash.thy (diff)
The file was modified src/HOL/SPARK/Examples/RIPEMD-160/K_L.thy (diff)
The file was modified src/HOL/SPARK/Examples/RIPEMD-160/K_R.thy (diff)
The file was modified src/HOL/SPARK/Examples/RIPEMD-160/R_L.thy (diff)
The file was modified src/HOL/SPARK/Examples/RIPEMD-160/R_R.thy (diff)
The file was modified src/HOL/SPARK/Examples/RIPEMD-160/Round.thy (diff)
The file was modified src/HOL/SPARK/Examples/RIPEMD-160/S_L.thy (diff)
The file was modified src/HOL/SPARK/Examples/RIPEMD-160/S_R.thy (diff)
The file was modified src/HOL/SPARK/Examples/Sqrt/Sqrt.thy (diff)
The file was modified src/HOL/SPARK/Manual/Complex_Types.thy (diff)
The file was modified src/HOL/SPARK/Manual/Proc1.thy (diff)
The file was modified src/HOL/SPARK/Manual/Proc2.thy (diff)
The file was modified src/HOL/SPARK/Manual/Simple_Greatest_Common_Divisor.thy (diff)
The file was modified src/HOL/SPARK/SPARK_Setup.thy (diff)
The file was modified src/HOL/Semiring_Normalization.thy (diff)
The file was modified src/HOL/Sledgehammer.thy (diff)
The file was modified src/HOL/Statespace/DistinctTreeProver.thy (diff)
The file was modified src/HOL/Statespace/StateSpaceLocale.thy (diff)
The file was modified src/HOL/String.thy (diff)
The file was modified src/HOL/TPTP/ATP_Problem_Import.thy (diff)
The file was modified src/HOL/TPTP/ATP_Theory_Export.thy (diff)
The file was modified src/HOL/TPTP/MaSh_Eval.thy (diff)
The file was modified src/HOL/TPTP/MaSh_Export_Base.thy (diff)
The file was modified src/HOL/TPTP/TPTP_Interpret.thy (diff)
The file was modified src/HOL/TPTP/TPTP_Parser.thy (diff)
The file was modified src/HOL/TPTP/TPTP_Proof_Reconstruction.thy (diff)
The file was modified src/HOL/Transfer.thy (diff)
The file was modified src/HOL/Transitive_Closure.thy (diff)
The file was modified src/HOL/Typedef.thy (diff)
The file was modified src/HOL/Types_To_Sets/Types_To_Sets.thy (diff)
The file was modified src/HOL/UNITY/UNITY_Main.thy (diff)
The file was modified src/HOL/Word/Word.thy (diff)
The file was modified src/Sequents/LK.thy (diff)
The file was modified src/Sequents/Modal0.thy (diff)
The file was modified src/Sequents/Sequents.thy (diff)
The file was modified src/Tools/Code_Generator.thy (diff)
The file was modified src/Tools/SML/Examples.thy (diff)
The file was modified src/Tools/Spec_Check/Spec_Check.thy (diff)
The file was modified src/ZF/ArithSimp.thy (diff)
The file was modified src/ZF/Bin.thy (diff)
The file was modified src/ZF/Datatype.thy (diff)
The file was modified src/ZF/Inductive.thy (diff)
The file was modified src/ZF/pair.thy (diff)
The file was modified src/ZF/upair.thy (diff)
Changeset 69604:d80b2df54d31 by wenzelm:
isabelle update -u control_cartouches;
The file was modified src/HOL/Proofs/Extraction/Pigeonhole.thy (diff)
The file was modified src/HOL/ex/Cartouche_Examples.thy (diff)
Changeset 69603:67ae2e164c0f by wenzelm:
support for isabelle update -u path_cartouches;
The file was modified etc/options (diff)
The file was modified src/Doc/System/Sessions.thy (diff)
The file was modified src/Pure/Isar/token.scala (diff)
The file was modified src/Pure/Tools/update.scala (diff)
Changeset 69602:48e973251070 by wenzelm:
clarified documentation;
The file was modified src/Doc/System/Sessions.thy (diff)
Changeset 69601:c51a9bd4cf09 by wenzelm:
redundant (see isabelle.Dump.make_options);
The file was modified src/Doc/System/Sessions.thy (diff)
Changeset 69600:86e8e7347ac0 by nipkow:
typed definitions
The file was modified src/HOL/Analysis/Abstract_Topology.thy (diff)
The file was modified src/HOL/Analysis/Inner_Product.thy (diff)
The file was modified src/HOL/Analysis/L2_Norm.thy (diff)
The file was modified src/HOL/Analysis/Linear_Algebra.thy (diff)