Diffusion afp-devel 0d86fcd673f9

isabelle update_cartouches;
0d86fcd673f9
Actions

Description

isabelle update_cartouches;

Details

Provenance

makarius

Authored on

Parents

rAFP877ead9ac185: merge

Branches

Unknown

Tags

Unknown

Event Timeline

makarius committed rAFP0d86fcd673f9: isabelle update_cartouches;.Jan 8 2021, 4:17 PM

Changes (77)

Path

Size

thys/

Bicategory/

BicategoryOfSpans.thy

InternalAdjunction.thy

Pseudofunctor.thy

Subbicategory.thy

Binding_Syntax_Theory/

Equiv_Relation2.thy

Iteration.thy

Preliminaries.thy

QuasiTerms_Environments_Substitution.thy

QuasiTerms_PickFresh_Alpha.thy

QuasiTerms_Swap_Fresh.thy

Recursion.thy

Semantic_Domains.thy

Terms.thy

Transition_QuasiTerms_Terms.thy

Variable.thy

Well_Sorted_Terms.thy

Category3/

CartesianCategory.thy

Limit.thy

Chandy_Lamport/

Distributed_System.thy

Complex_Geometry/

Oriented_Circlines.thy

Unit_Circle_Preserving_Moebius.thy

Farkas/

Farkas.thy

Generalized_Counting_Sort/

Sorting.thy

Goedel_Incompleteness/

Abstract_First_Goedel_Rosser.thy

Deduction2.thy

Jeroslow_Original.thy

Standard_Model_More.thy

HOL-CSP/

Inductive_Inference/

Inductive_Inference_Basics.thy

LIM_BC.thy

Lemma_R.thy

Partial_Recursive.thy

Jacobson_Basic_Algebra/

Set_Theory.thy

LTL/

Disjunctive_Normal_Form.thy

LTL.thy

LTL_Master_Theorem/

Logical_Characterization/

Advice.thy

After.thy

Asymmetric_Master_Theorem.thy

Extra_Equivalence_Relations.thy

Master_Theorem.thy

Restricted_Master_Theorem.thy

Linear_Inequalities/

Convex_Hull.thy

Decomposition_Theorem.thy

Optics/

Poincare_Disc/

Poincare_Distance.thy

Poincare_Lines.thy

Poincare_Lines_Axis_Intersections.thy

Poincare_Lines_Ideal_Points.thy

Poincare_Tarski.thy

QHLProver/

Complex_Matrix.thy

Relational-Incorrectness-Logic/

RelationalIncorrectness.thy

Relational_Method/

Anonymity.thy

Authentication.thy

Safe_Distance/

Safe_Distance.thy

Safe_Distance_Reaction.thy

Syntax_Independent_Logic/

Szpilrajn/

rAFP0d86fcd673f9

View Options

thys/Bicategory/BicategoryOfSpans.thy

View Options

thys/Bicategory/InternalAdjunction.thy

View Options

thys/Bicategory/Pseudofunctor.thy

View Options

thys/Bicategory/Subbicategory.thy

View Options

thys/Binding_Syntax_Theory/Equiv_Relation2.thy

View Options

thys/Binding_Syntax_Theory/Iteration.thy

View Options

thys/Binding_Syntax_Theory/Preliminaries.thy

View Options

thys/Binding_Syntax_Theory/QuasiTerms_Environments_Substitution.thy

View Options

thys/Binding_Syntax_Theory/QuasiTerms_PickFresh_Alpha.thy

View Options

thys/Binding_Syntax_Theory/QuasiTerms_Swap_Fresh.thy

View Options

thys/Binding_Syntax_Theory/Recursion.thy

View Options

thys/Binding_Syntax_Theory/Semantic_Domains.thy

View Options

thys/Binding_Syntax_Theory/Terms.thy

View Options

thys/Binding_Syntax_Theory/Transition_QuasiTerms_Terms.thy

View Options

thys/Binding_Syntax_Theory/Variable.thy

View Options

thys/Binding_Syntax_Theory/Well_Sorted_Terms.thy

View Options

thys/Category3/CartesianCategory.thy

View Options

thys/Category3/Limit.thy

View Options

thys/Chandy_Lamport/Distributed_System.thy

View Options

thys/Chandy_Lamport/Example.thy

View Options

thys/Chandy_Lamport/Snapshot.thy

View Options

thys/Chandy_Lamport/Swap.thy

View Options

thys/Chandy_Lamport/Trace.thy

