Diffusion afp-devel c594c8cd5faa

Some additions to IICF by Valentin Springsklee
c594c8cd5faa
Actions

Tags

None

Subscribers

None

Description

Some additions to IICF by Valentin Springsklee

Details

Provenance

Authored on

Parents

rAFPb07f8898e878: merge

Branches

Unknown

Tags

Unknown

Event Timeline

peter_lammich committed rAFPc594c8cd5faa: Some additions to IICF by Valentin Springsklee.Jul 27 2023, 2:27 PM

Changes (10)

Path

Size

metadata/

entries/

Refine_Imperative_HOL.toml

Separation_Logic_Imperative_HOL.toml

thys/

Automatic_Refinement/

Parametricity/

Refine_Imperative_HOL/

IICF/

Impl/

IICF_Indexed_Array_List.thy

IICF_Sepl_Binding.thy

Intf/

Separation_Logic_Imperative_HOL/

Examples/

Hash_Set_Impl.thy

Imp_Set_Spec.thy

rAFPc594c8cd5faa

metadata/authors.toml

Loading...

metadata/entries/Refine_Imperative_HOL.toml

Loading...

metadata/entries/Separation_Logic_Imperative_HOL.toml

Loading...

thys/Automatic_Refinement/Parametricity/Param_HOL.thy

Loading...

thys/Automatic_Refinement/Parametricity/Relators.thy

Loading...

thys/Refine_Imperative_HOL/IICF/Impl/IICF_Indexed_Array_List.thy

Loading...

thys/Refine_Imperative_HOL/IICF/Impl/IICF_Sepl_Binding.thy

Loading...

thys/Refine_Imperative_HOL/IICF/Intf/IICF_Set.thy

Loading...

thys/Separation_Logic_Imperative_HOL/Examples/Hash_Set_Impl.thy

Loading...

thys/Separation_Logic_Imperative_HOL/Examples/Imp_Set_Spec.thy

Loading...