Session Refine_Monadic
View
theory dependencies
View
document
View
outline
Theories
Refine_Chapter
HOL-Library.Adhoc_Overloading
File ‹adhoc_overloading.ML›
HOL-Library.Monad_Syntax
Refine_Mono_Prover
File ‹refine_mono_prover.ML›
Refine_Misc
RefineG_Transfer
RefineG_Domain
RefineG_Recursion
RefineG_Assert
Refine_Basic
Refine_Leof
Refine_Heuristics
Refine_More_Comb
HOL-Library.While_Combinator
RefineG_While
Refine_While
Refine_Det
Refine_Pfun
Refine_Transfer
Refine_Foreach
Refine_Automation
Autoref_Monadic
Refine_Monadic
Example_Chapter
Breadth_First_Search
HOL-Library.Phantom_Type
HOL-Library.Cardinality
HOL-Library.Numeral_Type
HOL-Library.Type_Length
HOL-Library.Word
File ‹Tools/word_lib.ML›
File ‹Tools/smt_word.ML›
WordRefine
Examples