View Options

thys/Complex_Geometry/Angles.thy

View Options

thys/Complex_Geometry/Linear_Systems.thy

View Options

thys/Complex_Geometry/Oriented_Circlines.thy

View Options

thys/Complex_Geometry/Unit_Circle_Preserving_Moebius.thy

View Options

thys/Farkas/Farkas.thy

View Options

thys/Generalized_Counting_Sort/Sorting.thy

View Options

thys/Goedel_Incompleteness/Abstract_First_Goedel_Rosser.thy

View Options

thys/Goedel_Incompleteness/Deduction2.thy

View Options

thys/Goedel_Incompleteness/Jeroslow_Original.thy

View Options

thys/Goedel_Incompleteness/Standard_Model_More.thy

View Options

thys/HOL-CSP/Mndet.thy

View Options

thys/HOL-CSP/Mprefix.thy

View Options

thys/Inductive_Inference/CONS_LIM.thy

View Options

thys/Inductive_Inference/CP_FIN_NUM.thy

View Options

thys/Inductive_Inference/Inductive_Inference_Basics.thy

View Options

thys/Inductive_Inference/LIM_BC.thy

View Options

thys/Inductive_Inference/Lemma_R.thy

View Options

thys/Inductive_Inference/Partial_Recursive.thy

View Options

thys/Inductive_Inference/R1_BC.thy

View Options

thys/Inductive_Inference/Standard_Results.thy

View Options

thys/Inductive_Inference/TOTAL_CONS.thy

View Options

thys/Inductive_Inference/Union.thy

View Options

thys/Inductive_Inference/Universal.thy

View Options

thys/Jacobson_Basic_Algebra/Set_Theory.thy

View Options

thys/LTL/Disjunctive_Normal_Form.thy

View Options

thys/LTL/LTL.thy

View Options

thys/LTL_Master_Theorem/Logical_Characterization/Advice.thy

View Options

thys/LTL_Master_Theorem/Logical_Characterization/After.thy

View Options

thys/LTL_Master_Theorem/Logical_Characterization/Asymmetric_Master_Theorem.thy

View Options

thys/LTL_Master_Theorem/Logical_Characterization/Extra_Equivalence_Relations.thy

View Options

thys/LTL_Master_Theorem/Logical_Characterization/Master_Theorem.thy

View Options

thys/LTL_Master_Theorem/Logical_Characterization/Restricted_Master_Theorem.thy

View Options

thys/Linear_Inequalities/Convex_Hull.thy

View Options

thys/Linear_Inequalities/Decomposition_Theorem.thy

View Options

thys/Linear_Inequalities/Integer_Hull.thy

View Options

thys/Optics/Two.thy

View Options

thys/Poincare_Disc/Poincare_Between.thy

View Options

thys/Poincare_Disc/Poincare_Circles.thy

View Options

thys/Poincare_Disc/Poincare_Distance.thy

View Options

thys/Poincare_Disc/Poincare_Lines.thy

View Options

thys/Poincare_Disc/Poincare_Lines_Axis_Intersections.thy

View Options

thys/Poincare_Disc/Poincare_Lines_Ideal_Points.thy

View Options

thys/Poincare_Disc/Poincare_Tarski.thy

View Options

thys/QHLProver/Complex_Matrix.thy

View Options

thys/Relational-Incorrectness-Logic/RelationalIncorrectness.thy

View Options

thys/Relational_Method/Anonymity.thy

View Options

thys/Relational_Method/Authentication.thy

View Options

thys/Safe_Distance/Safe_Distance.thy

View Options

thys/Safe_Distance/Safe_Distance_Reaction.thy

View Options

thys/Syntax_Independent_Logic/Deduction.thy

View Options

thys/Syntax_Independent_Logic/Deduction_Q.thy

View Options

thys/Syntax_Independent_Logic/Syntax.thy

View Options

thys/Syntax_Independent_Logic/Syntax_Arith.thy

View Options

thys/Szpilrajn/Szpilrajn.thy

isabelle update_cartouches;0d86fcd673f9Actions

Description

Details

Event Timeline

Changes (77)

rAFP0d86fcd673f9

thys/Bicategory/BicategoryOfSpans.thy

thys/Bicategory/InternalAdjunction.thy

thys/Bicategory/Pseudofunctor.thy

thys/Bicategory/Subbicategory.thy

thys/Binding_Syntax_Theory/Equiv_Relation2.thy

