Diffusion afp-devel 1668bf4eba40

So…
1668bf4eba40
Actions

Description

Automated merge with bundle:/var/folders/9z/l1x9y3bd16x9_70pdp4703jr0000gp/T/SourceTreeTemp.3gPj1U

Details

Provenance

paulson <lp15@cam.ac.uk>

Authored on

Parents

rAFPef2cf009504d: Tidied auto/simp with null arguments
rAFP173359fcafa4: merged

Branches

Unknown

Tags

Unknown

Event Timeline

paulson <lp15@cam.ac.uk> committed rAFP1668bf4eba40: Automated merge with bundle:/var/folders/9z/l1x9y3bd16x9_70pdp4703jr0000gp/T/So….May 17 2022, 3:11 PM

Merged Changes

This commit merges a very large number of changes. Only the first 50 are shown.

173359fcafa4 merged
Author
nipkow
Browse Repository
No Builds
No Audits
3ec6dc59412e comleted single loop refinement
Author
nipkow
Browse Repository
No Builds
No Audits
d0c948a42af2 merged
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
00c034528a4a clarified formatting, for the sake of scala3;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
dbddab778577 merged
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
e3c2aeafc2c0 merged
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
fbafb44dc503 hugo site: better scrolling;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
1be19de7eecb hugo site: updated devel info;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
38314be41f9f hugo site: updated content;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
3e574f15c9bf hugo site: proper ordering;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
2ad5e37aebc5 hugo site: restricted generated affiliations;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
16c8b18bede4 hugo site: proper theory view link scrolling;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
d406e40678a5 hugo site: tuned affiliation keys;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
244ac17a6498 hugo site: proper topic-only topics page;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
fc2d817db048 hugo site: relativize paths;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
d1a781d9fb9c hugo site: list sessions separately;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
9f4523b8ed97 hugo site: tuned;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
0f50a79d8721 hugo site: tuned;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
79e043c174f0 hugo site: merge gen and build tool;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
e56a3c69ae27 hugo site: added doc headers;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
51c88bc0b376 hugo site: tuned;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
8d67d9a9da75 afp metadata: index keys for emails and urls;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
e4b3556a40fe hugo site: improve theory view;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
0dd4c34b22d5 hugo site: cleaned up;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
6091eddc9db6 hugo site: added devel version;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
fef45c5031a4 hugo site: updated search and content;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
9192b15831b3 hugo site: added theory view styling for different device sizes;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
f1fb5d9cc8b2 Updated metadata in migration and theory view;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
8f595e5bd261 hugo site: updated site templates;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
09a3e2523fd9 metadata migration: updated authors;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
bd32b1fd6406 merged
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
d80eeff3bd7d hugo: added mobile view;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
9be5074d44ca hugo: copy to proper path;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
080b665e6ae3 added theory navbar;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
2bcb6698a17e tuned formatting;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
1266c86cf47b added loader;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
b30cbcc1846c tuned;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
d6ff995cf5a9 tuned: more canonical Isabelle code style;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
b32649b547e9 proper loading of foundational hrefs;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
53e6f3897fff fix dependencies;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
ab1cf8fca876 added devel flag;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
cc835fde7a38 updated about page;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
5f2eb2ceef51 moved extraction of related entries to hugo;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
a53823fdccd8 improved keyword extraction;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
cea71b734a23 added keywords to site generated entry data;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
b69b09d8f99a use tmp file for python script instead of command;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
e450d45c4680 added js-side theory loading to afp site;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
5857c4582eae integrated metadata changes into site;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
09790a81f454 added missing keyword data;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
5369b980e2fe removed html dir from sitegen (now set inside hugo);
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits

Changes (88)

Path

Size

thys/

Affine_Arithmetic/

Affine_Approximation.thy

Counterclockwise_2D_Arbitrary.thy

Counterclockwise_2D_Strict.thy

Executable_Euclidean_Space.thy

Floatarith_Expression.thy

Intersection.thy

Polygon.thy

Straight_Line_Program.thy

Amicable_Numbers/

Amicable_Numbers.thy

