Name		Name	Last commit message	Last commit date
parent directory ..
document		document
ex		ex
AlternativeSmallStep.thy		AlternativeSmallStep.thy
DPC0Expressions.thy		DPC0Expressions.thy
DPC0Library.thy		DPC0Library.thy
Generalise.thy		Generalise.thy
HeapList.thy		HeapList.thy
Hoare.thy		Hoare.thy
HoarePartial.thy		HoarePartial.thy
HoarePartialDef.thy		HoarePartialDef.thy
HoarePartialProps.thy		HoarePartialProps.thy
HoareTotal.thy		HoareTotal.thy
HoareTotalDef.thy		HoareTotalDef.thy
HoareTotalProps.thy		HoareTotalProps.thy
Language.thy		Language.thy
README.md		README.md
ROOT		ROOT
Semantic.thy		Semantic.thy
Simpl.thy		Simpl.thy
Simpl_Heap.thy		Simpl_Heap.thy
SmallStep.thy		SmallStep.thy
StateSpace.thy		StateSpace.thy
SyntaxTest.thy		SyntaxTest.thy
Termination.thy		Termination.thy
UserGuide.thy		UserGuide.thy
Vcg.thy		Vcg.thy
XVcg.thy		XVcg.thy
generalise_state.ML		generalise_state.ML
hoare.ML		hoare.ML
hoare_syntax.ML		hoare_syntax.ML

README.md

Simpl

This directory contains Norbert Schirmer's Simpl language and associated VCG tool. The code is covered by an LGPL licence.

See https://www.isa-afp.org/entries/Simpl.html