HomeIsabelle/Phabricator
Diffusion afp-devel 0de1311fe42d

adapted to Isabelle/0252d635bfb2
0de1311fe42d
Actions

Description

adapted to Isabelle/0252d635bfb2

Details

Provenance
desharnaAuthored on
Parents
rAFP8c220a4fb5ab: merging
Branches
Unknown
Tags
Unknown

Changes (114)
Show All Changes

Very Large Commit

This commit is very large. Load each file individually.
PathSize
thys/
BNF_CC/
CakeML_Codegen/
Backend/
Compiler/
Rewriting/
Terms/
Coinductive_Languages/
Core_DOM/
common/
classes/
monads/
standard/
classes/
Core_SC_DOM/
common/
classes/
monads/
safely_composable/
classes/
DOM_Components/
Decl_Sem_Fun_PL/
Extended_Finite_State_Machine_Inference/
Extended_Finite_State_Machines/
examples/
FO_Theory_Rewriting/
Closure/
Primitives/
Util/
FSM_Tests/
EquivalenceTesting/
Factored_Transition_System_Bounding/
Formula_Derivatives/
Incredible_Proof_Machine/
IsaNet/
infrastructure/
instances/
LTL/
LTL_Normal_Form/
Linear_Programming/
MiniSail/
Nested_Multisets_Ordinals/
Nominal2/
PAC_Checker/
Query_Optimization/
Regular_Tree_Relations/
Horn_Setup/
Tree_Automata/
Ribbon_Proofs/
SC_DOM_Components/
Safe_OCL/
Shadow_DOM/
classes/
monads/
Shadow_SC_DOM/
classes/
monads/
Simplex/
Solidity/
UTP/
toolkit/

rAFP0de1311fe42d

View Options

thys/BNF_CC/DDS.thy

View Options

thys/CakeML_Codegen/Backend/CakeML_Correctness.thy

View Options

thys/CakeML_Codegen/Compiler/Compiler.thy

View Options

thys/CakeML_Codegen/Compiler/Composition.thy

View Options

thys/CakeML_Codegen/Rewriting/Rewriting_Pterm_Elim.thy

View Options

thys/CakeML_Codegen/Rewriting/Rewriting_Sterm.thy

View Options

thys/CakeML_Codegen/Terms/Pterm.thy

View Options

thys/CakeML_Codegen/Terms/Sterm.thy

View Options

thys/Coinductive_Languages/Context_Free_Grammar.thy

View Options

thys/Core_DOM/common/classes/CharacterDataClass.thy

View Options

thys/Core_DOM/common/classes/DocumentClass.thy

View Options

thys/Core_DOM/common/classes/NodeClass.thy

View Options

thys/Core_DOM/common/classes/ObjectClass.thy

View Options

thys/Core_DOM/common/monads/BaseMonad.thy

View Options

thys/Core_DOM/common/monads/CharacterDataMonad.thy

View Options

thys/Core_DOM/common/monads/DocumentMonad.thy

View Options

thys/Core_DOM/common/monads/ElementMonad.thy

View Options

thys/Core_DOM/common/monads/NodeMonad.thy

View Options

thys/Core_DOM/common/monads/ObjectMonad.thy

View Options

thys/Core_DOM/standard/Core_DOM_Heap_WF.thy

View Options

thys/Core_DOM/standard/classes/ElementClass.thy

View Options

thys/Core_SC_DOM/common/classes/CharacterDataClass.thy

View Options

thys/Core_SC_DOM/common/classes/DocumentClass.thy

View Options

thys/Core_SC_DOM/common/classes/NodeClass.thy

View Options

thys/Core_SC_DOM/common/classes/ObjectClass.thy

View Options

thys/Core_SC_DOM/common/monads/BaseMonad.thy

View Options

thys/Core_SC_DOM/common/monads/CharacterDataMonad.thy

View Options

thys/Core_SC_DOM/common/monads/DocumentMonad.thy

View Options

thys/Core_SC_DOM/common/monads/ElementMonad.thy

View Options

thys/Core_SC_DOM/common/monads/NodeMonad.thy

View Options

thys/Core_SC_DOM/common/monads/ObjectMonad.thy

View Options

thys/Core_SC_DOM/safely_composable/Core_DOM_Heap_WF.thy

View Options

thys/Core_SC_DOM/safely_composable/classes/ElementClass.thy

View Options

thys/DOM_Components/Core_DOM_Components.thy

View Options

thys/Decl_Sem_Fun_PL/DenotCompleteFSet.thy

View Options

thys/Decl_Sem_Fun_PL/DenotSoundFSet.thy

View Options

thys/Decl_Sem_Fun_PL/ValuesFSetProps.thy

View Options

thys/Extended_Finite_State_Machine_Inference/Inference.thy

View Options

thys/Extended_Finite_State_Machines/EFSM.thy

View Options

thys/Extended_Finite_State_Machines/EFSM_LTL.thy

View Options

thys/Extended_Finite_State_Machines/FSet_Utils.thy

View Options

thys/Extended_Finite_State_Machines/examples/Drinks_Machine.thy

View Options

thys/FO_Theory_Rewriting/Closure/GTT_RRn.thy

View Options

thys/FO_Theory_Rewriting/Closure/TA_Clousure_Const.thy

View Options

thys/FO_Theory_Rewriting/FOR_Check.thy

View Options

thys/FO_Theory_Rewriting/FOR_Check_Impl.thy

View Options

