Session Simpl

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