Session Simpl

Theories

• Language
• Semantic
• HoarePartialDef
• HoarePartialProps
• HoarePartial
• Termination
• SmallStep
• HoareTotalDef
• HoareTotalProps
• HoareTotal
• Hoare
• StateSpace
• AlternativeSmallStep
• Simpl_Heap
• HeapList
• Generalise
  • File ‹generalise_state.ML›
• Vcg
  • File ‹hoare.ML›
  • File ‹hoare_syntax.ML›
• SyntaxTest
• VcgEx
• VcgExSP
• VcgExTotal
• Quicksort
• XVcg
• XVcgEx
• ProcParEx
• ProcParExSP
• Closure
• ClosureEx
• Compose
• ComposeEx
• UserGuide
• Simpl