Collections/

Examples/

Autoref/

Simple_DFS.thy

Complex_Bounded_Operators/

Cblinfun_Code.thy

One_Dimensional_Spaces.thy

Complx/

OG_Soundness.thy

ex/

Examples.thy

Core_DOM/

standard/

Core_DOM_Heap_WF.thy

Core_SC_DOM/

safely_composable/

Core_DOM_Heap_WF.thy

Dirichlet_L/

Dirichlet_L_Functions.thy

Dynamic_Tables/

Tables_nat.thy

Extended_Finite_State_Machines/

EFSM_LTL.thy

examples/

Drinks_Machine_LTL.thy

FO_Theory_Rewriting/

Util/

Multihole_Context.thy

Flow_Networks/

Residual_Graph.thy

Goedel_HFSet_Semanticless/

Sigma.thy

Graph_Theory/

Digraph_Isomorphism.thy

Kuratowski.thy

Green/

Integrals.thy

Hoare_Time/

Big_StepT_Partial.thy

IP_Addresses/

WordInterval.thy

Incompleteness/

Sigma.thy

Iptables_Semantics/

Primitive_Matchers/

Lambert_W/

Laplace_Transform/

List_Update/

MFMC_Countable/

MFMC_Flow_Attainability.thy

MFMC_Unbounded.thy

MFMC_Web.thy

Markov_Models/

Continuous_Time_Markov_Chain.thy

ex/

PCTL.thy

Ordinary_Differential_Equations/

Ex/

Lorenz/

Lorenz_Approximation.thy

IVP/

Cones.thy

Flow.thy

Flow_Congs.thy

Picard_Lindeloef_Qualitative.thy

Poincare_Map.thy

Upper_Lower_Solution.thy

Library/

Linear_ODE.thy

Numerics/

Concrete_Reachability_Analysis.thy

Concrete_Reachability_Analysis_C1.thy

Concrete_Rigorous_Numerics.thy

Example_Utilities.thy

Init_ODE_Solver.thy

Refine_Reachability_Analysis.thy

Refine_Reachability_Analysis_C1.thy

Refine_Rigorous_Numerics_Aform.thy

Transfer_Euclidean_Space_Vector.thy

ODE_Auxiliarities.thy

Refinement/

Refine_Vector_List.thy

Weak_Set.thy

PAC_Checker/

PAC_More_Poly.thy

Planarity_Certificates/

Planarity/

Graph_Genus.thy

Poincare_Bendixson/

Analysis_Misc.thy

ODE_Misc.thy

Poincare_Bendixson.thy

Random_BSTs/

Random_BSTs.thy

Refine_Imperative_HOL/

IICF/

Impl/

Heaps/

IICF_Abs_Heap.thy

IICF_Abs_Heapmap.thy

SC_DOM_Components/

Core_DOM_SC_DOM_Components.thy

Security_Protocol_Refinement/

Refinement/

Smooth_Manifolds/

Stirling_Formula/

Gamma_Asymptotics.thy

Sturm_Sequences/

Sturm_Method.thy

Taylor_Models/

Taylor_Models.thy

VerifyThis2019/

Challenge3.thy

Virtual_Substitution/

Debruijn.thy

EliminateVariable.thy

ExecutiblePolyProps.thy

rAFP1668bf4eba40

View Options

thys/Affine_Arithmetic/Affine_Approximation.thy

View Options

thys/Affine_Arithmetic/Counterclockwise_2D_Arbitrary.thy

View Options

thys/Affine_Arithmetic/Counterclockwise_2D_Strict.thy

View Options

thys/Affine_Arithmetic/Executable_Euclidean_Space.thy

View Options

thys/Affine_Arithmetic/Floatarith_Expression.thy

View Options

thys/Affine_Arithmetic/Intersection.thy

View Options

thys/Affine_Arithmetic/Polygon.thy

View Options

thys/Affine_Arithmetic/Straight_Line_Program.thy

View Options

thys/Amicable_Numbers/Amicable_Numbers.thy

View Options

thys/Collections/Examples/Autoref/Simple_DFS.thy

