HomeIsabelle/Phabricator
Diffusion afp-devel 7fc86009bce1

Added proofs for various properties of well-founded heaps and normalized type…
7fc86009bce1
Actions

Description

Added proofs for various properties of well-founded heaps and normalized type synonyms for heaps.

Details

Provenance
Achim D. Brucker <adbrucker@0x5f.org>Authored on
Parents
rAFP8f6e1822c2b8: Fixed typo.
Branches
Unknown
Tags
Unknown

Changes (20)

PathSize
thys/
Core_DOM/
common/
classes/
monads/
preliminaries/
tests/
standard/
classes/
pointers/

rAFP7fc86009bce1

View Options

thys/Core_DOM/common/Core_DOM_Functions.thy

Loading...
View Options

thys/Core_DOM/common/classes/CharacterDataClass.thy

Loading...
View Options

thys/Core_DOM/common/classes/DocumentClass.thy

Loading...
View Options

thys/Core_DOM/common/classes/NodeClass.thy

Loading...
View Options

thys/Core_DOM/common/classes/ObjectClass.thy

Loading...
View Options

thys/Core_DOM/common/monads/CharacterDataMonad.thy

Loading...
View Options

thys/Core_DOM/common/monads/DocumentMonad.thy

Loading...
View Options

thys/Core_DOM/common/monads/ElementMonad.thy

Loading...
View Options

thys/Core_DOM/common/monads/NodeMonad.thy

Loading...
View Options

thys/Core_DOM/common/monads/ObjectMonad.thy

Loading...
View Options

thys/Core_DOM/common/preliminaries/Heap_Error_Monad.thy

Loading...
View Options

thys/Core_DOM/common/preliminaries/Testing_Utils.thy

Loading...
View Options

thys/Core_DOM/common/tests/Core_DOM_BaseTest.thy

Loading...
View Options

thys/Core_DOM/common/tests/Document_adoptNode.thy

Loading...
View Options

thys/Core_DOM/common/tests/Document_getElementById.thy

Loading...
View Options

thys/Core_DOM/common/tests/Node_insertBefore.thy

Loading...
View Options

thys/Core_DOM/common/tests/Node_removeChild.thy

Loading...
View Options

thys/Core_DOM/standard/Core_DOM_Heap_WF.thy

Loading...
View Options

thys/Core_DOM/standard/classes/ElementClass.thy

Loading...
View Options

thys/Core_DOM/standard/pointers/ShadowRootPointer.thy

Loading...