Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. tuned proofs -- avoid improper use of "this";
  3. tuned;
  4. tuned;
Changeset 6970:4f3f5fe3f628 by wenzelm:
merged
Changeset 6969:3321e1bc3d3a by wenzelm:
tuned proofs -- avoid improper use of "this";
The file was modified thys/AWN/AWN_Invariants.thy (diff)
The file was modified thys/AWN/OAWN_Invariants.thy (diff)
The file was modified thys/AWN/ONode_Lifting.thy (diff)
The file was modified thys/AWN/Pnet.thy (diff)
The file was modified thys/AWN/Toy.thy (diff)
The file was modified thys/Akra_Bazzi/Akra_Bazzi.thy (diff)
The file was modified thys/Akra_Bazzi/Akra_Bazzi_Real.thy (diff)
The file was modified thys/Bell_Numbers_Spivey/Set_Partition.thy (diff)
The file was modified thys/Buildings/Algebra.thy (diff)
The file was modified thys/Buildings/Chamber.thy (diff)
The file was modified thys/Call_Arity/CoCallGraph-TTree.thy (diff)
The file was modified thys/Category3/Adjunction.thy (diff)
The file was modified thys/Category3/Category.thy (diff)
The file was modified thys/Category3/EpiMonoIso.thy (diff)
The file was modified thys/Category3/FreeCategory.thy (diff)
The file was modified thys/Category3/Limit.thy (diff)
The file was modified thys/Category3/SetCategory.thy (diff)
The file was modified thys/Collections/GenCF/Impl/Impl_List_Map.thy (diff)
The file was modified thys/Density_Compiler/PDF_Compiler.thy (diff)
The file was modified thys/Dependent_SIFUM_Refinement/CompositionalRefinement.thy (diff)
The file was modified thys/Descartes_Sign_Rule/Descartes_Sign_Rule.thy (diff)
The file was modified thys/Encodability_Process_Calculi/CombinedCriteria.thy (diff)
The file was modified thys/Encodability_Process_Calculi/OperationalCorrespondence.thy (diff)
The file was modified thys/Formal_SSA/Minimality.thy (diff)
The file was modified thys/JinjaThreads/BV/BVProgressThreaded.thy (diff)
The file was modified thys/JinjaThreads/Compiler/JVMJ1.thy (diff)
The file was modified thys/JinjaThreads/MM/JMM_Common.thy (diff)
The file was modified thys/List_Interleaving/ListInterleaving.thy (diff)
The file was modified thys/Markov_Models/MDP_Reachability_Problem.thy (diff)
The file was modified thys/Noninterference_CSP/CSPNoninterference.thy (diff)
The file was modified thys/Noninterference_CSP/ClassicalNoninterference.thy (diff)
The file was modified thys/Noninterference_Generic_Unwinding/GenericUnwinding.thy (diff)
The file was modified thys/Noninterference_Inductive_Unwinding/InductiveUnwinding.thy (diff)
The file was modified thys/Noninterference_Ipurge_Unwinding/IpurgeUnwinding.thy (diff)
The file was modified thys/Ordinary_Differential_Equations/IVP/Flow.thy (diff)
The file was modified thys/Ordinary_Differential_Equations/IVP/Initial_Value_Problem.thy (diff)
The file was modified thys/Probabilistic_Noninterference/Trace_Based.thy (diff)
The file was modified thys/Program-Conflict-Analysis/ConstraintSystems.thy (diff)
The file was modified thys/Promela/Promela.thy (diff)
The file was modified thys/Randomised_Social_Choice/Automation/SDS_Automation.thy (diff)
The file was modified thys/Randomised_Social_Choice/Order_Predicates.thy (diff)
The file was modified thys/Randomised_Social_Choice/Preference_Profiles.thy (diff)
The file was modified thys/Randomised_Social_Choice/SDS_Lowering.thy (diff)
The file was modified thys/Randomised_Social_Choice/Utility_Functions.thy (diff)
The file was modified thys/RefinementReactive/Reactive.thy (diff)
The file was modified thys/Simpl/AlternativeSmallStep.thy (diff)
The file was modified thys/Simpl/HoarePartialDef.thy (diff)
The file was modified thys/Simpl/HoarePartialProps.thy (diff)
The file was modified thys/Simpl/HoareTotalProps.thy (diff)
The file was modified thys/Simpl/Termination.thy (diff)
The file was modified thys/Simpl/ex/Compose.thy (diff)
The file was modified thys/Slicing/Basic/Postdomination.thy (diff)
The file was modified thys/Stern_Brocot/Stern_Brocot_Tree.thy (diff)
The file was modified thys/Sturm_Sequences/Sturm_Theorem.thy (diff)
The file was modified thys/Tail_Recursive_Functions/CaseStudy1.thy (diff)
The file was modified thys/Timed_Automata/Approx_Beta.thy (diff)
The file was modified thys/Timed_Automata/Closure.thy (diff)
The file was modified thys/Timed_Automata/Paths_Cycles.thy (diff)
The file was modified thys/UpDown_Scheme/Grid.thy (diff)
Changeset 6968:4b49f3162a7d by wenzelm:
tuned;
The file was modified thys/Noninterference_Generic_Unwinding/ROOT (diff)
Changeset 6967:6c64eaaee638 by wenzelm:
tuned;
The file was modified thys/Category3/ROOT (diff)
The file was modified thys/List_Interleaving/ROOT (diff)
The file was modified thys/Noninterference_Inductive_Unwinding/ROOT (diff)
The file was modified thys/RefinementReactive/ROOT (diff)
The file was modified thys/Tail_Recursive_Functions/ROOT (diff)