View Options

thys/Complex_Bounded_Operators/Cblinfun_Code.thy

View Options

thys/Complex_Bounded_Operators/One_Dimensional_Spaces.thy

View Options

thys/Complx/OG_Soundness.thy

View Options

thys/Complx/ex/Examples.thy

View Options

thys/Core_DOM/standard/Core_DOM_Heap_WF.thy

View Options

thys/Core_SC_DOM/safely_composable/Core_DOM_Heap_WF.thy

View Options

thys/Dirichlet_L/Dirichlet_L_Functions.thy

View Options

thys/Dynamic_Tables/Tables_nat.thy

View Options

thys/Extended_Finite_State_Machines/EFSM_LTL.thy

View Options

thys/Extended_Finite_State_Machines/examples/Drinks_Machine_LTL.thy

View Options

thys/FO_Theory_Rewriting/Util/Multihole_Context.thy

View Options

thys/Flow_Networks/Residual_Graph.thy

View Options

thys/Goedel_HFSet_Semanticless/Sigma.thy

View Options

thys/Graph_Theory/Digraph_Isomorphism.thy

View Options

thys/Graph_Theory/Kuratowski.thy

View Options

thys/Green/Integrals.thy

View Options

thys/Hoare_Time/Big_StepT_Partial.thy

View Options

thys/IP_Addresses/WordInterval.thy

View Options

thys/Incompleteness/Sigma.thy

View Options

thys/Iptables_Semantics/Primitive_Matchers/IpAddresses.thy

View Options

thys/Lambert_W/Lambert_W.thy

View Options

thys/Laplace_Transform/Existence.thy

View Options

thys/List_Update/BIT.thy

View Options

thys/List_Update/List_Factoring.thy

View Options

thys/List_Update/Prob_Theory.thy

View Options

thys/List_Update/TS.thy

View Options

thys/MFMC_Countable/MFMC_Flow_Attainability.thy

View Options

thys/MFMC_Countable/MFMC_Unbounded.thy

View Options

thys/MFMC_Countable/MFMC_Web.thy

View Options

thys/Markov_Models/Continuous_Time_Markov_Chain.thy

View Options

thys/Markov_Models/ex/PCTL.thy

View Options

thys/Ordinary_Differential_Equations/Ex/Lorenz/Lorenz_Approximation.thy

View Options

thys/Ordinary_Differential_Equations/IVP/Cones.thy

View Options

thys/Ordinary_Differential_Equations/IVP/Flow.thy

View Options

thys/Ordinary_Differential_Equations/IVP/Flow_Congs.thy

View Options

thys/Ordinary_Differential_Equations/IVP/Picard_Lindeloef_Qualitative.thy

View Options

thys/Ordinary_Differential_Equations/IVP/Poincare_Map.thy

View Options

thys/Ordinary_Differential_Equations/IVP/Upper_Lower_Solution.thy

View Options

thys/Ordinary_Differential_Equations/Library/Linear_ODE.thy

View Options

thys/Ordinary_Differential_Equations/Numerics/Concrete_Reachability_Analysis.thy

View Options

thys/Ordinary_Differential_Equations/Numerics/Concrete_Reachability_Analysis_C1.thy

View Options

thys/Ordinary_Differential_Equations/Numerics/Concrete_Rigorous_Numerics.thy

View Options

thys/Ordinary_Differential_Equations/Numerics/Example_Utilities.thy

View Options

thys/Ordinary_Differential_Equations/Numerics/Init_ODE_Solver.thy

View Options

thys/Ordinary_Differential_Equations/Numerics/Refine_Reachability_Analysis.thy

View Options

thys/Ordinary_Differential_Equations/Numerics/Refine_Reachability_Analysis_C1.thy

View Options

thys/Ordinary_Differential_Equations/Numerics/Refine_Rigorous_Numerics_Aform.thy

View Options

thys/Ordinary_Differential_Equations/Numerics/Transfer_Euclidean_Space_Vector.thy

View Options

thys/Ordinary_Differential_Equations/ODE_Auxiliarities.thy

