Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. minimum of maintainability for proof
  2. tuned proofs
  3. dropped various legacy fact bindings and tuned proofs
  4. separated potentially conflicting type class instance into separate theory
  5. accommodated gcd instances for polynomials
  6. more sophisticated GCD syntax
  7. dropped various legacy fact bindings
  8. prefer abbreviations for compound operators INFIMUM and SUPREMUM
Changeset 6336:5e250f26ad4f by haftmann:
minimum of maintainability for proof
The file was modified thys/List_Update/RExp_Var.thy (diff)
Changeset 6335:c049cd8d1630 by haftmann:
tuned proofs
The file was modified thys/Regular-Sets/Regular_Set.thy (diff)
Changeset 6334:63f5e1c0aa64 by haftmann:
dropped various legacy fact bindings and tuned proofs
The file was modified thys/Case_Labeling/Examples/Monadic_Language.thy (diff)
The file was modified thys/Echelon_Form/Euclidean_Algorithm.thy (diff)
Changeset 6333:f7ed37faace8 by haftmann:
separated potentially conflicting type class instance into separate theory
The file was modified thys/Descartes_Sign_Rule/Descartes_Sign_Rule.thy (diff)
The file was modified thys/Echelon_Form/Euclidean_Algorithm_Extension.thy (diff)
The file was modified thys/Liouville_Numbers/Liouville_Numbers.thy (diff)
The file was modified thys/Liouville_Numbers/Liouville_Numbers_Misc.thy (diff)
The file was modified thys/Liouville_Numbers/ROOT (diff)
The file was modified thys/Polynomial_Factorization/Order_Polynomial.thy (diff)
The file was modified thys/Polynomial_Factorization/ROOT (diff)
The file was modified thys/Rep_Fin_Groups/Rep_Fin_Groups.thy (diff)
The file was modified thys/Sturm_Sequences/Lib/Misc_Polynomial.thy (diff)
The file was modified thys/Sturm_Sequences/Sturm_Theorem.thy (diff)
The file was modified thys/Sturm_Tarski/PolyMisc.thy (diff)
The file was modified thys/Sturm_Tarski/ROOT (diff)
Changeset 6332:ffa326517429 by haftmann:
accommodated gcd instances for polynomials
The file was modified thys/Echelon_Form/Euclidean_Algorithm_Extension.thy (diff)
The file was modified thys/Lehmer/Multiplicative_Group.thy (diff)
The file was modified thys/Markov_Models/Classifying_Markov_Chain_States.thy (diff)
The file was modified thys/Markov_Models/ex/Example_A.thy (diff)
The file was modified thys/Markov_Models/ex/Example_B.thy (diff)
The file was modified thys/Perfect-Number-Thm/PerfectBasics.thy (diff)
The file was modified thys/Perfect-Number-Thm/Sigma.thy (diff)
The file was modified thys/Real_Impl/Prime_Product.thy (diff)
The file was modified thys/Secondary_Sylow/SndSylow.thy (diff)
The file was modified thys/Sturm_Sequences/Lib/Misc_Polynomial.thy (diff)
The file was modified thys/Sturm_Tarski/Sturm_Tarski.thy (diff)
Changeset 6331:273ef38505c7 by haftmann:
more sophisticated GCD syntax
The file was modified thys/Polynomial_Factorization/Square_Free_Factorization.thy (diff)
Changeset 6330:4112e5cd5994 by haftmann:
dropped various legacy fact bindings
The file was modified thys/Algebraic_Numbers/Algebraic_Numbers_Prelim.thy (diff)
The file was modified thys/BDD/General.thy (diff)
The file was modified thys/BDD/NormalizeTotalProof.thy (diff)
The file was modified thys/Echelon_Form/Euclidean_Algorithm_Extension.thy (diff)
The file was modified thys/Featherweight_OCL/src/collection_types/UML_Set.thy (diff)
The file was modified thys/Fermat3_4/Fermat4.thy (diff)
The file was modified thys/Fermat3_4/IntNatAux.thy (diff)
The file was modified thys/Fermat3_4/QuadForm.thy (diff)
The file was modified thys/FunWithFunctions/FunWithFunctions.thy (diff)
The file was modified thys/Group-Ring-Module/Algebra1.thy (diff)
The file was modified thys/Group-Ring-Module/Algebra4.thy (diff)
The file was modified thys/Group-Ring-Module/Algebra6.thy (diff)
The file was modified thys/Impossible_Geometry/Impossible_Geometry.thy (diff)
The file was modified thys/JinjaThreads/J/Progress.thy (diff)
The file was modified thys/Knot_Theory/Tangle_Algebra.thy (diff)
The file was modified thys/Lehmer/Lehmer.thy (diff)
The file was modified thys/Lehmer/Multiplicative_Group.thy (diff)
The file was modified thys/List_Update/Move_to_Front.thy (diff)
The file was modified thys/Native_Word/Word_Misc.thy (diff)
The file was modified thys/Ordinary_Differential_Equations/Numerics/Optimize_Float.thy (diff)
The file was modified thys/Perfect-Number-Thm/Perfect.thy (diff)
The file was modified thys/Perfect-Number-Thm/Sigma.thy (diff)
The file was modified thys/Planarity_Certificates/Planarity/Executable_Permutations.thy (diff)
The file was modified thys/Planarity_Certificates/Planarity/Graph_Genus.thy (diff)
The file was modified thys/Polynomial_Factorization/Gauss_Lemma.thy (diff)
The file was modified thys/Polynomial_Factorization/Prime_Factorization.thy (diff)
The file was modified thys/Polynomial_Factorization/Square_Free_Factorization.thy (diff)
The file was modified thys/Polynomial_Factorization/Unique_Factorization_Domain.thy (diff)
The file was modified thys/Polynomial_Interpolation/Missing_Polynomial.thy (diff)
The file was modified thys/Polynomial_Interpolation/Missing_Unsorted.thy (diff)
The file was modified thys/Rank_Nullity_Theorem/Mod_Type.thy (diff)
The file was modified thys/Real_Impl/Prime_Product.thy (diff)
The file was modified thys/Real_Impl/Real_Impl.thy (diff)
The file was modified thys/Sqrt_Babylonian/NthRoot_Impl.thy (diff)
The file was modified thys/Stern_Brocot/Bird_Tree.thy (diff)
The file was modified thys/Stern_Brocot/Stern_Brocot_Tree.thy (diff)
The file was modified thys/SumSquares/FourSquares.thy (diff)
The file was modified thys/Valuation/Valuation1.thy (diff)
The file was modified thys/Valuation/Valuation2.thy (diff)
The file was modified thys/Valuation/Valuation3.thy (diff)
The file was modified thys/Well_Quasi_Orders/Multiset_Extension.thy (diff)
The file was modified thys/pGCL/Determinism.thy (diff)
The file was modified thys/pGCL/Tutorial/Monty.thy (diff)
Changeset 6329:2920922afe7d by haftmann:
prefer abbreviations for compound operators INFIMUM and SUPREMUM
The file was modified thys/Call_Arity/TTree-HOLCF.thy (diff)
The file was modified thys/Coinductive/Coinductive_List.thy (diff)
The file was modified thys/Coinductive/Coinductive_Nat.thy (diff)
The file was modified thys/Coinductive/Coinductive_Stream.thy (diff)
The file was modified thys/Coinductive/Complete_Partial_Order2.thy (diff)
The file was modified thys/Coinductive/Examples/CCPO_Topology.thy (diff)
The file was modified thys/Coinductive/TLList_CCPO.thy (diff)
The file was modified thys/Collections/Lib/Robdd.thy (diff)
The file was modified thys/Consensus_Refined/Consensus_Misc.thy (diff)
The file was modified thys/Containers/Set_Impl.thy (diff)
The file was modified thys/DataRefinementIBP/DataRefinement.thy (diff)
The file was modified thys/DataRefinementIBP/Diagram.thy (diff)
The file was modified thys/DataRefinementIBP/Hoare.thy (diff)
The file was modified thys/Decreasing-Diagrams-II/Decreasing_Diagrams_II.thy (diff)
The file was modified thys/DiskPaxos/DiskPaxos_Inv5.thy (diff)
The file was modified thys/Ergodic_Theory/Recurrence.thy (diff)
The file was modified thys/Ergodic_Theory/SG_Library_Complement.thy (diff)
The file was modified thys/FOL-Fitting/FOL_Fitting.thy (diff)
The file was modified thys/Flyspeck-Tame/PlaneGraphIso.thy (diff)
The file was modified thys/Flyspeck-Tame/PlaneProps.thy (diff)
The file was modified thys/Gabow_SCC/Gabow_GBG.thy (diff)
The file was modified thys/Girth_Chromatic/Ugraphs.thy (diff)
The file was modified thys/Graph_Theory/Shortest_Path.thy (diff)
The file was modified thys/Graph_Theory/Stuff.thy (diff)
The file was modified thys/Inductive_Confidentiality/DolevYao/ConfidentialityDY.thy (diff)
The file was modified thys/Integration/Integral.thy (diff)
The file was modified thys/Integration/Measure.thy (diff)
The file was modified thys/Jinja/Common/TypeRel.thy (diff)
The file was modified thys/JinjaThreads/Common/TypeRel.thy (diff)
The file was modified thys/JinjaThreads/Execute/ExternalCall_Execute.thy (diff)
The file was modified thys/JinjaThreads/Execute/Scheduler.thy (diff)
The file was modified thys/Jordan_Normal_Form/Jordan_Normal_Form.thy (diff)
The file was modified thys/KBPs/Kripke.thy (diff)
The file was modified thys/Koenigsberg_Friendship/FriendshipTheory.thy (diff)
The file was modified thys/LTL_to_DRA/Impl/LTL_Rabin_Impl.thy (diff)
The file was modified thys/LTL_to_DRA/LTL_Rabin.thy (diff)
The file was modified thys/LatticeProperties/Complete_Lattice_Prop.thy (diff)
The file was modified thys/LinearQuantifierElim/Thys/QElin.thy (diff)
The file was modified thys/Locally-Nameless-Sigma/Sigma/Sigma.thy (diff)
The file was modified thys/Lower_Semicontinuous/Lower_Semicontinuous.thy (diff)
The file was modified thys/MSO_Regex_Equivalence/Pi_Derivatives.thy (diff)
The file was modified thys/Markov_Models/MDP_Reachability_Problem.thy (diff)
The file was modified thys/Markov_Models/Markov_Decision_Process.thy (diff)
The file was modified thys/MonoBoolTranAlgebra/Assertion_Algebra.thy (diff)
The file was modified thys/MonoBoolTranAlgebra/Mono_Bool_Tran.thy (diff)
The file was modified thys/MonoBoolTranAlgebra/Mono_Bool_Tran_Algebra.thy (diff)
The file was modified thys/MonoBoolTranAlgebra/Statements.thy (diff)
The file was modified thys/Multirelations/Multirelations.thy (diff)
The file was modified thys/Myhill-Nerode/Closures.thy (diff)
The file was modified thys/Nat-Interval-Logic/IL_Interval.thy (diff)
The file was modified thys/Network_Security_Policy_Verification/TopoS_Composition_Theory.thy (diff)
The file was modified thys/Nominal2/Nominal2_Base.thy (diff)
The file was modified thys/Ordinal/OrdinalVeblen.thy (diff)
The file was modified thys/PCF/Dual_Lattice.thy (diff)
The file was modified thys/Planarity_Certificates/Planarity/Digraph_Map_Impl.thy (diff)
The file was modified thys/Presburger-Automata/Presburger_Automata.thy (diff)
The file was modified thys/Probabilistic_Noninterference/Language_Semantics.thy (diff)
The file was modified thys/Program-Conflict-Analysis/ConsInterleave.thy (diff)
The file was modified thys/Promela/PromelaInvariants.thy (diff)
The file was modified thys/Refine_Monadic/Generic/RefineG_Recursion.thy (diff)
The file was modified thys/Refine_Monadic/Refine_Basic.thy (diff)
The file was modified thys/Refine_Monadic/Refine_Foreach.thy (diff)
The file was modified thys/Refine_Monadic/Refine_Misc.thy (diff)
The file was modified thys/Refine_Monadic/Refine_Pfun.thy (diff)
The file was modified thys/Refine_Monadic/Refine_Transfer.thy (diff)
The file was modified thys/RefinementReactive/Refinement.thy (diff)
The file was modified thys/RefinementReactive/Temporal.thy (diff)
The file was modified thys/Regex_Equivalence/After2.thy (diff)
The file was modified thys/Regex_Equivalence/Derivatives_Finite.thy (diff)
The file was modified thys/Regular-Sets/Derivatives.thy (diff)
The file was modified thys/Regular-Sets/Regular_Set.thy (diff)
The file was modified thys/Rep_Fin_Groups/Rep_Fin_Groups.thy (diff)
The file was modified thys/Simpl/hoare.ML (diff)
The file was modified thys/Statecharts/HA.thy (diff)
The file was modified thys/Statecharts/HAOps.thy (diff)
The file was modified thys/Statecharts/HASem.thy (diff)
The file was modified thys/Verified-Prover/Prover.thy (diff)
The file was modified thys/Vickrey_Clarke_Groves/CombinatorialAuction.thy (diff)
The file was modified thys/Vickrey_Clarke_Groves/Partitions.thy (diff)
The file was modified thys/Vickrey_Clarke_Groves/Universes.thy (diff)
The file was modified thys/pGCL/Continuity.thy (diff)
The file was modified thys/pGCL/Healthiness.thy (diff)
The file was modified thys/pGCL/LoopInduction.thy (diff)
The file was modified thys/pGCL/StructuredReasoning.thy (diff)
The file was modified thys/pGCL/Sublinearity.thy (diff)