src/HOL/Hoare/Hoare_Tac.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hoare/Hoare_Tac.thy	Wed Dec 23 17:16:05 2020 +0100
@@ -0,0 +1,35 @@
+(*  Title:      HOL/Hoare/Hoare_Tac.thy
+    Author:     Leonor Prensa Nieto & Tobias Nipkow
+    Author:     Walter Guttmann (extension to total-correctness proofs)
+
+Derivation of the proof rules and, most importantly, the VCG tactic.
+*)
+
+theory Hoare_Tac
+  imports Main
+begin
+
+context
+begin
+
+qualified named_theorems BasicRule
+qualified named_theorems SkipRule
+qualified named_theorems AbortRule
+qualified named_theorems SeqRule
+qualified named_theorems CondRule
+qualified named_theorems WhileRule
+
+qualified named_theorems BasicRuleTC
+qualified named_theorems SkipRuleTC
+qualified named_theorems SeqRuleTC
+qualified named_theorems CondRuleTC
+qualified named_theorems WhileRuleTC
+
+lemma Compl_Collect: "-(Collect b) = {x. \<not>(b x)}"
+  by blast
+
+ML_file \<open>hoare_tac.ML\<close>
+
+end
+
+end