View Options

thys/Ordinary_Differential_Equations/Refinement/Autoref_Misc.thy

View Options

thys/Ordinary_Differential_Equations/Refinement/Refine_Default.thy

View Options

thys/Ordinary_Differential_Equations/Refinement/Refine_Interval.thy

View Options

thys/Ordinary_Differential_Equations/Refinement/Refine_Parallel.thy

View Options

thys/Ordinary_Differential_Equations/Refinement/Refine_Vector_List.thy

View Options

thys/Ordinary_Differential_Equations/Refinement/Weak_Set.thy

View Options

thys/PAC_Checker/PAC_More_Poly.thy

View Options

thys/Planarity_Certificates/Planarity/Graph_Genus.thy

View Options

thys/Poincare_Bendixson/Analysis_Misc.thy

View Options

thys/Poincare_Bendixson/ODE_Misc.thy

View Options

thys/Poincare_Bendixson/Poincare_Bendixson.thy

View Options

thys/Random_BSTs/Random_BSTs.thy

View Options

thys/Refine_Imperative_HOL/IICF/Impl/Heaps/IICF_Abs_Heap.thy

View Options

thys/Refine_Imperative_HOL/IICF/Impl/Heaps/IICF_Abs_Heapmap.thy

View Options

thys/SC_DOM_Components/Core_DOM_SC_DOM_Components.thy

View Options

thys/Security_Protocol_Refinement/Refinement/Message.thy

View Options

thys/Smooth_Manifolds/Analysis_More.thy

View Options

thys/Smooth_Manifolds/Bump_Function.thy

View Options

thys/Smooth_Manifolds/Chart.thy

View Options

thys/Smooth_Manifolds/Cotangent_Space.thy

View Options

thys/Smooth_Manifolds/Projective_Space.thy

View Options

thys/Smooth_Manifolds/Tangent_Space.thy

View Options

thys/Stirling_Formula/Gamma_Asymptotics.thy

View Options

thys/Sturm_Sequences/Sturm_Method.thy

View Options

thys/Taylor_Models/Taylor_Models.thy

View Options

thys/VerifyThis2019/Challenge3.thy

View Options

thys/Virtual_Substitution/Debruijn.thy

View Options

thys/Virtual_Substitution/EliminateVariable.thy

View Options

thys/Virtual_Substitution/ExecutiblePolyProps.thy

Automated merge with bundle:/var/folders/9z/l1x9y3bd16x9_70pdp4703jr0000gp/T/So…1668bf4eba40Actions

Description

Details

Event Timeline

Merged Changes

Changes (88)

rAFP1668bf4eba40

thys/Affine_Arithmetic/Affine_Approximation.thy

thys/Affine_Arithmetic/Counterclockwise_2D_Arbitrary.thy

thys/Affine_Arithmetic/Counterclockwise_2D_Strict.thy

thys/Affine_Arithmetic/Executable_Euclidean_Space.thy

thys/Affine_Arithmetic/Floatarith_Expression.thy

thys/Affine_Arithmetic/Intersection.thy

thys/Affine_Arithmetic/Polygon.thy

thys/Affine_Arithmetic/Straight_Line_Program.thy

thys/Amicable_Numbers/Amicable_Numbers.thy

thys/Collections/Examples/Autoref/Simple_DFS.thy

thys/Complex_Bounded_Operators/Cblinfun_Code.thy

thys/Complex_Bounded_Operators/One_Dimensional_Spaces.thy

thys/Complx/OG_Soundness.thy

thys/Complx/ex/Examples.thy

thys/Core_DOM/standard/Core_DOM_Heap_WF.thy

thys/Core_SC_DOM/safely_composable/Core_DOM_Heap_WF.thy

thys/Dirichlet_L/Dirichlet_L_Functions.thy

thys/Dynamic_Tables/Tables_nat.thy

thys/Extended_Finite_State_Machines/EFSM_LTL.thy

thys/Extended_Finite_State_Machines/examples/Drinks_Machine_LTL.thy

thys/FO_Theory_Rewriting/Util/Multihole_Context.thy