thys/Binding_Syntax_Theory/Iteration.thy

thys/Binding_Syntax_Theory/Preliminaries.thy

thys/Binding_Syntax_Theory/QuasiTerms_Environments_Substitution.thy

thys/Binding_Syntax_Theory/QuasiTerms_PickFresh_Alpha.thy

thys/Binding_Syntax_Theory/QuasiTerms_Swap_Fresh.thy

thys/Binding_Syntax_Theory/Recursion.thy

thys/Binding_Syntax_Theory/Semantic_Domains.thy

thys/Binding_Syntax_Theory/Terms.thy

thys/Binding_Syntax_Theory/Transition_QuasiTerms_Terms.thy

thys/Binding_Syntax_Theory/Variable.thy

thys/Binding_Syntax_Theory/Well_Sorted_Terms.thy

thys/Category3/CartesianCategory.thy

thys/Category3/Limit.thy

thys/Chandy_Lamport/Distributed_System.thy

thys/Chandy_Lamport/Example.thy

thys/Chandy_Lamport/Snapshot.thy

thys/Chandy_Lamport/Swap.thy

thys/Chandy_Lamport/Trace.thy

thys/Complex_Geometry/Angles.thy

thys/Complex_Geometry/Linear_Systems.thy

thys/Complex_Geometry/Oriented_Circlines.thy

thys/Complex_Geometry/Unit_Circle_Preserving_Moebius.thy

thys/Farkas/Farkas.thy

thys/Generalized_Counting_Sort/Sorting.thy

thys/Goedel_Incompleteness/Abstract_First_Goedel_Rosser.thy

thys/Goedel_Incompleteness/Deduction2.thy

thys/Goedel_Incompleteness/Jeroslow_Original.thy

thys/Goedel_Incompleteness/Standard_Model_More.thy

thys/HOL-CSP/Mndet.thy

thys/HOL-CSP/Mprefix.thy

thys/Inductive_Inference/CONS_LIM.thy

thys/Inductive_Inference/CP_FIN_NUM.thy

thys/Inductive_Inference/Inductive_Inference_Basics.thy

thys/Inductive_Inference/LIM_BC.thy

thys/Inductive_Inference/Lemma_R.thy

thys/Inductive_Inference/Partial_Recursive.thy

thys/Inductive_Inference/R1_BC.thy

thys/Inductive_Inference/Standard_Results.thy

thys/Inductive_Inference/TOTAL_CONS.thy

thys/Inductive_Inference/Union.thy

thys/Inductive_Inference/Universal.thy

thys/Jacobson_Basic_Algebra/Set_Theory.thy

thys/LTL/Disjunctive_Normal_Form.thy

thys/LTL/LTL.thy

thys/LTL_Master_Theorem/Logical_Characterization/Advice.thy

thys/LTL_Master_Theorem/Logical_Characterization/After.thy

thys/LTL_Master_Theorem/Logical_Characterization/Asymmetric_Master_Theorem.thy

thys/LTL_Master_Theorem/Logical_Characterization/Extra_Equivalence_Relations.thy

thys/LTL_Master_Theorem/Logical_Characterization/Master_Theorem.thy

thys/LTL_Master_Theorem/Logical_Characterization/Restricted_Master_Theorem.thy

thys/Linear_Inequalities/Convex_Hull.thy

thys/Linear_Inequalities/Decomposition_Theorem.thy

thys/Linear_Inequalities/Integer_Hull.thy

thys/Optics/Two.thy

thys/Poincare_Disc/Poincare_Between.thy

thys/Poincare_Disc/Poincare_Circles.thy

thys/Poincare_Disc/Poincare_Distance.thy

thys/Poincare_Disc/Poincare_Lines.thy

thys/Poincare_Disc/Poincare_Lines_Axis_Intersections.thy

thys/Poincare_Disc/Poincare_Lines_Ideal_Points.thy

thys/Poincare_Disc/Poincare_Tarski.thy

thys/QHLProver/Complex_Matrix.thy

thys/Relational-Incorrectness-Logic/RelationalIncorrectness.thy

thys/Relational_Method/Anonymity.thy

thys/Relational_Method/Authentication.thy

thys/Safe_Distance/Safe_Distance.thy

thys/Safe_Distance/Safe_Distance_Reaction.thy

thys/Syntax_Independent_Logic/Deduction.thy

thys/Syntax_Independent_Logic/Deduction_Q.thy

isabelle update_cartouches;
0d86fcd673f9
Actions