thys/FO_Theory_Rewriting/Primitives/LV_to_GTT.thy

View Options

thys/FO_Theory_Rewriting/Primitives/NF.thy

View Options

thys/FO_Theory_Rewriting/Primitives/NF_Impl.thy

View Options

thys/FO_Theory_Rewriting/Util/Tree_Automata_Derivation_Split.thy

View Options

thys/FSM_Tests/EquivalenceTesting/Simple_Convergence_Graph.thy

View Options

thys/FSM_Tests/FSM.thy

View Options

thys/FSM_Tests/Minimisation.thy

View Options

thys/FSM_Tests/Observability.thy

View Options

thys/Factored_Transition_System_Bounding/FactoredSystem.thy

View Options

thys/Factored_Transition_System_Bounding/SystemAbstraction.thy

View Options

thys/Formula_Derivatives/WS1S_Alt_Formula.thy

View Options

thys/Formula_Derivatives/WS1S_Formula.thy

View Options

thys/Formula_Derivatives/WS1S_Prelim.thy

View Options

thys/Incredible_Proof_Machine/Abstract_Rules_To_Incredible.thy

View Options

thys/Incredible_Proof_Machine/Build_Incredible_Tree.thy

View Options

thys/Incredible_Proof_Machine/Incredible_Completeness.thy

View Options

thys/Incredible_Proof_Machine/Incredible_Correctness.thy

View Options

thys/Incredible_Proof_Machine/Incredible_Deduction.thy

View Options

thys/Incredible_Proof_Machine/Incredible_Signatures.thy

View Options

thys/Incredible_Proof_Machine/Incredible_Trees.thy

View Options

thys/Incredible_Proof_Machine/Indexed_FSet.thy

View Options

thys/IsaNet/infrastructure/Abstract_XOR.thy

View Options

thys/IsaNet/infrastructure/Message.thy

View Options

thys/IsaNet/instances/Anapaya_SCION.thy

View Options

thys/LTL/Disjunctive_Normal_Form.thy

View Options

thys/LTL_Normal_Form/Normal_Form_Code_Export.thy

View Options

thys/Linear_Programming/Matrix_LinPoly.thy

View Options

thys/MiniSail/SyntaxL.thy

View Options

thys/Nested_Multisets_Ordinals/Unary_PCF.thy

View Options

thys/Nominal2/Nominal2_Base.thy

View Options

thys/PAC_Checker/Finite_Map_Multiset.thy

View Options

thys/PAC_Checker/PAC_Map_Rel.thy

View Options

thys/Query_Optimization/Dtree.thy

View Options

thys/Query_Optimization/IKKBZ.thy

View Options

thys/Query_Optimization/IKKBZ_Optimality.thy

View Options

thys/Query_Optimization/List_Dtree.thy

View Options

thys/Regular_Tree_Relations/GTT_Compose.thy

View Options

thys/Regular_Tree_Relations/GTT_Transitive_Closure.thy

View Options

thys/Regular_Tree_Relations/Horn_Setup/Horn_Fset.thy

View Options

thys/Regular_Tree_Relations/Pair_Automaton.thy

View Options

thys/Regular_Tree_Relations/RR2_Infinite.thy

View Options

thys/Regular_Tree_Relations/RR2_Infinite_Q_infinity.thy

View Options

thys/Regular_Tree_Relations/RRn_Automata.thy

View Options

thys/Regular_Tree_Relations/Regular_Relation_Abstract_Impl.thy

View Options

thys/Regular_Tree_Relations/Regular_Relation_Impl.thy

View Options

thys/Regular_Tree_Relations/Tree_Automata/Myhill_Nerode.thy

View Options

thys/Regular_Tree_Relations/Tree_Automata/Tree_Automata.thy

View Options

thys/Regular_Tree_Relations/Tree_Automata/Tree_Automata_Abstract_Impl.thy

View Options

thys/Regular_Tree_Relations/Tree_Automata/Tree_Automata_Complement.thy

View Options

thys/Regular_Tree_Relations/Tree_Automata/Tree_Automata_Det.thy

View Options

thys/Regular_Tree_Relations/Tree_Automata/Tree_Automata_Impl.thy

View Options

thys/Ribbon_Proofs/Ribbons_Graphical_Soundness.thy

View Options

thys/Ribbon_Proofs/Ribbons_Interfaces.thy

View Options

thys/SC_DOM_Components/Core_DOM_DOM_Components.thy

View Options

thys/SC_DOM_Components/Core_DOM_SC_DOM_Components.thy

View Options

thys/SC_DOM_Components/Shadow_DOM_SC_DOM_Components.thy

View Options

thys/Safe_OCL/Finite_Map_Ext.thy

View Options

thys/Safe_OCL/OCL_Typing.thy

View Options

thys/Safe_OCL/Object_Model.thy

View Options

thys/Shadow_DOM/Shadow_DOM.thy

View Options

thys/Shadow_DOM/classes/ShadowRootClass.thy

View Options

thys/Shadow_DOM/monads/ShadowRootMonad.thy

View Options

thys/Shadow_SC_DOM/Shadow_DOM.thy

View Options

thys/Shadow_SC_DOM/classes/ShadowRootClass.thy

View Options

thys/Shadow_SC_DOM/monads/ShadowRootMonad.thy

View Options

thys/Simplex/Linear_Poly_Maps.thy

View Options

thys/Solidity/Statements.thy

View Options

thys/UTP/toolkit/FSet_Extra.thy