thys/Flow_Networks/Residual_Graph.thy

thys/Goedel_HFSet_Semanticless/Sigma.thy

thys/Graph_Theory/Digraph_Isomorphism.thy

thys/Graph_Theory/Kuratowski.thy

thys/Green/Integrals.thy

thys/Hoare_Time/Big_StepT_Partial.thy

thys/IP_Addresses/WordInterval.thy

thys/Incompleteness/Sigma.thy

thys/Iptables_Semantics/Primitive_Matchers/IpAddresses.thy

thys/Lambert_W/Lambert_W.thy

thys/Laplace_Transform/Existence.thy

thys/List_Update/BIT.thy

thys/List_Update/List_Factoring.thy

thys/List_Update/Prob_Theory.thy

thys/List_Update/TS.thy

thys/MFMC_Countable/MFMC_Flow_Attainability.thy

thys/MFMC_Countable/MFMC_Unbounded.thy

thys/MFMC_Countable/MFMC_Web.thy

thys/Markov_Models/Continuous_Time_Markov_Chain.thy

thys/Markov_Models/ex/PCTL.thy

thys/Ordinary_Differential_Equations/Ex/Lorenz/Lorenz_Approximation.thy

thys/Ordinary_Differential_Equations/IVP/Cones.thy

thys/Ordinary_Differential_Equations/IVP/Flow.thy

thys/Ordinary_Differential_Equations/IVP/Flow_Congs.thy

thys/Ordinary_Differential_Equations/IVP/Picard_Lindeloef_Qualitative.thy

thys/Ordinary_Differential_Equations/IVP/Poincare_Map.thy

thys/Ordinary_Differential_Equations/IVP/Upper_Lower_Solution.thy

thys/Ordinary_Differential_Equations/Library/Linear_ODE.thy

thys/Ordinary_Differential_Equations/Numerics/Concrete_Reachability_Analysis.thy

thys/Ordinary_Differential_Equations/Numerics/Concrete_Reachability_Analysis_C1.thy

thys/Ordinary_Differential_Equations/Numerics/Concrete_Rigorous_Numerics.thy

thys/Ordinary_Differential_Equations/Numerics/Example_Utilities.thy

thys/Ordinary_Differential_Equations/Numerics/Init_ODE_Solver.thy

thys/Ordinary_Differential_Equations/Numerics/Refine_Reachability_Analysis.thy

thys/Ordinary_Differential_Equations/Numerics/Refine_Reachability_Analysis_C1.thy

thys/Ordinary_Differential_Equations/Numerics/Refine_Rigorous_Numerics_Aform.thy

thys/Ordinary_Differential_Equations/Numerics/Transfer_Euclidean_Space_Vector.thy

thys/Ordinary_Differential_Equations/ODE_Auxiliarities.thy

thys/Ordinary_Differential_Equations/Refinement/Autoref_Misc.thy

thys/Ordinary_Differential_Equations/Refinement/Refine_Default.thy

thys/Ordinary_Differential_Equations/Refinement/Refine_Interval.thy

thys/Ordinary_Differential_Equations/Refinement/Refine_Parallel.thy

thys/Ordinary_Differential_Equations/Refinement/Refine_Vector_List.thy

thys/Ordinary_Differential_Equations/Refinement/Weak_Set.thy

thys/PAC_Checker/PAC_More_Poly.thy

thys/Planarity_Certificates/Planarity/Graph_Genus.thy

thys/Poincare_Bendixson/Analysis_Misc.thy

thys/Poincare_Bendixson/ODE_Misc.thy

thys/Poincare_Bendixson/Poincare_Bendixson.thy

thys/Random_BSTs/Random_BSTs.thy

thys/Refine_Imperative_HOL/IICF/Impl/Heaps/IICF_Abs_Heap.thy

thys/Refine_Imperative_HOL/IICF/Impl/Heaps/IICF_Abs_Heapmap.thy

Automated merge with bundle:/var/folders/9z/l1x9y3bd16x9_70pdp4703jr0000gp/T/So…
1668bf4eba40
Actions