Session HOL-Hoare

Theories

• Hoare_Syntax
  • File ‹hoare_syntax.ML›
• Hoare_Tac
  • File ‹hoare_tac.ML›
• Hoare_Logic
• Arith2
• Examples
• Hoare_Logic_Abort
• ExamplesAbort
• ExamplesTC
• Pointers0
• Heap
• HeapSyntax
• Pointer_Examples
• HeapSyntaxAbort
• Pointer_ExamplesAbort
• SchorrWaite
• SepLogHeap
• Separation