Session Simpl
View
theory dependencies
View
document
View
outline
Theories
HOL-Library.Old_Recdef
File ‹old_recdef.ML›
Language
Semantic
HoarePartialDef
HoarePartialProps
HoarePartial
Termination
SmallStep
HoareTotalDef
HoareTotalProps
HoareTotal
Hoare
StateSpace
AlternativeSmallStep
Simpl_Heap
HeapList
HOL-Statespace.DistinctTreeProver
File ‹distinct_tree_prover.ML›
HOL-Statespace.StateFun
HOL-Statespace.StateSpaceLocale
File ‹state_space.ML›
File ‹state_fun.ML›
Generalise
File ‹generalise_state.ML›
Vcg
File ‹hoare.ML›
File ‹hoare_syntax.ML›
SyntaxTest
VcgEx
VcgExSP
VcgExTotal
HOL-Library.Cancellation
File ‹Cancellation/cancel.ML›
File ‹Cancellation/cancel_data.ML›
File ‹Cancellation/cancel_simprocs.ML›
HOL-Library.Multiset
File ‹multiset_simprocs.ML›
Quicksort
XVcg
XVcgEx
ProcParEx
ProcParExSP
Closure
ClosureEx
Compose
ComposeEx
HOL-Statespace.StateSpaceSyntax
HOL-Library.LaTeXsugar
UserGuide
Simpl