Diffusion afp-devel 2dab1d50e8a7

updated to new map update syntax priorities
2dab1d50e8a7
Actions

Description

updated to new map update syntax priorities

Details

Provenance

nipkow

Authored on

Parents

rAFPb8d596202cef: Minor refinements

Branches

Unknown

Tags

Unknown

Event Timeline

nipkow committed rAFP2dab1d50e8a7: updated to new map update syntax priorities.Mar 15 2023, 6:43 AM

Changes (36)

Path

Size

thys/

AI_Planning_Languages_Semantics/

SASP_Checker.thy

Automatic_Refinement/

Lib/

Misc.thy

Concurrent_Revisions/

Containers/

CoreC++/

Featherweight_OCL/

examples/

Employee_Model/

Analysis/

Analysis_UML.thy

Design/

Design_UML.thy

Hoare_Time/

Big_StepT_Partial.thy

Isabelle_Meta_Model/

toy_example/

document_generated/

Design_generated.thy

Design_generated_generated.thy

generator/

Design_shallow.thy

LightweightJava/

Lightweight_Java_Definition.thy

Lightweight_Java_Proof.thy

Locally-Nameless-Sigma/

Sigma/

Sigma.thy

Monad_Memo_DP/

heap_monad/

Pair_Memory.thy

State_Heap.thy

Name_Carrying_Type_Inference/

PreSimplyTyped.thy

SimplyTyped.thy

SATSolverVerification/

ConflictAnalysis.thy

SPARCv8/

SparcModel_MMU/

Sparc_Properties.thy

Security_Protocol_Refinement/

Key_establish/

Separation_Logic_Imperative_HOL/

Examples/

UPF/

rAFP2dab1d50e8a7

View Options

thys/AI_Planning_Languages_Semantics/SASP_Checker.thy

View Options

thys/Automatic_Refinement/Lib/Misc.thy

View Options

thys/Concurrent_Revisions/Renaming.thy

View Options

thys/Containers/RBT_ext.thy

View Options

thys/CoreC++/Determinism.thy

View Options

thys/CoreC++/Equivalence.thy

View Options

thys/CoreC++/Exceptions.thy

View Options

thys/CoreC++/Execute.thy

View Options

thys/CoreC++/TypeSafe.thy

View Options

thys/Featherweight_OCL/examples/Employee_Model/Analysis/Analysis_UML.thy

View Options

thys/Featherweight_OCL/examples/Employee_Model/Design/Design_UML.thy

View Options

thys/Hoare_Time/Big_StepT_Partial.thy

View Options

thys/Isabelle_Meta_Model/toy_example/document_generated/Design_generated.thy

View Options

thys/Isabelle_Meta_Model/toy_example/document_generated/Design_generated_generated.thy

View Options

thys/Isabelle_Meta_Model/toy_example/generator/Design_shallow.thy

View Options

thys/LightweightJava/Lightweight_Java_Definition.thy

View Options

thys/LightweightJava/Lightweight_Java_Proof.thy

View Options

thys/Locally-Nameless-Sigma/Sigma/Sigma.thy

View Options

thys/Monad_Memo_DP/heap_monad/Pair_Memory.thy

View Options

thys/Monad_Memo_DP/heap_monad/State_Heap.thy

View Options

thys/Name_Carrying_Type_Inference/PreSimplyTyped.thy

View Options

thys/Name_Carrying_Type_Inference/SimplyTyped.thy

View Options

thys/SATSolverVerification/ConflictAnalysis.thy

View Options

thys/SPARCv8/SparcModel_MMU/Sparc_Properties.thy

View Options

thys/Security_Protocol_Refinement/Key_establish/m1_kerberos.thy

View Options

thys/Security_Protocol_Refinement/Key_establish/m3_ds.thy

View Options

thys/Security_Protocol_Refinement/Key_establish/m3_ds_par.thy

View Options

thys/Security_Protocol_Refinement/Key_establish/m3_kerberos4.thy

View Options

thys/Security_Protocol_Refinement/Key_establish/m3_kerberos5.thy

View Options

thys/Security_Protocol_Refinement/Key_establish/m3_kerberos_par.thy

View Options

thys/Security_Protocol_Refinement/Key_establish/m3_nssk.thy

View Options

thys/Security_Protocol_Refinement/Key_establish/m3_nssk_par.thy

View Options

thys/Separation_Logic_Imperative_HOL/Examples/Array_Map_Impl.thy

View Options

thys/Separation_Logic_Imperative_HOL/Examples/Hash_Map.thy

View Options

thys/Separation_Logic_Imperative_HOL/Examples/Hash_Set_Impl.thy

View Options

thys/UPF/ServiceExample.thy

updated to new map update syntax priorities2dab1d50e8a7Actions

Description

Details

Event Timeline

Changes (36)

rAFP2dab1d50e8a7

thys/AI_Planning_Languages_Semantics/SASP_Checker.thy

thys/Automatic_Refinement/Lib/Misc.thy

thys/Concurrent_Revisions/Renaming.thy

thys/Containers/RBT_ext.thy

thys/CoreC++/Determinism.thy

thys/CoreC++/Equivalence.thy

thys/CoreC++/Exceptions.thy

thys/CoreC++/Execute.thy

thys/CoreC++/TypeSafe.thy

thys/Featherweight_OCL/examples/Employee_Model/Analysis/Analysis_UML.thy

thys/Featherweight_OCL/examples/Employee_Model/Design/Design_UML.thy

thys/Hoare_Time/Big_StepT_Partial.thy

thys/Isabelle_Meta_Model/toy_example/document_generated/Design_generated.thy

thys/Isabelle_Meta_Model/toy_example/document_generated/Design_generated_generated.thy

thys/Isabelle_Meta_Model/toy_example/generator/Design_shallow.thy

thys/LightweightJava/Lightweight_Java_Definition.thy

thys/LightweightJava/Lightweight_Java_Proof.thy

thys/Locally-Nameless-Sigma/Sigma/Sigma.thy

thys/Monad_Memo_DP/heap_monad/Pair_Memory.thy

thys/Monad_Memo_DP/heap_monad/State_Heap.thy

thys/Name_Carrying_Type_Inference/PreSimplyTyped.thy

thys/Name_Carrying_Type_Inference/SimplyTyped.thy

thys/SATSolverVerification/ConflictAnalysis.thy

thys/SPARCv8/SparcModel_MMU/Sparc_Properties.thy

thys/Security_Protocol_Refinement/Key_establish/m1_kerberos.thy

thys/Security_Protocol_Refinement/Key_establish/m3_ds.thy

thys/Security_Protocol_Refinement/Key_establish/m3_ds_par.thy

thys/Security_Protocol_Refinement/Key_establish/m3_kerberos4.thy

thys/Security_Protocol_Refinement/Key_establish/m3_kerberos5.thy

thys/Security_Protocol_Refinement/Key_establish/m3_kerberos_par.thy

thys/Security_Protocol_Refinement/Key_establish/m3_nssk.thy

thys/Security_Protocol_Refinement/Key_establish/m3_nssk_par.thy

thys/Separation_Logic_Imperative_HOL/Examples/Array_Map_Impl.thy

thys/Separation_Logic_Imperative_HOL/Examples/Hash_Map.thy

thys/Separation_Logic_Imperative_HOL/Examples/Hash_Set_Impl.thy

thys/UPF/ServiceExample.thy

updated to new map update syntax priorities
2dab1d50e8a7
Actions