diff --git a/src/HOL/Hoare/Hoare_Logic.thy b/src/HOL/Hoare/Hoare_Logic.thy
--- a/src/HOL/Hoare/Hoare_Logic.thy
+++ b/src/HOL/Hoare/Hoare_Logic.thy
@@ -1,219 +1,226 @@
 (*  Title:      HOL/Hoare/Hoare_Logic.thy
     Author:     Leonor Prensa Nieto & Tobias Nipkow
     Copyright   1998 TUM
     Author:     Walter Guttmann (extension to total-correctness proofs)
 
 Sugared semantic embedding of Hoare logic.
 Strictly speaking a shallow embedding (as implemented by Norbert Galm
 following Mike Gordon) would suffice. Maybe the datatype com comes in useful
 later.
 *)
 
 theory Hoare_Logic
-imports Main
+imports Hoare_Tac
 begin
 
 type_synonym 'a bexp = "'a set"
 type_synonym 'a assn = "'a set"
 type_synonym 'a var = "'a \<Rightarrow> nat"
 
 datatype 'a com =
   Basic "'a \<Rightarrow> 'a"
 | Seq "'a com" "'a com"               ("(_;/ _)"      [61,60] 60)
 | Cond "'a bexp" "'a com" "'a com"    ("(1IF _/ THEN _ / ELSE _/ FI)"  [0,0,0] 61)
 | While "'a bexp" "'a assn" "'a var" "'a com"  ("(1WHILE _/ INV {_} / VAR {_} //DO _ /OD)"  [0,0,0,0] 61)
 
 syntax
   "_whilePC" :: "'a bexp \<Rightarrow> 'a assn \<Rightarrow> 'a com \<Rightarrow> 'a com"  ("(1WHILE _/ INV {_} //DO _ /OD)"  [0,0,0] 61)
 translations
   "WHILE b INV {x} DO c OD" \<rightharpoonup> "WHILE b INV {x} VAR {0} DO c OD"
 
 abbreviation annskip ("SKIP") where "SKIP == Basic id"
 
 type_synonym 'a sem = "'a => 'a => bool"
 
 inductive Sem :: "'a com \<Rightarrow> 'a sem"
 where
   "Sem (Basic f) s (f s)"
 | "Sem c1 s s'' \<Longrightarrow> Sem c2 s'' s' \<Longrightarrow> Sem (c1;c2) s s'"
 | "s \<in> b \<Longrightarrow> Sem c1 s s' \<Longrightarrow> Sem (IF b THEN c1 ELSE c2 FI) s s'"
 | "s \<notin> b \<Longrightarrow> Sem c2 s s' \<Longrightarrow> Sem (IF b THEN c1 ELSE c2 FI) s s'"
 | "s \<notin> b \<Longrightarrow> Sem (While b x y c) s s"
 | "s \<in> b \<Longrightarrow> Sem c s s'' \<Longrightarrow> Sem (While b x y c) s'' s' \<Longrightarrow>
    Sem (While b x y c) s s'"
 
 inductive_cases [elim!]:
   "Sem (Basic f) s s'" "Sem (c1;c2) s s'"
   "Sem (IF b THEN c1 ELSE c2 FI) s s'"
 
 lemma Sem_deterministic:
   assumes "Sem c s s1"
       and "Sem c s s2"
     shows "s1 = s2"
 proof -
   have "Sem c s s1 \<Longrightarrow> (\<forall>s2. Sem c s s2 \<longrightarrow> s1 = s2)"
     by (induct rule: Sem.induct) (subst Sem.simps, blast)+
   thus ?thesis
     using assms by simp
 qed
 
 definition Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool"
   where "Valid p c q \<equiv> \<forall>s s'. Sem c s s' \<longrightarrow> s \<in> p \<longrightarrow> s' \<in> q"
 
 definition ValidTC :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool"
   where "ValidTC p c q \<equiv> \<forall>s . s \<in> p \<longrightarrow> (\<exists>t . Sem c s t \<and> t \<in> q)"
 
 lemma tc_implies_pc:
   "ValidTC p c q \<Longrightarrow> Valid p c q"
   by (metis Sem_deterministic Valid_def ValidTC_def)
 
 lemma tc_extract_function:
   "ValidTC p c q \<Longrightarrow> \<exists>f . \<forall>s . s \<in> p \<longrightarrow> f s \<in> q"
   by (metis ValidTC_def)
 
 syntax
   "_assign" :: "idt => 'b => 'a com"  ("(2_ :=/ _)" [70, 65] 61)
 
 syntax
  "_hoare_vars" :: "[idts, 'a assn,'a com,'a assn] => bool"
                  ("VARS _// {_} // _ // {_}" [0,0,55,0] 50)
 syntax (output)
  "_hoare"      :: "['a assn,'a com,'a assn] => bool"
                  ("{_} // _ // {_}" [0,55,0] 50)
 
 ML_file \<open>hoare_syntax.ML\<close>
 parse_translation \<open>[(\<^syntax_const>\<open>_hoare_vars\<close>, K Hoare_Syntax.hoare_vars_tr)]\<close>
 print_translation \<open>[(\<^const_syntax>\<open>Valid\<close>, K (Hoare_Syntax.spec_tr' \<^syntax_const>\<open>_hoare\<close>))]\<close>
 
 syntax
  "_hoare_tc_vars" :: "[idts, 'a assn,'a com,'a assn] => bool"
                     ("VARS _// [_] // _ // [_]" [0,0,55,0] 50)
 syntax (output)
  "_hoare_tc"      :: "['a assn,'a com,'a assn] => bool"
                     ("[_] // _ // [_]" [0,55,0] 50)
 
 parse_translation \<open>[(\<^syntax_const>\<open>_hoare_tc_vars\<close>, K Hoare_Syntax.hoare_tc_vars_tr)]\<close>
 print_translation \<open>[(\<^const_syntax>\<open>ValidTC\<close>, K (Hoare_Syntax.spec_tr' \<^syntax_const>\<open>_hoare_tc\<close>))]\<close>
 
 
 lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) q"
 by (auto simp:Valid_def)
 
 lemma BasicRule: "p \<subseteq> {s. f s \<in> q} \<Longrightarrow> Valid p (Basic f) q"
 by (auto simp:Valid_def)
 
 lemma SeqRule: "Valid P c1 Q \<Longrightarrow> Valid Q c2 R \<Longrightarrow> Valid P (c1;c2) R"
 by (auto simp:Valid_def)
 
 lemma CondRule:
  "p \<subseteq> {s. (s \<in> b \<longrightarrow> s \<in> w) \<and> (s \<notin> b \<longrightarrow> s \<in> w')}
   \<Longrightarrow> Valid w c1 q \<Longrightarrow> Valid w' c2 q \<Longrightarrow> Valid p (Cond b c1 c2) q"
 by (auto simp:Valid_def)
 
 lemma While_aux:
   assumes "Sem (WHILE b INV {i} VAR {v} DO c OD) s s'"
   shows "\<forall>s s'. Sem c s s' \<longrightarrow> s \<in> I \<and> s \<in> b \<longrightarrow> s' \<in> I \<Longrightarrow>
     s \<in> I \<Longrightarrow> s' \<in> I \<and> s' \<notin> b"
   using assms
   by (induct "WHILE b INV {i} VAR {v} DO c OD" s s') auto
 
 lemma WhileRule:
  "p \<subseteq> i \<Longrightarrow> Valid (i \<inter> b) c i \<Longrightarrow> i \<inter> (-b) \<subseteq> q \<Longrightarrow> Valid p (While b i v c) q"
 apply (clarsimp simp:Valid_def)
 apply(drule While_aux)
   apply assumption
  apply blast
 apply blast
 done
 
 lemma SkipRuleTC:
   assumes "p \<subseteq> q"
     shows "ValidTC p (Basic id) q"
   by (metis assms Sem.intros(1) ValidTC_def id_apply subsetD)
 
 lemma BasicRuleTC:
   assumes "p \<subseteq> {s. f s \<in> q}"
     shows "ValidTC p (Basic f) q"
   by (metis assms Ball_Collect Sem.intros(1) ValidTC_def)
 
 lemma SeqRuleTC:
   assumes "ValidTC p c1 q"
       and "ValidTC q c2 r"
     shows "ValidTC p (c1;c2) r"
   by (meson assms Sem.intros(2) ValidTC_def)
 
 lemma CondRuleTC:
  assumes "p \<subseteq> {s. (s \<in> b \<longrightarrow> s \<in> w) \<and> (s \<notin> b \<longrightarrow> s \<in> w')}"
      and "ValidTC w c1 q"
      and "ValidTC w' c2 q"
    shows "ValidTC p (Cond b c1 c2) q"
 proof (unfold ValidTC_def, rule allI)
   fix s
   show "s \<in> p \<longrightarrow> (\<exists>t . Sem (Cond b c1 c2) s t \<and> t \<in> q)"
     apply (cases "s \<in> b")
     apply (metis (mono_tags, lifting) assms(1,2) Ball_Collect Sem.intros(3) ValidTC_def)
     by (metis (mono_tags, lifting) assms(1,3) Ball_Collect Sem.intros(4) ValidTC_def)
 qed
 
 lemma WhileRuleTC:
   assumes "p \<subseteq> i"
       and "\<And>n::nat . ValidTC (i \<inter> b \<inter> {s . v s = n}) c (i \<inter> {s . v s < n})"
       and "i \<inter> uminus b \<subseteq> q"
     shows "ValidTC p (While b i v c) q"
 proof -
   {
     fix s n
     have "s \<in> i \<and> v s = n \<longrightarrow> (\<exists>t . Sem (While b i v c) s t \<and> t \<in> q)"
     proof (induction "n" arbitrary: s rule: less_induct)
       fix n :: nat
       fix s :: 'a
       assume 1: "\<And>(m::nat) s::'a . m < n \<Longrightarrow> s \<in> i \<and> v s = m \<longrightarrow> (\<exists>t . Sem (While b i v c) s t \<and> t \<in> q)"
       show "s \<in> i \<and> v s = n \<longrightarrow> (\<exists>t . Sem (While b i v c) s t \<and> t \<in> q)"
       proof (rule impI, cases "s \<in> b")
         assume 2: "s \<in> b" and "s \<in> i \<and> v s = n"
         hence "s \<in> i \<inter> b \<inter> {s . v s = n}"
           using assms(1) by auto
         hence "\<exists>t . Sem c s t \<and> t \<in> i \<inter> {s . v s < n}"
           by (metis assms(2) ValidTC_def)
         from this obtain t where 3: "Sem c s t \<and> t \<in> i \<inter> {s . v s < n}"
           by auto
         hence "\<exists>u . Sem (While b i v c) t u \<and> u \<in> q"
           using 1 by auto
         thus "\<exists>t . Sem (While b i v c) s t \<and> t \<in> q"
           using 2 3 Sem.intros(6) by force
       next
         assume "s \<notin> b" and "s \<in> i \<and> v s = n"
         thus "\<exists>t . Sem (While b i v c) s t \<and> t \<in> q"
           using Sem.intros(5) assms(3) by fastforce
       qed
     qed
   }
   thus ?thesis
     using assms(1) ValidTC_def by force
 qed
 
-lemma Compl_Collect: "-(Collect b) = {x. \<not>(b x)}"
-  by blast
 
-lemmas AbortRule = SkipRule  \<comment> \<open>dummy version\<close>
-ML_file \<open>hoare_tac.ML\<close>
+declare BasicRule [Hoare_Tac.BasicRule]
+  and SkipRule [Hoare_Tac.SkipRule]
+  and SeqRule [Hoare_Tac.SeqRule]
+  and CondRule [Hoare_Tac.CondRule]
+  and WhileRule [Hoare_Tac.WhileRule]
+
+declare BasicRuleTC [Hoare_Tac.BasicRuleTC]
+  and SkipRuleTC [Hoare_Tac.SkipRuleTC]
+  and SeqRuleTC [Hoare_Tac.SeqRuleTC]
+  and CondRuleTC [Hoare_Tac.CondRuleTC]
+  and WhileRuleTC [Hoare_Tac.WhileRuleTC]
 
 method_setup vcg = \<open>
-  Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare.hoare_tac ctxt (K all_tac)))\<close>
+  Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare_Tac.hoare_tac ctxt (K all_tac)))\<close>
   "verification condition generator"
 
 method_setup vcg_simp = \<open>
   Scan.succeed (fn ctxt =>
-    SIMPLE_METHOD' (Hoare.hoare_tac ctxt (asm_full_simp_tac ctxt)))\<close>
+    SIMPLE_METHOD' (Hoare_Tac.hoare_tac ctxt (asm_full_simp_tac ctxt)))\<close>
   "verification condition generator plus simplification"
 
 method_setup vcg_tc = \<open>
-  Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare.hoare_tc_tac ctxt (K all_tac)))\<close>
+  Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare_Tac.hoare_tc_tac ctxt (K all_tac)))\<close>
   "verification condition generator"
 
 method_setup vcg_tc_simp = \<open>
   Scan.succeed (fn ctxt =>
-    SIMPLE_METHOD' (Hoare.hoare_tc_tac ctxt (asm_full_simp_tac ctxt)))\<close>
+    SIMPLE_METHOD' (Hoare_Tac.hoare_tc_tac ctxt (asm_full_simp_tac ctxt)))\<close>
   "verification condition generator plus simplification"
 
 end
diff --git a/src/HOL/Hoare/Hoare_Logic_Abort.thy b/src/HOL/Hoare/Hoare_Logic_Abort.thy
--- a/src/HOL/Hoare/Hoare_Logic_Abort.thy
+++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy
@@ -1,243 +1,251 @@
 (*  Title:      HOL/Hoare/Hoare_Logic_Abort.thy
     Author:     Leonor Prensa Nieto & Tobias Nipkow
     Copyright   2003 TUM
     Author:     Walter Guttmann (extension to total-correctness proofs)
 
 Like Hoare_Logic.thy, but with an Abort statement for modelling run time errors.
 *)
 
 theory Hoare_Logic_Abort
-imports Main
+imports Hoare_Tac
 begin
 
 type_synonym 'a bexp = "'a set"
 type_synonym 'a assn = "'a set"
 type_synonym 'a var = "'a \<Rightarrow> nat"
 
 datatype 'a com =
   Basic "'a \<Rightarrow> 'a"
 | Abort
 | Seq "'a com" "'a com"               ("(_;/ _)"      [61,60] 60)
 | Cond "'a bexp" "'a com" "'a com"    ("(1IF _/ THEN _ / ELSE _/ FI)"  [0,0,0] 61)
 | While "'a bexp" "'a assn" "'a var" "'a com"  ("(1WHILE _/ INV {_} / VAR {_} //DO _ /OD)"  [0,0,0,0] 61)
 
 syntax
   "_whilePC" :: "'a bexp \<Rightarrow> 'a assn \<Rightarrow> 'a com \<Rightarrow> 'a com"  ("(1WHILE _/ INV {_} //DO _ /OD)"  [0,0,0] 61)
 translations
   "WHILE b INV {x} DO c OD" \<rightharpoonup> "WHILE b INV {x} VAR {0} DO c OD"
 
 abbreviation annskip ("SKIP") where "SKIP == Basic id"
 
 type_synonym 'a sem = "'a option => 'a option => bool"
 
 inductive Sem :: "'a com \<Rightarrow> 'a sem"
 where
   "Sem (Basic f) None None"
 | "Sem (Basic f) (Some s) (Some (f s))"
 | "Sem Abort s None"
 | "Sem c1 s s'' \<Longrightarrow> Sem c2 s'' s' \<Longrightarrow> Sem (c1;c2) s s'"
 | "Sem (IF b THEN c1 ELSE c2 FI) None None"
 | "s \<in> b \<Longrightarrow> Sem c1 (Some s) s' \<Longrightarrow> Sem (IF b THEN c1 ELSE c2 FI) (Some s) s'"
 | "s \<notin> b \<Longrightarrow> Sem c2 (Some s) s' \<Longrightarrow> Sem (IF b THEN c1 ELSE c2 FI) (Some s) s'"
 | "Sem (While b x y c) None None"
 | "s \<notin> b \<Longrightarrow> Sem (While b x y c) (Some s) (Some s)"
 | "s \<in> b \<Longrightarrow> Sem c (Some s) s'' \<Longrightarrow> Sem (While b x y c) s'' s' \<Longrightarrow>
    Sem (While b x y c) (Some s) s'"
 
 inductive_cases [elim!]:
   "Sem (Basic f) s s'" "Sem (c1;c2) s s'"
   "Sem (IF b THEN c1 ELSE c2 FI) s s'"
 
 lemma Sem_deterministic:
   assumes "Sem c s s1"
       and "Sem c s s2"
     shows "s1 = s2"
 proof -
   have "Sem c s s1 \<Longrightarrow> (\<forall>s2. Sem c s s2 \<longrightarrow> s1 = s2)"
     by (induct rule: Sem.induct) (subst Sem.simps, blast)+
   thus ?thesis
     using assms by simp
 qed
 
 definition Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool"
   where "Valid p c q \<equiv> \<forall>s s'. Sem c s s' \<longrightarrow> s \<in> Some ` p \<longrightarrow> s' \<in> Some ` q"
 
 definition ValidTC :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool"
   where "ValidTC p c q \<equiv> \<forall>s . s \<in> p \<longrightarrow> (\<exists>t . Sem c (Some s) (Some t) \<and> t \<in> q)"
 
 lemma tc_implies_pc:
   "ValidTC p c q \<Longrightarrow> Valid p c q"
   by (smt Sem_deterministic ValidTC_def Valid_def image_iff)
 
 lemma tc_extract_function:
   "ValidTC p c q \<Longrightarrow> \<exists>f . \<forall>s . s \<in> p \<longrightarrow> f s \<in> q"
   by (meson ValidTC_def)
 
 syntax
   "_assign" :: "idt => 'b => 'a com"  ("(2_ :=/ _)" [70, 65] 61)
 
 syntax
   "_hoare_abort_vars" :: "[idts, 'a assn,'a com,'a assn] => bool"
                  ("VARS _// {_} // _ // {_}" [0,0,55,0] 50)
 syntax (output)
   "_hoare_abort"      :: "['a assn,'a com,'a assn] => bool"
                  ("{_} // _ // {_}" [0,55,0] 50)
 
 ML_file \<open>hoare_syntax.ML\<close>
 parse_translation \<open>[(\<^syntax_const>\<open>_hoare_abort_vars\<close>, K Hoare_Syntax.hoare_vars_tr)]\<close>
 print_translation \<open>[(\<^const_syntax>\<open>Valid\<close>, K (Hoare_Syntax.spec_tr' \<^syntax_const>\<open>_hoare_abort\<close>))]\<close>
 
 syntax
  "_hoare_abort_tc_vars" :: "[idts, 'a assn,'a com,'a assn] => bool"
                           ("VARS _// [_] // _ // [_]" [0,0,55,0] 50)
 syntax (output)
  "_hoare_abort_tc"      :: "['a assn,'a com,'a assn] => bool"
                           ("[_] // _ // [_]" [0,55,0] 50)
 
 parse_translation \<open>[(\<^syntax_const>\<open>_hoare_abort_tc_vars\<close>, K Hoare_Syntax.hoare_tc_vars_tr)]\<close>
 print_translation \<open>[(\<^const_syntax>\<open>ValidTC\<close>, K (Hoare_Syntax.spec_tr' \<^syntax_const>\<open>_hoare_abort_tc\<close>))]\<close>
 
 text \<open>The proof rules for partial correctness\<close>
 
 lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) q"
 by (auto simp:Valid_def)
 
 lemma BasicRule: "p \<subseteq> {s. f s \<in> q} \<Longrightarrow> Valid p (Basic f) q"
 by (auto simp:Valid_def)
 
 lemma SeqRule: "Valid P c1 Q \<Longrightarrow> Valid Q c2 R \<Longrightarrow> Valid P (c1;c2) R"
 by (auto simp:Valid_def)
 
 lemma CondRule:
  "p \<subseteq> {s. (s \<in> b \<longrightarrow> s \<in> w) \<and> (s \<notin> b \<longrightarrow> s \<in> w')}
   \<Longrightarrow> Valid w c1 q \<Longrightarrow> Valid w' c2 q \<Longrightarrow> Valid p (Cond b c1 c2) q"
 by (fastforce simp:Valid_def image_def)
 
 lemma While_aux:
   assumes "Sem (WHILE b INV {i} VAR {v} DO c OD) s s'"
   shows "\<forall>s s'. Sem c s s' \<longrightarrow> s \<in> Some ` (I \<inter> b) \<longrightarrow> s' \<in> Some ` I \<Longrightarrow>
     s \<in> Some ` I \<Longrightarrow> s' \<in> Some ` (I \<inter> -b)"
   using assms
   by (induct "WHILE b INV {i} VAR {v} DO c OD" s s') auto
 
 lemma WhileRule:
  "p \<subseteq> i \<Longrightarrow> Valid (i \<inter> b) c i \<Longrightarrow> i \<inter> (-b) \<subseteq> q \<Longrightarrow> Valid p (While b i v c) q"
 apply (clarsimp simp:Valid_def)
 apply(drule While_aux)
   apply assumption
  apply blast
 apply blast
 done
 
 lemma AbortRule: "p \<subseteq> {s. False} \<Longrightarrow> Valid p Abort q"
 by(auto simp:Valid_def)
 
 text \<open>The proof rules for total correctness\<close>
 
 lemma SkipRuleTC:
   assumes "p \<subseteq> q"
     shows "ValidTC p (Basic id) q"
   by (metis Sem.intros(2) ValidTC_def assms id_def subsetD)
 
 lemma BasicRuleTC:
   assumes "p \<subseteq> {s. f s \<in> q}"
     shows "ValidTC p (Basic f) q"
   by (metis Ball_Collect Sem.intros(2) ValidTC_def assms)
 
 lemma SeqRuleTC:
   assumes "ValidTC p c1 q"
       and "ValidTC q c2 r"
     shows "ValidTC p (c1;c2) r"
   by (meson assms Sem.intros(4) ValidTC_def)
 
 lemma CondRuleTC:
  assumes "p \<subseteq> {s. (s \<in> b \<longrightarrow> s \<in> w) \<and> (s \<notin> b \<longrightarrow> s \<in> w')}"
      and "ValidTC w c1 q"
      and "ValidTC w' c2 q"
    shows "ValidTC p (Cond b c1 c2) q"
 proof (unfold ValidTC_def, rule allI)
   fix s
   show "s \<in> p \<longrightarrow> (\<exists>t . Sem (Cond b c1 c2) (Some s) (Some t) \<and> t \<in> q)"
     apply (cases "s \<in> b")
     apply (metis (mono_tags, lifting) Ball_Collect Sem.intros(6) ValidTC_def assms(1,2))
     by (metis (mono_tags, lifting) Ball_Collect Sem.intros(7) ValidTC_def assms(1,3))
 qed
 
 lemma WhileRuleTC:
   assumes "p \<subseteq> i"
       and "\<And>n::nat . ValidTC (i \<inter> b \<inter> {s . v s = n}) c (i \<inter> {s . v s < n})"
       and "i \<inter> uminus b \<subseteq> q"
     shows "ValidTC p (While b i v c) q"
 proof -
   {
     fix s n
     have "s \<in> i \<and> v s = n \<longrightarrow> (\<exists>t . Sem (While b i v c) (Some s) (Some t) \<and> t \<in> q)"
     proof (induction "n" arbitrary: s rule: less_induct)
       fix n :: nat
       fix s :: 'a
       assume 1: "\<And>(m::nat) s::'a . m < n \<Longrightarrow> s \<in> i \<and> v s = m \<longrightarrow> (\<exists>t . Sem (While b i v c) (Some s) (Some t) \<and> t \<in> q)"
       show "s \<in> i \<and> v s = n \<longrightarrow> (\<exists>t . Sem (While b i v c) (Some s) (Some t) \<and> t \<in> q)"
       proof (rule impI, cases "s \<in> b")
         assume 2: "s \<in> b" and "s \<in> i \<and> v s = n"
         hence "s \<in> i \<inter> b \<inter> {s . v s = n}"
           using assms(1) by auto
         hence "\<exists>t . Sem c (Some s) (Some t) \<and> t \<in> i \<inter> {s . v s < n}"
           by (metis assms(2) ValidTC_def)
         from this obtain t where 3: "Sem c (Some s) (Some t) \<and> t \<in> i \<inter> {s . v s < n}"
           by auto
         hence "\<exists>u . Sem (While b i v c) (Some t) (Some u) \<and> u \<in> q"
           using 1 by auto
         thus "\<exists>t . Sem (While b i v c) (Some s) (Some t) \<and> t \<in> q"
           using 2 3 Sem.intros(10) by force
       next
         assume "s \<notin> b" and "s \<in> i \<and> v s = n"
         thus "\<exists>t . Sem (While b i v c) (Some s) (Some t) \<and> t \<in> q"
           using Sem.intros(9) assms(3) by fastforce
       qed
     qed
   }
   thus ?thesis
     using assms(1) ValidTC_def by force
 qed
 
 
 subsection \<open>Derivation of the proof rules and, most importantly, the VCG tactic\<close>
 
-lemma Compl_Collect: "-(Collect b) = {x. \<not>(b x)}"
-  by blast
+declare BasicRule [Hoare_Tac.BasicRule]
+  and SkipRule [Hoare_Tac.SkipRule]
+  and AbortRule [Hoare_Tac.AbortRule]
+  and SeqRule [Hoare_Tac.SeqRule]
+  and CondRule [Hoare_Tac.CondRule]
+  and WhileRule [Hoare_Tac.WhileRule]
 
-ML_file \<open>hoare_tac.ML\<close>
+declare BasicRuleTC [Hoare_Tac.BasicRuleTC]
+  and SkipRuleTC [Hoare_Tac.SkipRuleTC]
+  and SeqRuleTC [Hoare_Tac.SeqRuleTC]
+  and CondRuleTC [Hoare_Tac.CondRuleTC]
+  and WhileRuleTC [Hoare_Tac.WhileRuleTC]
 
 method_setup vcg = \<open>
-  Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare.hoare_tac ctxt (K all_tac)))\<close>
+  Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare_Tac.hoare_tac ctxt (K all_tac)))\<close>
   "verification condition generator"
 
 method_setup vcg_simp = \<open>
   Scan.succeed (fn ctxt =>
-    SIMPLE_METHOD' (Hoare.hoare_tac ctxt (asm_full_simp_tac ctxt)))\<close>
+    SIMPLE_METHOD' (Hoare_Tac.hoare_tac ctxt (asm_full_simp_tac ctxt)))\<close>
   "verification condition generator plus simplification"
 
 method_setup vcg_tc = \<open>
-  Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare.hoare_tc_tac ctxt (K all_tac)))\<close>
+  Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare_Tac.hoare_tc_tac ctxt (K all_tac)))\<close>
   "verification condition generator"
 
 method_setup vcg_tc_simp = \<open>
   Scan.succeed (fn ctxt =>
-    SIMPLE_METHOD' (Hoare.hoare_tc_tac ctxt (asm_full_simp_tac ctxt)))\<close>
+    SIMPLE_METHOD' (Hoare_Tac.hoare_tc_tac ctxt (asm_full_simp_tac ctxt)))\<close>
   "verification condition generator plus simplification"
 
 \<comment> \<open>Special syntax for guarded statements and guarded array updates:\<close>
 syntax
   "_guarded_com" :: "bool \<Rightarrow> 'a com \<Rightarrow> 'a com"  ("(2_ \<rightarrow>/ _)" 71)
   "_array_update" :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a com"  ("(2_[_] :=/ _)" [70, 65] 61)
 translations
   "P \<rightarrow> c" == "IF P THEN c ELSE CONST Abort FI"
   "a[i] := v" => "(i < CONST length a) \<rightarrow> (a := CONST list_update a i v)"
   \<comment> \<open>reverse translation not possible because of duplicate \<open>a\<close>\<close>
 
 text \<open>
   Note: there is no special syntax for guarded array access. Thus
   you must write \<open>j < length a \<rightarrow> a[i] := a!j\<close>.
 \<close>
 
 end
diff --git a/src/HOL/Hoare/Hoare_Tac.thy b/src/HOL/Hoare/Hoare_Tac.thy
new file mode 100644
--- /dev/null
+++ b/src/HOL/Hoare/Hoare_Tac.thy
@@ -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
diff --git a/src/HOL/Hoare/hoare_tac.ML b/src/HOL/Hoare/hoare_tac.ML
--- a/src/HOL/Hoare/hoare_tac.ML
+++ b/src/HOL/Hoare/hoare_tac.ML
@@ -1,235 +1,236 @@
 (*  Title:      HOL/Hoare/hoare_tac.ML
     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.
 *)
 
-signature HOARE =
+signature HOARE_TAC =
 sig
   val hoare_rule_tac: Proof.context -> term list * thm -> (int -> tactic) -> bool ->
     int -> tactic
   val hoare_tac: Proof.context -> (int -> tactic) -> int -> tactic
   val hoare_tc_tac: Proof.context -> (int -> tactic) -> int -> tactic
 end;
 
-structure Hoare: HOARE =
+structure Hoare_Tac: HOARE_TAC =
 struct
 
 (*** The tactics ***)
 
 (*****************************************************************************)
 (** The function Mset makes the theorem                                     **)
 (** "?Mset <= {(x1,...,xn). ?P (x1,...,xn)} ==> ?Mset <= {s. ?P s}",        **)
 (** where (x1,...,xn) are the variables of the particular program we are    **)
 (** working on at the moment of the call                                    **)
 (*****************************************************************************)
 
 local
 
 (** maps (%x1 ... xn. t) to [x1,...,xn] **)
 fun abs2list (Const (\<^const_name>\<open>case_prod\<close>, _) $ Abs (x, T, t)) = Free (x, T) :: abs2list t
   | abs2list (Abs (x, T, _)) = [Free (x, T)]
   | abs2list _ = [];
 
 (** maps {(x1,...,xn). t} to [x1,...,xn] **)
 fun mk_vars (Const (\<^const_name>\<open>Collect\<close>,_) $ T) = abs2list T
   | mk_vars _ = [];
 
 (** abstraction of body over a tuple formed from a list of free variables.
 Types are also built **)
 fun mk_abstupleC [] body = absfree ("x", HOLogic.unitT) body
   | mk_abstupleC [v] body = absfree (dest_Free v) body
   | mk_abstupleC (v :: w) body =
       let
         val (x, T) = dest_Free v;
         val z = mk_abstupleC w body;
         val T2 =
           (case z of
             Abs (_, T, _) => T
           | Const (_, Type (_, [_, Type (_, [T, _])])) $ _ => T);
       in
         Const (\<^const_name>\<open>case_prod\<close>,
             (T --> T2 --> HOLogic.boolT) --> HOLogic.mk_prodT (T, T2) --> HOLogic.boolT) $
           absfree (x, T) z
       end;
 
 (** maps [x1,...,xn] to (x1,...,xn) and types**)
 fun mk_bodyC [] = HOLogic.unit
   | mk_bodyC [x] = x
   | mk_bodyC (x :: xs) =
       let
         val (_, T) = dest_Free x;
         val z = mk_bodyC xs;
         val T2 =
           (case z of
             Free (_, T) => T
           | Const (\<^const_name>\<open>Pair\<close>, Type ("fun", [_, Type ("fun", [_, T])])) $ _ $ _ => T);
      in Const (\<^const_name>\<open>Pair\<close>, [T, T2] ---> HOLogic.mk_prodT (T, T2)) $ x $ z end;
 
 (** maps a subgoal of the form:
     VARS x1 ... xn {._.} _ {._.} or to [x1,...,xn]
 **)
 fun get_vars c =
   let
     val d = Logic.strip_assums_concl c;
     val Const _ $ pre $ _ $ _ = HOLogic.dest_Trueprop d;
   in mk_vars pre end;
 
 fun mk_CollectC tm =
-  let val T as Type ("fun",[t,_]) = fastype_of tm;
+  let val Type ("fun",[t,_]) = fastype_of tm;
   in HOLogic.Collect_const t $ tm end;
 
 fun inclt ty = Const (\<^const_name>\<open>Orderings.less_eq\<close>, [ty,ty] ---> HOLogic.boolT);
 
 in
 
 fun Mset ctxt prop =
   let
     val [(Mset, _), (P, _)] = Variable.variant_frees ctxt [] [("Mset", ()), ("P", ())];
 
     val vars = get_vars prop;
     val varsT = fastype_of (mk_bodyC vars);
     val big_Collect =
       mk_CollectC (mk_abstupleC vars (Free (P, varsT --> HOLogic.boolT) $ mk_bodyC vars));
     val small_Collect =
       mk_CollectC (Abs ("x", varsT, Free (P, varsT --> HOLogic.boolT) $ Bound 0));
 
     val MsetT = fastype_of big_Collect;
     fun Mset_incl t = HOLogic.mk_Trueprop (inclt MsetT $ Free (Mset, MsetT) $ t);
     val impl = Logic.mk_implies (Mset_incl big_Collect, Mset_incl small_Collect);
     val th = Goal.prove ctxt [Mset, P] [] impl (fn _ => blast_tac ctxt 1);
  in (vars, th) end;
 
 end;
 
 
 (*****************************************************************************)
 (** Simplifying:                                                            **)
 (** Some useful lemmata, lists and simplification tactics to control which  **)
 (** theorems are used to simplify at each moment, so that the original      **)
 (** input does not suffer any unexpected transformation                     **)
 (*****************************************************************************)
 
 (**Simp_tacs**)
 
 fun before_set2pred_simp_tac ctxt =
   simp_tac (put_simpset HOL_basic_ss ctxt addsimps [Collect_conj_eq RS sym, @{thm Compl_Collect}]);
 
 fun split_simp_tac ctxt =
   simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm split_conv}]);
 
 (*****************************************************************************)
 (** set_to_pred_tac transforms sets inclusion into predicates implication,  **)
 (** maintaining the original variable names.                                **)
 (** Ex. "{x. x=0} <= {x. x <= 1}" -set2pred-> "x=0 --> x <= 1"              **)
 (** Subgoals containing intersections (A Int B) or complement sets (-A)     **)
 (** are first simplified by "before_set2pred_simp_tac", that returns only   **)
 (** subgoals of the form "{x. P x} <= {x. Q x}", which are easily           **)
 (** transformed.                                                            **)
 (** This transformation may solve very easy subgoals due to a ligth         **)
 (** simplification done by (split_all_tac)                                  **)
 (*****************************************************************************)
 
 fun set_to_pred_tac ctxt var_names = SUBGOAL (fn (_, i) =>
   before_set2pred_simp_tac ctxt i THEN_MAYBE
   EVERY [
     resolve_tac ctxt [subsetI] i,
     resolve_tac ctxt [CollectI] i,
     dresolve_tac ctxt [CollectD] i,
     TRY (split_all_tac ctxt i) THEN_MAYBE
      (rename_tac var_names i THEN
       full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm split_conv}]) i)]);
 
 (*******************************************************************************)
 (** basic_simp_tac is called to simplify all verification conditions. It does **)
 (** a light simplification by applying "mem_Collect_eq", then it calls        **)
 (** max_simp_tac, which solves subgoals of the form "A <= A",                 **)
 (** and transforms any other into predicates, applying then                   **)
 (** the tactic chosen by the user, which may solve the subgoal completely.    **)
 (*******************************************************************************)
 
 fun max_simp_tac ctxt var_names tac =
   FIRST' [resolve_tac ctxt [subset_refl],
     set_to_pred_tac ctxt var_names THEN_MAYBE' tac];
 
 fun basic_simp_tac ctxt var_names tac =
   simp_tac
     (put_simpset HOL_basic_ss ctxt
       addsimps [mem_Collect_eq, @{thm split_conv}] addsimprocs [Record.simproc])
   THEN_MAYBE' max_simp_tac ctxt var_names tac;
 
 
 (** hoare_rule_tac **)
 
 fun hoare_rule_tac ctxt (vars, Mlem) tac =
   let
+    val get_thms = Proof_Context.get_thms ctxt;
     val var_names = map (fst o dest_Free) vars;
     fun wlp_tac i =
-      resolve_tac ctxt @{thms SeqRule} i THEN rule_tac false (i + 1)
+      resolve_tac ctxt (get_thms \<^named_theorems>\<open>SeqRule\<close>) i THEN rule_tac false (i + 1)
     and rule_tac pre_cond i st = st |> (*abstraction over st prevents looping*)
       ((wlp_tac i THEN rule_tac pre_cond i)
         ORELSE
         (FIRST [
-          resolve_tac ctxt @{thms SkipRule} i,
-          resolve_tac ctxt @{thms AbortRule} i,
+          resolve_tac ctxt (get_thms \<^named_theorems>\<open>SkipRule\<close>) i,
+          resolve_tac ctxt (get_thms \<^named_theorems>\<open>AbortRule\<close>) i,
           EVERY [
-            resolve_tac ctxt @{thms BasicRule} i,
+            resolve_tac ctxt (get_thms \<^named_theorems>\<open>BasicRule\<close>) i,
             resolve_tac ctxt [Mlem] i,
             split_simp_tac ctxt i],
           EVERY [
-            resolve_tac ctxt @{thms CondRule} i,
+            resolve_tac ctxt (get_thms \<^named_theorems>\<open>CondRule\<close>) i,
             rule_tac false (i + 2),
             rule_tac false (i + 1)],
           EVERY [
-            resolve_tac ctxt @{thms WhileRule} i,
+            resolve_tac ctxt (get_thms \<^named_theorems>\<open>WhileRule\<close>) i,
             basic_simp_tac ctxt var_names tac (i + 2),
             rule_tac true (i + 1)]]
          THEN (
            if pre_cond then basic_simp_tac ctxt var_names tac i
            else resolve_tac ctxt [subset_refl] i)));
   in rule_tac end;
 
 
 (** tac is the tactic the user chooses to solve or simplify **)
 (** the final verification conditions                       **)
 
 fun hoare_tac ctxt tac = SUBGOAL (fn (goal, i) =>
   SELECT_GOAL (hoare_rule_tac ctxt (Mset ctxt goal) tac true 1) i);
 
 
 (* total correctness rules *)
 
 fun hoare_tc_rule_tac ctxt (vars, Mlem) tac =
   let
+    val get_thms = Proof_Context.get_thms ctxt;
     val var_names = map (fst o dest_Free) vars;
     fun wlp_tac i =
-      resolve_tac ctxt @{thms SeqRuleTC} i THEN rule_tac false (i + 1)
+      resolve_tac ctxt (get_thms \<^named_theorems>\<open>SeqRuleTC\<close>) i THEN rule_tac false (i + 1)
     and rule_tac pre_cond i st = st |> (*abstraction over st prevents looping*)
       ((wlp_tac i THEN rule_tac pre_cond i)
         ORELSE
         (FIRST [
-          resolve_tac ctxt @{thms SkipRuleTC} i,
+          resolve_tac ctxt (get_thms \<^named_theorems>\<open>SkipRuleTC\<close>) i,
           EVERY [
-            resolve_tac ctxt @{thms BasicRuleTC} i,
+            resolve_tac ctxt (get_thms \<^named_theorems>\<open>BasicRuleTC\<close>) i,
             resolve_tac ctxt [Mlem] i,
             split_simp_tac ctxt i],
           EVERY [
-            resolve_tac ctxt @{thms CondRuleTC} i,
+            resolve_tac ctxt (get_thms \<^named_theorems>\<open>CondRuleTC\<close>) i,
             rule_tac false (i + 2),
             rule_tac false (i + 1)],
           EVERY [
-            resolve_tac ctxt @{thms WhileRuleTC} i,
+            resolve_tac ctxt (get_thms \<^named_theorems>\<open>WhileRuleTC\<close>) i,
             basic_simp_tac ctxt var_names tac (i + 2),
             rule_tac true (i + 1)]]
          THEN (
            if pre_cond then basic_simp_tac ctxt var_names tac i
            else resolve_tac ctxt [subset_refl] i)));
   in rule_tac end;
 
 
 fun hoare_tc_tac ctxt tac = SUBGOAL (fn (goal, i) =>
   SELECT_GOAL (hoare_tc_rule_tac ctxt (Mset ctxt goal) tac true 1) i);
 
 end;
-
diff --git a/src/HOL/Isar_Examples/Hoare.thy b/src/HOL/Isar_Examples/Hoare.thy
--- a/src/HOL/Isar_Examples/Hoare.thy
+++ b/src/HOL/Isar_Examples/Hoare.thy
@@ -1,419 +1,413 @@
 (*  Title:      HOL/Isar_Examples/Hoare.thy
     Author:     Makarius
 
 A formulation of Hoare logic suitable for Isar.
 *)
 
 section \<open>Hoare Logic\<close>
 
 theory Hoare
-  imports Main
+  imports "HOL-Hoare.Hoare_Tac"
 begin
 
 subsection \<open>Abstract syntax and semantics\<close>
 
 text \<open>
   The following abstract syntax and semantics of Hoare Logic over \<^verbatim>\<open>WHILE\<close>
   programs closely follows the existing tradition in Isabelle/HOL of
   formalizing the presentation given in @{cite \<open>\S6\<close> "Winskel:1993"}. See also
   \<^dir>\<open>~~/src/HOL/Hoare\<close> and @{cite "Nipkow:1998:Winskel"}.
 \<close>
 
 type_synonym 'a bexp = "'a set"
 type_synonym 'a assn = "'a set"
 type_synonym 'a var = "'a \<Rightarrow> nat"
 
 datatype 'a com =
     Basic "'a \<Rightarrow> 'a"
   | Seq "'a com" "'a com"    ("(_;/ _)" [60, 61] 60)
   | Cond "'a bexp" "'a com" "'a com"
   | While "'a bexp" "'a assn" "'a var" "'a com"
 
 abbreviation Skip  ("SKIP")
   where "SKIP \<equiv> Basic id"
 
 type_synonym 'a sem = "'a \<Rightarrow> 'a \<Rightarrow> bool"
 
 primrec iter :: "nat \<Rightarrow> 'a bexp \<Rightarrow> 'a sem \<Rightarrow> 'a sem"
   where
     "iter 0 b S s s' \<longleftrightarrow> s \<notin> b \<and> s = s'"
   | "iter (Suc n) b S s s' \<longleftrightarrow> s \<in> b \<and> (\<exists>s''. S s s'' \<and> iter n b S s'' s')"
 
 primrec Sem :: "'a com \<Rightarrow> 'a sem"
   where
     "Sem (Basic f) s s' \<longleftrightarrow> s' = f s"
   | "Sem (c1; c2) s s' \<longleftrightarrow> (\<exists>s''. Sem c1 s s'' \<and> Sem c2 s'' s')"
   | "Sem (Cond b c1 c2) s s' \<longleftrightarrow> (if s \<in> b then Sem c1 s s' else Sem c2 s s')"
   | "Sem (While b x y c) s s' \<longleftrightarrow> (\<exists>n. iter n b (Sem c) s s')"
 
 definition Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool"  ("(3\<turnstile> _/ (2_)/ _)" [100, 55, 100] 50)
   where "\<turnstile> P c Q \<longleftrightarrow> (\<forall>s s'. Sem c s s' \<longrightarrow> s \<in> P \<longrightarrow> s' \<in> Q)"
 
 lemma ValidI [intro?]: "(\<And>s s'. Sem c s s' \<Longrightarrow> s \<in> P \<Longrightarrow> s' \<in> Q) \<Longrightarrow> \<turnstile> P c Q"
   by (simp add: Valid_def)
 
 lemma ValidD [dest?]: "\<turnstile> P c Q \<Longrightarrow> Sem c s s' \<Longrightarrow> s \<in> P \<Longrightarrow> s' \<in> Q"
   by (simp add: Valid_def)
 
 
 subsection \<open>Primitive Hoare rules\<close>
 
 text \<open>
   From the semantics defined above, we derive the standard set of primitive
   Hoare rules; e.g.\ see @{cite \<open>\S6\<close> "Winskel:1993"}. Usually, variant forms
   of these rules are applied in actual proof, see also \S\ref{sec:hoare-isar}
   and \S\ref{sec:hoare-vcg}.
 
   \<^medskip>
   The \<open>basic\<close> rule represents any kind of atomic access to the state space.
   This subsumes the common rules of \<open>skip\<close> and \<open>assign\<close>, as formulated in
   \S\ref{sec:hoare-isar}.
 \<close>
 
 theorem basic: "\<turnstile> {s. f s \<in> P} (Basic f) P"
 proof
   fix s s'
   assume s: "s \<in> {s. f s \<in> P}"
   assume "Sem (Basic f) s s'"
   then have "s' = f s" by simp
   with s show "s' \<in> P" by simp
 qed
 
 text \<open>
   The rules for sequential commands and semantic consequences are established
   in a straight forward manner as follows.
 \<close>
 
 theorem seq: "\<turnstile> P c1 Q \<Longrightarrow> \<turnstile> Q c2 R \<Longrightarrow> \<turnstile> P (c1; c2) R"
 proof
   assume cmd1: "\<turnstile> P c1 Q" and cmd2: "\<turnstile> Q c2 R"
   fix s s'
   assume s: "s \<in> P"
   assume "Sem (c1; c2) s s'"
   then obtain s'' where sem1: "Sem c1 s s''" and sem2: "Sem c2 s'' s'"
     by auto
   from cmd1 sem1 s have "s'' \<in> Q" ..
   with cmd2 sem2 show "s' \<in> R" ..
 qed
 
 theorem conseq: "P' \<subseteq> P \<Longrightarrow> \<turnstile> P c Q \<Longrightarrow> Q \<subseteq> Q' \<Longrightarrow> \<turnstile> P' c Q'"
 proof
   assume P'P: "P' \<subseteq> P" and QQ': "Q \<subseteq> Q'"
   assume cmd: "\<turnstile> P c Q"
   fix s s' :: 'a
   assume sem: "Sem c s s'"
   assume "s \<in> P'" with P'P have "s \<in> P" ..
   with cmd sem have "s' \<in> Q" ..
   with QQ' show "s' \<in> Q'" ..
 qed
 
 text \<open>
   The rule for conditional commands is directly reflected by the corresponding
   semantics; in the proof we just have to look closely which cases apply.
 \<close>
 
 theorem cond:
   assumes case_b: "\<turnstile> (P \<inter> b) c1 Q"
     and case_nb: "\<turnstile> (P \<inter> -b) c2 Q"
   shows "\<turnstile> P (Cond b c1 c2) Q"
 proof
   fix s s'
   assume s: "s \<in> P"
   assume sem: "Sem (Cond b c1 c2) s s'"
   show "s' \<in> Q"
   proof cases
     assume b: "s \<in> b"
     from case_b show ?thesis
     proof
       from sem b show "Sem c1 s s'" by simp
       from s b show "s \<in> P \<inter> b" by simp
     qed
   next
     assume nb: "s \<notin> b"
     from case_nb show ?thesis
     proof
       from sem nb show "Sem c2 s s'" by simp
       from s nb show "s \<in> P \<inter> -b" by simp
     qed
   qed
 qed
 
 text \<open>
   The \<open>while\<close> rule is slightly less trivial --- it is the only one based on
   recursion, which is expressed in the semantics by a Kleene-style least
   fixed-point construction. The auxiliary statement below, which is by
   induction on the number of iterations is the main point to be proven; the
   rest is by routine application of the semantics of \<^verbatim>\<open>WHILE\<close>.
 \<close>
 
 theorem while:
   assumes body: "\<turnstile> (P \<inter> b) c P"
   shows "\<turnstile> P (While b X Y c) (P \<inter> -b)"
 proof
   fix s s' assume s: "s \<in> P"
   assume "Sem (While b X Y c) s s'"
   then obtain n where "iter n b (Sem c) s s'" by auto
   from this and s show "s' \<in> P \<inter> -b"
   proof (induct n arbitrary: s)
     case 0
     then show ?case by auto
   next
     case (Suc n)
     then obtain s'' where b: "s \<in> b" and sem: "Sem c s s''"
       and iter: "iter n b (Sem c) s'' s'" by auto
     from Suc and b have "s \<in> P \<inter> b" by simp
     with body sem have "s'' \<in> P" ..
     with iter show ?case by (rule Suc)
   qed
 qed
 
 
 subsection \<open>Concrete syntax for assertions\<close>
 
 text \<open>
   We now introduce concrete syntax for describing commands (with embedded
   expressions) and assertions. The basic technique is that of semantic
   ``quote-antiquote''. A \<^emph>\<open>quotation\<close> is a syntactic entity delimited by an
   implicit abstraction, say over the state space. An \<^emph>\<open>antiquotation\<close> is a
   marked expression within a quotation that refers the implicit argument; a
   typical antiquotation would select (or even update) components from the
   state.
 
   We will see some examples later in the concrete rules and applications.
 
   \<^medskip>
   The following specification of syntax and translations is for Isabelle
   experts only; feel free to ignore it.
 
   While the first part is still a somewhat intelligible specification of the
   concrete syntactic representation of our Hoare language, the actual ``ML
   drivers'' is quite involved. Just note that the we re-use the basic
   quote/antiquote translations as already defined in Isabelle/Pure (see \<^ML>\<open>Syntax_Trans.quote_tr\<close>, and \<^ML>\<open>Syntax_Trans.quote_tr'\<close>,).
 \<close>
 
 syntax
   "_quote" :: "'b \<Rightarrow> ('a \<Rightarrow> 'b)"
   "_antiquote" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b"  ("\<acute>_" [1000] 1000)
   "_Subst" :: "'a bexp \<Rightarrow> 'b \<Rightarrow> idt \<Rightarrow> 'a bexp"  ("_[_'/\<acute>_]" [1000] 999)
   "_Assert" :: "'a \<Rightarrow> 'a set"  ("(\<lbrace>_\<rbrace>)" [0] 1000)
   "_Assign" :: "idt \<Rightarrow> 'b \<Rightarrow> 'a com"  ("(\<acute>_ :=/ _)" [70, 65] 61)
   "_Cond" :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com \<Rightarrow> 'a com"
     ("(0IF _/ THEN _/ ELSE _/ FI)" [0, 0, 0] 61)
   "_While_inv" :: "'a bexp \<Rightarrow> 'a assn \<Rightarrow> 'a com \<Rightarrow> 'a com"
     ("(0WHILE _/ INV _ //DO _ /OD)"  [0, 0, 0] 61)
   "_While" :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com"  ("(0WHILE _ //DO _ /OD)"  [0, 0] 61)
 
 translations
   "\<lbrace>b\<rbrace>" \<rightharpoonup> "CONST Collect (_quote b)"
   "B [a/\<acute>x]" \<rightharpoonup> "\<lbrace>\<acute>(_update_name x (\<lambda>_. a)) \<in> B\<rbrace>"
   "\<acute>x := a" \<rightharpoonup> "CONST Basic (_quote (\<acute>(_update_name x (\<lambda>_. a))))"
   "IF b THEN c1 ELSE c2 FI" \<rightharpoonup> "CONST Cond \<lbrace>b\<rbrace> c1 c2"
   "WHILE b INV i DO c OD" \<rightharpoonup> "CONST While \<lbrace>b\<rbrace> i (\<lambda>_. 0) c"
   "WHILE b DO c OD" \<rightleftharpoons> "WHILE b INV CONST undefined DO c OD"
 
 parse_translation \<open>
   let
     fun quote_tr [t] = Syntax_Trans.quote_tr \<^syntax_const>\<open>_antiquote\<close> t
       | quote_tr ts = raise TERM ("quote_tr", ts);
   in [(\<^syntax_const>\<open>_quote\<close>, K quote_tr)] end
 \<close>
 
 text \<open>
   As usual in Isabelle syntax translations, the part for printing is more
   complicated --- we cannot express parts as macro rules as above. Don't look
   here, unless you have to do similar things for yourself.
 \<close>
 
 print_translation \<open>
   let
     fun quote_tr' f (t :: ts) =
           Term.list_comb (f $ Syntax_Trans.quote_tr' \<^syntax_const>\<open>_antiquote\<close> t, ts)
       | quote_tr' _ _ = raise Match;
 
     val assert_tr' = quote_tr' (Syntax.const \<^syntax_const>\<open>_Assert\<close>);
 
     fun bexp_tr' name ((Const (\<^const_syntax>\<open>Collect\<close>, _) $ t) :: ts) =
           quote_tr' (Syntax.const name) (t :: ts)
       | bexp_tr' _ _ = raise Match;
 
     fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) =
           quote_tr' (Syntax.const \<^syntax_const>\<open>_Assign\<close> $ Syntax_Trans.update_name_tr' f)
             (Abs (x, dummyT, Syntax_Trans.const_abs_tr' k) :: ts)
       | assign_tr' _ = raise Match;
   in
    [(\<^const_syntax>\<open>Collect\<close>, K assert_tr'),
     (\<^const_syntax>\<open>Basic\<close>, K assign_tr'),
     (\<^const_syntax>\<open>Cond\<close>, K (bexp_tr' \<^syntax_const>\<open>_Cond\<close>)),
     (\<^const_syntax>\<open>While\<close>, K (bexp_tr' \<^syntax_const>\<open>_While_inv\<close>))]
   end
 \<close>
 
 
 subsection \<open>Rules for single-step proof \label{sec:hoare-isar}\<close>
 
 text \<open>
   We are now ready to introduce a set of Hoare rules to be used in single-step
   structured proofs in Isabelle/Isar. We refer to the concrete syntax
   introduce above.
 
   \<^medskip>
   Assertions of Hoare Logic may be manipulated in calculational proofs, with
   the inclusion expressed in terms of sets or predicates. Reversed order is
   supported as well.
 \<close>
 
 lemma [trans]: "\<turnstile> P c Q \<Longrightarrow> P' \<subseteq> P \<Longrightarrow> \<turnstile> P' c Q"
   by (unfold Valid_def) blast
 lemma [trans] : "P' \<subseteq> P \<Longrightarrow> \<turnstile> P c Q \<Longrightarrow> \<turnstile> P' c Q"
   by (unfold Valid_def) blast
 
 lemma [trans]: "Q \<subseteq> Q' \<Longrightarrow> \<turnstile> P c Q \<Longrightarrow> \<turnstile> P c Q'"
   by (unfold Valid_def) blast
 lemma [trans]: "\<turnstile> P c Q \<Longrightarrow> Q \<subseteq> Q' \<Longrightarrow> \<turnstile> P c Q'"
   by (unfold Valid_def) blast
 
 lemma [trans]:
     "\<turnstile> \<lbrace>\<acute>P\<rbrace> c Q \<Longrightarrow> (\<And>s. P' s \<longrightarrow> P s) \<Longrightarrow> \<turnstile> \<lbrace>\<acute>P'\<rbrace> c Q"
   by (simp add: Valid_def)
 lemma [trans]:
     "(\<And>s. P' s \<longrightarrow> P s) \<Longrightarrow> \<turnstile> \<lbrace>\<acute>P\<rbrace> c Q \<Longrightarrow> \<turnstile> \<lbrace>\<acute>P'\<rbrace> c Q"
   by (simp add: Valid_def)
 
 lemma [trans]:
     "\<turnstile> P c \<lbrace>\<acute>Q\<rbrace> \<Longrightarrow> (\<And>s. Q s \<longrightarrow> Q' s) \<Longrightarrow> \<turnstile> P c \<lbrace>\<acute>Q'\<rbrace>"
   by (simp add: Valid_def)
 lemma [trans]:
     "(\<And>s. Q s \<longrightarrow> Q' s) \<Longrightarrow> \<turnstile> P c \<lbrace>\<acute>Q\<rbrace> \<Longrightarrow> \<turnstile> P c \<lbrace>\<acute>Q'\<rbrace>"
   by (simp add: Valid_def)
 
 
 text \<open>
   Identity and basic assignments.\<^footnote>\<open>The \<open>hoare\<close> method introduced in
   \S\ref{sec:hoare-vcg} is able to provide proper instances for any number of
   basic assignments, without producing additional verification conditions.\<close>
 \<close>
 
 lemma skip [intro?]: "\<turnstile> P SKIP P"
 proof -
   have "\<turnstile> {s. id s \<in> P} SKIP P" by (rule basic)
   then show ?thesis by simp
 qed
 
 lemma assign: "\<turnstile> P [\<acute>a/\<acute>x::'a] \<acute>x := \<acute>a P"
   by (rule basic)
 
 text \<open>
   Note that above formulation of assignment corresponds to our preferred way
   to model state spaces, using (extensible) record types in HOL @{cite
   "Naraschewski-Wenzel:1998:HOOL"}. For any record field \<open>x\<close>, Isabelle/HOL
   provides a functions \<open>x\<close> (selector) and \<open>x_update\<close> (update). Above, there is
   only a place-holder appearing for the latter kind of function: due to
   concrete syntax \<open>\<acute>x := \<acute>a\<close> also contains \<open>x_update\<close>.\<^footnote>\<open>Note that due to the
   external nature of HOL record fields, we could not even state a general
   theorem relating selector and update functions (if this were required here);
   this would only work for any particular instance of record fields introduced
   so far.\<close>
 
   \<^medskip>
   Sequential composition --- normalizing with associativity achieves proper of
   chunks of code verified separately.
 \<close>
 
 lemmas [trans, intro?] = seq
 
 lemma seq_assoc [simp]: "\<turnstile> P c1;(c2;c3) Q \<longleftrightarrow> \<turnstile> P (c1;c2);c3 Q"
   by (auto simp add: Valid_def)
 
 text \<open>Conditional statements.\<close>
 
 lemmas [trans, intro?] = cond
 
 lemma [trans, intro?]:
   "\<turnstile> \<lbrace>\<acute>P \<and> \<acute>b\<rbrace> c1 Q
       \<Longrightarrow> \<turnstile> \<lbrace>\<acute>P \<and> \<not> \<acute>b\<rbrace> c2 Q
       \<Longrightarrow> \<turnstile> \<lbrace>\<acute>P\<rbrace> IF \<acute>b THEN c1 ELSE c2 FI Q"
     by (rule cond) (simp_all add: Valid_def)
 
 text \<open>While statements --- with optional invariant.\<close>
 
 lemma [intro?]: "\<turnstile> (P \<inter> b) c P \<Longrightarrow> \<turnstile> P (While b P V c) (P \<inter> -b)"
   by (rule while)
 
 lemma [intro?]: "\<turnstile> (P \<inter> b) c P \<Longrightarrow> \<turnstile> P (While b undefined V c) (P \<inter> -b)"
   by (rule while)
 
 
 lemma [intro?]:
   "\<turnstile> \<lbrace>\<acute>P \<and> \<acute>b\<rbrace> c \<lbrace>\<acute>P\<rbrace>
     \<Longrightarrow> \<turnstile> \<lbrace>\<acute>P\<rbrace> WHILE \<acute>b INV \<lbrace>\<acute>P\<rbrace> DO c OD \<lbrace>\<acute>P \<and> \<not> \<acute>b\<rbrace>"
   by (simp add: while Collect_conj_eq Collect_neg_eq)
 
 lemma [intro?]:
   "\<turnstile> \<lbrace>\<acute>P \<and> \<acute>b\<rbrace> c \<lbrace>\<acute>P\<rbrace>
     \<Longrightarrow> \<turnstile> \<lbrace>\<acute>P\<rbrace> WHILE \<acute>b DO c OD \<lbrace>\<acute>P \<and> \<not> \<acute>b\<rbrace>"
   by (simp add: while Collect_conj_eq Collect_neg_eq)
 
 
 subsection \<open>Verification conditions \label{sec:hoare-vcg}\<close>
 
 text \<open>
   We now load the \<^emph>\<open>original\<close> ML file for proof scripts and tactic definition
   for the Hoare Verification Condition Generator (see \<^dir>\<open>~~/src/HOL/Hoare\<close>).
   As far as we are concerned here, the result is a proof method \<open>hoare\<close>, which
   may be applied to a Hoare Logic assertion to extract purely logical
   verification conditions. It is important to note that the method requires
   \<^verbatim>\<open>WHILE\<close> loops to be fully annotated with invariants beforehand.
   Furthermore, only \<^emph>\<open>concrete\<close> pieces of code are handled --- the underlying
   tactic fails ungracefully if supplied with meta-variables or parameters, for
   example.
 \<close>
 
 lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) q"
   by (auto simp add: Valid_def)
 
 lemma BasicRule: "p \<subseteq> {s. f s \<in> q} \<Longrightarrow> Valid p (Basic f) q"
   by (auto simp: Valid_def)
 
 lemma SeqRule: "Valid P c1 Q \<Longrightarrow> Valid Q c2 R \<Longrightarrow> Valid P (c1;c2) R"
   by (auto simp: Valid_def)
 
 lemma CondRule:
   "p \<subseteq> {s. (s \<in> b \<longrightarrow> s \<in> w) \<and> (s \<notin> b \<longrightarrow> s \<in> w')}
     \<Longrightarrow> Valid w c1 q \<Longrightarrow> Valid w' c2 q \<Longrightarrow> Valid p (Cond b c1 c2) q"
   by (auto simp: Valid_def)
 
 lemma iter_aux:
   "\<forall>s s'. Sem c s s' \<longrightarrow> s \<in> I \<and> s \<in> b \<longrightarrow> s' \<in> I \<Longrightarrow>
        (\<And>s s'. s \<in> I \<Longrightarrow> iter n b (Sem c) s s' \<Longrightarrow> s' \<in> I \<and> s' \<notin> b)"
   by (induct n) auto
 
 lemma WhileRule:
     "p \<subseteq> i \<Longrightarrow> Valid (i \<inter> b) c i \<Longrightarrow> i \<inter> (-b) \<subseteq> q \<Longrightarrow> Valid p (While b i v c) q"
   apply (clarsimp simp: Valid_def)
   apply (drule iter_aux)
     prefer 2
     apply assumption
    apply blast
   apply blast
   done
 
-lemma Compl_Collect: "- Collect b = {x. \<not> b x}"
-  by blast
-
-lemmas AbortRule = SkipRule  \<comment> \<open>dummy version\<close>
-lemmas SeqRuleTC = SkipRule  \<comment> \<open>dummy version\<close>
-lemmas SkipRuleTC = SkipRule  \<comment> \<open>dummy version\<close>
-lemmas BasicRuleTC = SkipRule  \<comment> \<open>dummy version\<close>
-lemmas CondRuleTC = SkipRule  \<comment> \<open>dummy version\<close>
-lemmas WhileRuleTC = SkipRule  \<comment> \<open>dummy version\<close>
-
-ML_file \<open>~~/src/HOL/Hoare/hoare_tac.ML\<close>
+declare BasicRule [Hoare_Tac.BasicRule]
+  and SkipRule [Hoare_Tac.SkipRule]
+  and SeqRule [Hoare_Tac.SeqRule]
+  and CondRule [Hoare_Tac.CondRule]
+  and WhileRule [Hoare_Tac.WhileRule]
 
 method_setup hoare =
   \<open>Scan.succeed (fn ctxt =>
     (SIMPLE_METHOD'
-      (Hoare.hoare_tac ctxt
+      (Hoare_Tac.hoare_tac ctxt
         (simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm "Record.K_record_comp"}] )))))\<close>
   "verification condition generator for Hoare logic"
 
 end
diff --git a/src/HOL/ROOT b/src/HOL/ROOT
--- a/src/HOL/ROOT
+++ b/src/HOL/ROOT
@@ -1,1181 +1,1183 @@
 chapter HOL
 
 session HOL (main) = Pure +
   description "
     Classical Higher-order Logic.
   "
   options [strict_facts]
   sessions Tools
   theories
     Main (global)
     Complex_Main (global)
   document_theories
     Tools.Code_Generator
   document_files
     "root.bib"
     "root.tex"
 
 session "HOL-Examples" in Examples = HOL +
   description "
     Notable Examples in Isabelle/HOL.
   "
   sessions
     "HOL-Library"
   theories
     Adhoc_Overloading_Examples
     Ackermann
     Cantor
     Coherent
     Commands
     Drinker
     Groebner_Examples
     Iff_Oracle
     Induction_Schema
     Knaster_Tarski
     "ML"
     Peirce
     Records
     Seq
   document_files
     "root.bib"
     "root.tex"
 
 
 session "HOL-Proofs" (timing) in Proofs = Pure +
   description "
     HOL-Main with explicit proof terms.
   "
   options [quick_and_dirty = false, record_proofs = 2, parallel_limit = 500]
   sessions
     "HOL-Library"
   theories
     "HOL-Library.Realizers"
 
 session "HOL-Library" (main timing) in Library = HOL +
   description "
     Classical Higher-order Logic -- batteries included.
   "
   theories
     Library
     (*conflicting type class instantiations and dependent applications*)
     Finite_Lattice
     List_Lexorder
     List_Lenlexorder
     Prefix_Order
     Product_Lexorder
     Product_Order
     Subseq_Order
     (*conflicting syntax*)
     Datatype_Records
     (*data refinements and dependent applications*)
     AList_Mapping
     Code_Binary_Nat
     Code_Prolog
     Code_Real_Approx_By_Float
     Code_Target_Numeral
     DAList
     DAList_Multiset
     RBT_Mapping
     RBT_Set
     (*printing modifications*)
     OptionalSugar
     (*prototypic tools*)
     Predicate_Compile_Quickcheck
     (*legacy tools*)
     Old_Datatype
     Old_Recdef
     Realizers
     Refute
   document_files "root.bib" "root.tex"
 
 session "HOL-Analysis" (main timing) in Analysis = HOL +
   options [document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant",
     document_variants = "document:manual=-proof,-ML,-unimportant"]
   sessions
     "HOL-Library"
     "HOL-Computational_Algebra"
   theories
     Analysis
   document_files
     "root.tex"
     "root.bib"
 
 session "HOL-Complex_Analysis" (main timing) in Complex_Analysis = "HOL-Analysis" +
   options [document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant",
     document_variants = "document:manual=-proof,-ML,-unimportant"]
   theories
     Complex_Analysis
   document_files
     "root.tex"
     "root.bib"
 
 session "HOL-Analysis-ex" in "Analysis/ex" = "HOL-Analysis" +
   theories
     Approximations
     Metric_Arith_Examples
 
 session "HOL-Homology" (timing) in Homology = "HOL-Analysis" +
   options [document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant",
     document_variants = "document:manual=-proof,-ML,-unimportant"]
   sessions
     "HOL-Algebra"
   theories
     Homology
   document_files
     "root.tex"
 
 session "HOL-Computational_Algebra" (main timing) in "Computational_Algebra" = "HOL-Library" +
   theories
     Computational_Algebra
     (*conflicting type class instantiations and dependent applications*)
     Field_as_Ring
 
 session "HOL-Real_Asymp" in Real_Asymp = HOL +
   sessions
     "HOL-Decision_Procs"
   theories
     Real_Asymp
     Real_Asymp_Approx
     Real_Asymp_Examples
 
 session "HOL-Real_Asymp-Manual" in "Real_Asymp/Manual" = "HOL-Real_Asymp" +
   theories
     Real_Asymp_Doc
   document_files (in "~~/src/Doc")
     "iman.sty"
     "extra.sty"
     "isar.sty"
   document_files
     "root.tex"
     "style.sty"
 
 session "HOL-Hahn_Banach" in Hahn_Banach = HOL +
   description "
     Author:     Gertrud Bauer, TU Munich
 
     The Hahn-Banach theorem for real vector spaces.
 
     This is the proof of the Hahn-Banach theorem for real vectorspaces,
     following H. Heuser, Funktionalanalysis, p. 228 -232. The Hahn-Banach
     theorem is one of the fundamental theorems of functional analysis. It is a
     conclusion of Zorn's lemma.
 
     Two different formaulations of the theorem are presented, one for general
     real vectorspaces and its application to normed vectorspaces.
 
     The theorem says, that every continous linearform, defined on arbitrary
     subspaces (not only one-dimensional subspaces), can be extended to a
     continous linearform on the whole vectorspace.
   "
   sessions
     "HOL-Analysis"
   theories
     Hahn_Banach
   document_files "root.bib" "root.tex"
 
 session "HOL-Induct" in Induct = HOL +
   description "
     Examples of (Co)Inductive Definitions.
 
     Comb proves the Church-Rosser theorem for combinators (see
     http://www.cl.cam.ac.uk/ftp/papers/reports/TR396-lcp-generic-automatic-proof-tools.ps.gz).
 
     Mutil is the famous Mutilated Chess Board problem (see
     http://www.cl.cam.ac.uk/ftp/papers/reports/TR394-lcp-mutilated-chess-board.dvi.gz).
 
     PropLog proves the completeness of a formalization of propositional logic
     (see
     http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz).
 
     Exp demonstrates the use of iterated inductive definitions to reason about
     mutually recursive relations.
   "
   sessions
     "HOL-Library"
   theories [quick_and_dirty]
     Common_Patterns
   theories
     Nested_Datatype
     QuoDataType
     QuoNestedDataType
     Term
     SList
     ABexp
     Infinitely_Branching_Tree
     Ordinals
     Sigma_Algebra
     Comb
     PropLog
     Com
   document_files "root.tex"
 
 session "HOL-IMP" (timing) in IMP = "HOL-Library" +
   options [document_variants = document]
   theories
     BExp
     ASM
     Finite_Reachable
     Denotational
     Compiler2
     Poly_Types
     Sec_Typing
     Sec_TypingT
     Def_Init_Big
     Def_Init_Small
     Fold
     Live
     Live_True
     Hoare_Examples
     Hoare_Sound_Complete
     VCG
     Hoare_Total
     VCG_Total_EX
     VCG_Total_EX2
     Collecting1
     Collecting_Examples
     Abs_Int_Tests
     Abs_Int1_parity
     Abs_Int1_const
     Abs_Int3
     Procs_Dyn_Vars_Dyn
     Procs_Stat_Vars_Dyn
     Procs_Stat_Vars_Stat
     C_like
     OO
   document_files "root.bib" "root.tex"
 
 session "HOL-IMPP" in IMPP = HOL +
   description \<open>
     Author:     David von Oheimb
     Copyright   1999 TUM
 
     IMPP -- An imperative language with procedures.
 
     This is an extension of IMP with local variables and mutually recursive
     procedures. For documentation see "Hoare Logic for Mutual Recursion and
     Local Variables" (https://isabelle.in.tum.de/Bali/papers/FSTTCS99.html).
   \<close>
   theories EvenOdd
 
 session "HOL-Data_Structures" (timing) in Data_Structures = HOL +
   options [document_variants = document]
   sessions
     "HOL-Number_Theory"
   theories [document = false]
     Less_False
   theories
     Sorting
     Balance
     Tree_Map
     Interval_Tree
     AVL_Map
     AVL_Bal_Set
     AVL_Bal2_Set
     Height_Balanced_Tree
     RBT_Set2
     RBT_Map
     Tree23_Map
     Tree23_of_List
     Tree234_Map
     Brother12_Map
     AA_Map
     Set2_Join_RBT
     Array_Braun
     Trie_Fun
     Trie_Map
     Tries_Binary
     Queue_2Lists
     Heaps
     Leftist_Heap
     Binomial_Heap
   document_files "root.tex" "root.bib"
 
 session "HOL-Import" in Import = HOL +
   theories HOL_Light_Maps
   theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import
 
 session "HOL-Number_Theory" (main timing) in Number_Theory = "HOL-Computational_Algebra" +
   description "
     Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, Fermat/Euler
     Theorem, Wilson's Theorem, some lemmas for Quadratic Reciprocity.
   "
   sessions
     "HOL-Algebra"
   theories
     Number_Theory
   document_files
     "root.tex"
 
 session "HOL-Hoare" in Hoare = HOL +
   description "
     Verification of imperative programs (verification conditions are generated
     automatically from pre/post conditions and loop invariants).
   "
   theories Hoare
   document_files "root.bib" "root.tex"
 
 session "HOL-Hoare_Parallel" (timing) in Hoare_Parallel = HOL +
   description "
     Verification of shared-variable imperative programs a la Owicki-Gries.
     (verification conditions are generated automatically).
   "
   theories Hoare_Parallel
   document_files "root.bib" "root.tex"
 
 session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Library" +
   sessions
     "HOL-Number_Theory"
     "HOL-Data_Structures"
     "HOL-Examples"
   theories
     Generate
     Generate_Binary_Nat
     Generate_Target_Nat
     Generate_Efficient_Datastructures
     Code_Lazy_Test
     Code_Test_PolyML
     Code_Test_Scala
   theories [condition = ISABELLE_GHC]
     Code_Test_GHC
   theories [condition = ISABELLE_MLTON]
     Code_Test_MLton
   theories [condition = ISABELLE_OCAMLFIND]
     Code_Test_OCaml
   theories [condition = ISABELLE_SMLNJ]
     Code_Test_SMLNJ
 
 session "HOL-Metis_Examples" (timing) in Metis_Examples = "HOL-Library" +
   description "
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Author:     Jasmin Blanchette, TU Muenchen
 
     Testing Metis and Sledgehammer.
   "
   sessions
     "HOL-Decision_Procs"
   theories
     Abstraction
     Big_O
     Binary_Tree
     Clausification
     Message
     Proxies
     Tarski
     Trans_Closure
     Sets
 
 session "HOL-Nitpick_Examples" in Nitpick_Examples = HOL +
   description "
     Author:     Jasmin Blanchette, TU Muenchen
     Copyright   2009
   "
   sessions "HOL-Library"
   theories [quick_and_dirty] Nitpick_Examples
 
 session "HOL-Algebra" (main timing) in Algebra = "HOL-Computational_Algebra" +
   description "
     Author: Clemens Ballarin, started 24 September 1999, and many others
 
     The Isabelle Algebraic Library.
   "
   sessions
     "HOL-Cardinals"
   theories
     (* Orders and Lattices *)
     Galois_Connection    (* Knaster-Tarski theorem and Galois connections *)
     (* Groups *)
     FiniteProduct        (* Product operator for commutative groups *)
     Sylow                (* Sylow's theorem *)
     Bij                  (* Automorphism Groups *)
     Multiplicative_Group
     Zassenhaus            (* The Zassenhaus lemma *)
     (* Rings *)
     Divisibility         (* Rings *)
     IntRing              (* Ideals and residue classes *)
     UnivPoly             (* Polynomials *)
     (* Main theory *)
     Algebra
   document_files "root.bib" "root.tex"
 
 session "HOL-Auth" (timing) in Auth = HOL +
   description "
     A new approach to verifying authentication protocols.
   "
   sessions "HOL-Library"
   directories "Smartcard" "Guard"
   theories
     Auth_Shared
     Auth_Public
     "Smartcard/Auth_Smartcard"
     "Guard/Auth_Guard_Shared"
     "Guard/Auth_Guard_Public"
   document_files "root.tex"
 
 session "HOL-UNITY" (timing) in UNITY = "HOL-Auth" +
   description "
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1998  University of Cambridge
 
     Verifying security protocols using Chandy and Misra's UNITY formalism.
   "
   directories "Simple" "Comp"
   theories
     (*Basic meta-theory*)
     UNITY_Main
 
     (*Simple examples: no composition*)
     "Simple/Deadlock"
     "Simple/Common"
     "Simple/Network"
     "Simple/Token"
     "Simple/Channel"
     "Simple/Lift"
     "Simple/Mutex"
     "Simple/Reach"
     "Simple/Reachability"
 
     (*Verifying security protocols using UNITY*)
     "Simple/NSP_Bad"
 
     (*Example of composition*)
     "Comp/Handshake"
 
     (*Universal properties examples*)
     "Comp/Counter"
     "Comp/Counterc"
     "Comp/Priority"
 
     "Comp/TimerArray"
     "Comp/Progress"
 
     "Comp/Alloc"
     "Comp/AllocImpl"
     "Comp/Client"
 
     (*obsolete*)
     ELT
   document_files "root.tex"
 
 session "HOL-Unix" in Unix = HOL +
   options [print_mode = "no_brackets,no_type_brackets"]
   sessions "HOL-Library"
   theories Unix
   document_files "root.bib" "root.tex"
 
 session "HOL-ZF" in ZF = HOL +
   sessions "HOL-Library"
   theories
     MainZF
     Games
   document_files "root.tex"
 
 session "HOL-Imperative_HOL" (timing) in Imperative_HOL = HOL +
   options [print_mode = "iff,no_brackets"]
   sessions "HOL-Library"
   directories "ex"
   theories Imperative_HOL_ex
   document_files "root.bib" "root.tex"
 
 session "HOL-Decision_Procs" (timing) in Decision_Procs = "HOL-Algebra" +
   description "
     Various decision procedures, typically involving reflection.
   "
   directories "ex"
   theories
     Decision_Procs
 
 session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" +
   sessions
     "HOL-Examples"
   theories
     Hilbert_Classical
     Proof_Terms
     XML_Data
 
 session "HOL-Proofs-Extraction" (timing) in "Proofs/Extraction" = "HOL-Proofs" +
   description "
     Examples for program extraction in Higher-Order Logic.
   "
   options [quick_and_dirty = false]
   sessions
     "HOL-Computational_Algebra"
   theories
     Greatest_Common_Divisor
     Warshall
     Higman_Extraction
     Pigeonhole
     Euclid
   document_files "root.bib" "root.tex"
 
 session "HOL-Proofs-Lambda" (timing) in "Proofs/Lambda" = "HOL-Proofs" +
   description \<open>
     Lambda Calculus in de Bruijn's Notation.
 
     This session defines lambda-calculus terms with de Bruijn indixes and
     proves confluence of beta, eta and beta+eta.
 
     The paper "More Church-Rosser Proofs (in Isabelle/HOL)" describes the whole
     theory (see http://www.in.tum.de/~nipkow/pubs/jar2001.html).
   \<close>
   options [print_mode = "no_brackets", quick_and_dirty = false]
   sessions
     "HOL-Library"
   theories
     Eta
     StrongNorm
     Standardization
     WeakNorm
   document_files "root.bib" "root.tex"
 
 session "HOL-Prolog" in Prolog = HOL +
   description "
     Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
 
     A bare-bones implementation of Lambda-Prolog.
 
     This is a simple exploratory implementation of Lambda-Prolog in HOL,
     including some minimal examples (in Test.thy) and a more typical example of
     a little functional language and its type system.
   "
   theories Test Type
 
 session "HOL-MicroJava" (timing) in MicroJava = HOL +
   description "
     Formalization of a fragment of Java, together with a corresponding virtual
     machine and a specification of its bytecode verifier and a lightweight
     bytecode verifier, including proofs of type-safety.
   "
   sessions
     "HOL-Library"
     "HOL-Eisbach"
   directories "BV" "Comp" "DFA" "J" "JVM"
   theories
     MicroJava
   document_files
     "introduction.tex"
     "root.bib"
     "root.tex"
 
 session "HOL-NanoJava" in NanoJava = HOL +
   description "
     Hoare Logic for a tiny fragment of Java.
   "
   theories Example
   document_files "root.bib" "root.tex"
 
 session "HOL-Bali" (timing) in Bali = HOL +
   sessions
     "HOL-Library"
   theories
     AxExample
     AxSound
     AxCompl
     Trans
     TypeSafe
   document_files "root.tex"
 
 session "HOL-IOA" in IOA = HOL +
   description \<open>
     Author:     Tobias Nipkow and Konrad Slind and Olaf Müller
     Copyright   1994--1996  TU Muenchen
 
     The meta-theory of I/O-Automata in HOL. This formalization has been
     significantly changed and extended, see HOLCF/IOA. There are also the
     proofs of two communication protocols which formerly have been here.
 
     @inproceedings{Nipkow-Slind-IOA,
     author={Tobias Nipkow and Konrad Slind},
     title={{I/O} Automata in {Isabelle/HOL}},
     booktitle={Proc.\ TYPES Workshop 1994},
     publisher=Springer,
     series=LNCS,
     note={To appear}}
     ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/ioa.ps.gz
 
     and
 
     @inproceedings{Mueller-Nipkow,
     author={Olaf M\"uller and Tobias Nipkow},
     title={Combining Model Checking and Deduction for {I/O}-Automata},
     booktitle={Proc.\ TACAS Workshop},
     organization={Aarhus University, BRICS report},
     year=1995}
     ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz
   \<close>
   theories Solve
 
 session "HOL-Lattice" in Lattice = HOL +
   description "
     Author:     Markus Wenzel, TU Muenchen
 
     Basic theory of lattices and orders.
   "
   theories CompleteLattice
   document_files "root.tex"
 
 session "HOL-ex" (timing) in ex = "HOL-Number_Theory" +
   description "
     Miscellaneous examples for Higher-Order Logic.
   "
   theories
     Antiquote
     Argo_Examples
     Arith_Examples
     Ballot
     BinEx
     Birthday_Paradox
     Bit_Lists
     Bubblesort
     CTL
     Cartouche_Examples
     Case_Product
     Chinese
     Classical
     Code_Binary_Nat_examples
     Code_Lazy_Demo
     Code_Timing
     Coercion_Examples
     Computations
     Conditional_Parametricity_Examples
     Cubic_Quartic
     Datatype_Record_Examples
     Dedekind_Real
     Erdoes_Szekeres
     Eval_Examples
     Executable_Relation
     Execute_Choice
     Functions
     Function_Growth
     Gauge_Integration
     Guess
     HarmonicSeries
     Hebrew
     Hex_Bin_Examples
     IArray_Examples
     Intuitionistic
     Join_Theory
     Lagrange
     List_to_Set_Comprehension_Examples
     LocaleTest2
     MergeSort
     MonoidGroup
     Multiquote
     NatSum
     Normalization_by_Evaluation
     PER
     Parallel_Example
     Peano_Axioms
     Perm_Fragments
     PresburgerEx
     Primrec
     Pythagoras
     Quicksort
     Radix_Sort
     Reflection_Examples
     Refute_Examples
     Residue_Ring
     Rewrite_Examples
     SOS
     SOS_Cert
     Serbian
     Set_Comprehension_Pointfree_Examples
     Set_Theory
     Simproc_Tests
     Simps_Case_Conv_Examples
     Sketch_and_Explore
     Sorting_Algorithms_Examples
     Specifications_with_bundle_mixins
     Sqrt
     Sqrt_Script
     Sudoku
     Sum_of_Powers
     Tarski
     Termination
     ThreeDivides
     Transfer_Debug
     Transfer_Int_Nat
     Transitive_Closure_Table_Ex
     Tree23
     Triangular_Numbers
     Unification
     While_Combinator_Example
     veriT_Preprocessing
   theories [skip_proofs = false]
     SAT_Examples
     Meson_Test
 
 session "HOL-Isar_Examples" in Isar_Examples = "HOL-Computational_Algebra" +
   description "
     Miscellaneous Isabelle/Isar examples.
   "
   options [quick_and_dirty]
+  sessions
+    "HOL-Hoare"
   theories
     Structured_Statements
     Basic_Logic
     Expr_Compiler
     Fibonacci
     Group
     Group_Context
     Group_Notepad
     Hoare_Ex
     Mutilated_Checkerboard
     Puzzle
     Summation
   document_files
     "root.bib"
     "root.tex"
 
 session "HOL-Eisbach" in Eisbach = HOL +
   description \<open>
     The Eisbach proof method language and "match" method.
   \<close>
   sessions
     FOL
     "HOL-Analysis"
   theories
     Eisbach
     Tests
     Examples
     Examples_FOL
     Example_Metric
 
 session "HOL-SET_Protocol" (timing) in SET_Protocol = HOL +
   description "
     Verification of the SET Protocol.
   "
   sessions
     "HOL-Library"
   theories
     SET_Protocol
   document_files "root.tex"
 
 session "HOL-Matrix_LP" in Matrix_LP = HOL +
   description "
     Two-dimensional matrices and linear programming.
   "
   sessions "HOL-Library"
   directories "Compute_Oracle"
   theories Cplex
   document_files "root.tex"
 
 session "HOL-TLA" in TLA = HOL +
   description "
     Lamport's Temporal Logic of Actions.
   "
   theories TLA
 
 session "HOL-TLA-Inc" in "TLA/Inc" = "HOL-TLA" +
   theories Inc
 
 session "HOL-TLA-Buffer" in "TLA/Buffer" = "HOL-TLA" +
   theories DBuffer
 
 session "HOL-TLA-Memory" in "TLA/Memory" = "HOL-TLA" +
   theories MemoryImplementation
 
 session "HOL-TPTP" in TPTP = HOL +
   description "
     Author:     Jasmin Blanchette, TU Muenchen
     Author:     Nik Sultana, University of Cambridge
     Copyright   2011
 
     TPTP-related extensions.
   "
   sessions
     "HOL-Library"
   theories
     ATP_Theory_Export
     MaSh_Eval
     TPTP_Interpret
     THF_Arith
     TPTP_Proof_Reconstruction
   theories
     ATP_Problem_Import
 
 session "HOL-Probability" (main timing) in "Probability" = "HOL-Analysis" +
   theories
     Probability
   document_files "root.tex"
 
 session "HOL-Probability-ex" (timing) in "Probability/ex" = "HOL-Probability" +
   theories
     Dining_Cryptographers
     Koepf_Duermuth_Countermeasure
     Measure_Not_CCC
 
 session "HOL-Nominal" in Nominal = HOL +
   sessions "HOL-Library"
   theories
     Nominal
 
 session "HOL-Nominal-Examples" (timing) in "Nominal/Examples" = "HOL-Nominal" +
   theories
     Class3
     CK_Machine
     Compile
     Contexts
     Crary
     CR_Takahashi
     CR
     Fsub
     Height
     Lambda_mu
     Lam_Funs
     LocalWeakening
     Pattern
     SN
     SOS
     Standardization
     Support
     Type_Preservation
     Weakening
     W
   theories [quick_and_dirty]
     VC_Condition
 
 session "HOL-Cardinals" (timing) in Cardinals = HOL +
   description "
     Ordinals and Cardinals, Full Theories.
   "
   theories
     Cardinals
     Bounded_Set
   document_files
     "intro.tex"
     "root.tex"
     "root.bib"
 
 session "HOL-Datatype_Examples" (timing) in Datatype_Examples = "HOL-Library" +
   description "
     (Co)datatype Examples.
   "
   directories "Derivation_Trees"
   theories
     Compat
     Lambda_Term
     Process
     TreeFsetI
     "Derivation_Trees/Gram_Lang"
     "Derivation_Trees/Parallel_Composition"
     Koenig
     Lift_BNF
     Milner_Tofte
     Stream_Processor
     Cyclic_List
     Free_Idempotent_Monoid
     LDL
     TLList
     Misc_Codatatype
     Misc_Datatype
     Misc_Primcorec
     Misc_Primrec
     Datatype_Simproc_Tests
 
 session "HOL-Corec_Examples" (timing) in Corec_Examples = "HOL-Library" +
   description "
     Corecursion Examples.
   "
   directories "Tests"
   theories
     LFilter
     Paper_Examples
     Stream_Processor
     "Tests/Simple_Nesting"
     "Tests/Iterate_GPV"
   theories [quick_and_dirty]
     "Tests/GPV_Bare_Bones"
     "Tests/Merge_D"
     "Tests/Merge_Poly"
     "Tests/Misc_Mono"
     "Tests/Misc_Poly"
     "Tests/Small_Concrete"
     "Tests/Stream_Friends"
     "Tests/TLList_Friends"
     "Tests/Type_Class"
 
 session "HOL-Statespace" in Statespace = HOL +
   theories [skip_proofs = false]
     StateSpaceEx
   document_files "root.tex"
 
 session "HOL-Nonstandard_Analysis" (timing) in Nonstandard_Analysis = "HOL-Computational_Algebra" +
   description "
     Nonstandard analysis.
   "
   theories
     Nonstandard_Analysis
   document_files "root.tex"
 
 session "HOL-Nonstandard_Analysis-Examples" (timing) in "Nonstandard_Analysis/Examples" = "HOL-Nonstandard_Analysis" +
   theories
     NSPrimes
 
 session "HOL-Mirabelle" in Mirabelle = HOL +
   theories Mirabelle_Test
 
 session "HOL-Mirabelle-ex" in "Mirabelle/ex" = "HOL-Mirabelle" +
   options [timeout = 60]
   theories Ex
 
 session "HOL-SMT_Examples" (timing) in SMT_Examples = HOL +
   options [quick_and_dirty]
   sessions
     "HOL-Library"
   theories
     Boogie
     SMT_Examples
     SMT_Word_Examples
     SMT_Tests
     SMT_Tests_Verit
     SMT_Examples_Verit
 
 session "HOL-SPARK" in "SPARK" = HOL +
   sessions
     "HOL-Library"
   theories
     SPARK
 
 session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" +
   directories "Gcd" "Liseq" "RIPEMD-160" "Sqrt"
   theories
     "Gcd/Greatest_Common_Divisor"
     "Liseq/Longest_Increasing_Subsequence"
     "RIPEMD-160/F"
     "RIPEMD-160/Hash"
     "RIPEMD-160/K_L"
     "RIPEMD-160/K_R"
     "RIPEMD-160/R_L"
     "RIPEMD-160/Round"
     "RIPEMD-160/R_R"
     "RIPEMD-160/S_L"
     "RIPEMD-160/S_R"
     "Sqrt/Sqrt"
   export_files (in ".") "*:**.prv"
 
 session "HOL-SPARK-Manual" in "SPARK/Manual" = "HOL-SPARK" +
   options [show_question_marks = false]
   sessions
     "HOL-Library"
     "HOL-SPARK-Examples"
   theories
     Example_Verification
     VC_Principles
     Reference
     Complex_Types
   document_theories
     "HOL-SPARK-Examples.Greatest_Common_Divisor"
   document_files
     "complex_types.ads"
     "complex_types_app.adb"
     "complex_types_app.ads"
     "Gcd.adb"
     "Gcd.ads"
     "intro.tex"
     "loop_invariant.adb"
     "loop_invariant.ads"
     "root.bib"
     "root.tex"
     "Simple_Gcd.adb"
     "Simple_Gcd.ads"
 
 session "HOL-Mutabelle" in Mutabelle = HOL +
   sessions "HOL-Library"
   theories MutabelleExtra
 
 session "HOL-Quickcheck_Examples" (timing) in Quickcheck_Examples = HOL +
   sessions "HOL-Library"
   theories
     Quickcheck_Examples
     Quickcheck_Lattice_Examples
     Completeness
     Quickcheck_Interfaces
     Quickcheck_Nesting_Example
   theories [condition = ISABELLE_GHC]
     Hotel_Example
     Quickcheck_Narrowing_Examples
 
 session "HOL-Quotient_Examples" (timing) in Quotient_Examples = "HOL-Algebra" +
   description "
     Author:     Cezary Kaliszyk and Christian Urban
   "
   theories
     DList
     Quotient_FSet
     Quotient_Int
     Quotient_Message
     Lift_FSet
     Lift_Set
     Lift_Fun
     Quotient_Rat
     Lift_DList
     Int_Pow
     Lifting_Code_Dt_Test
 
 session "HOL-Predicate_Compile_Examples" (timing) in Predicate_Compile_Examples = HOL +
   sessions "HOL-Library"
   theories
     Examples
     Predicate_Compile_Tests
     Predicate_Compile_Quickcheck_Examples
     Specialisation_Examples
     IMP_1
     IMP_2
     (* FIXME since 21-Jul-2011
     Hotel_Example_Small_Generator *)
     IMP_3
     IMP_4
   theories [condition = ISABELLE_SWIPL]
     Code_Prolog_Examples
     Context_Free_Grammar_Example
     Hotel_Example_Prolog
     Lambda_Example
     List_Examples
   theories [condition = ISABELLE_SWIPL, quick_and_dirty]
     Reg_Exp_Example
 
 session "HOL-Types_To_Sets" in Types_To_Sets = HOL +
   description "
     Experimental extension of Higher-Order Logic to allow translation of types to sets.
   "
   directories "Examples"
   theories
     Types_To_Sets
     "Examples/Prerequisites"
     "Examples/Finite"
     "Examples/T2_Spaces"
     "Examples/Unoverload_Def"
     "Examples/Linear_Algebra_On"
 
 session HOLCF (main timing) in HOLCF = HOL +
   description "
     Author:     Franz Regensburger
     Author:     Brian Huffman
 
     HOLCF -- a semantic extension of HOL by the LCF logic.
   "
   sessions
     "HOL-Library"
   theories
     HOLCF (global)
   document_files "root.tex"
 
 session "HOLCF-Tutorial" in "HOLCF/Tutorial" = HOLCF +
   theories
     Domain_ex
     Fixrec_ex
     New_Domain
   document_files "root.tex"
 
 session "HOLCF-Library" in "HOLCF/Library" = HOLCF +
   theories
     HOLCF_Library
     HOL_Cpo
 
 session "HOLCF-IMP" in "HOLCF/IMP" = HOLCF +
   description "
     IMP -- A WHILE-language and its Semantics.
 
     This is the HOLCF-based denotational semantics of a simple WHILE-language.
   "
   sessions
     "HOL-IMP"
   theories
     HoareEx
   document_files
     "isaverbatimwrite.sty"
     "root.tex"
     "root.bib"
 
 session "HOLCF-ex" in "HOLCF/ex" = "HOLCF-Library" +
   description "
     Miscellaneous examples for HOLCF.
   "
   theories
     Dnat
     Dagstuhl
     Focus_ex
     Fix2
     Hoare
     Concurrency_Monad
     Loop
     Powerdomain_ex
     Domain_Proofs
     Letrec
     Pattern_Match
 
 session "HOLCF-FOCUS" in "HOLCF/FOCUS" = "HOLCF-Library" +
   description \<open>
     FOCUS: a theory of stream-processing functions Isabelle/HOLCF.
 
     For introductions to FOCUS, see
 
     "The Design of Distributed Systems - An Introduction to FOCUS"
     http://www4.in.tum.de/publ/html.php?e=2
 
     "Specification and Refinement of a Buffer of Length One"
     http://www4.in.tum.de/publ/html.php?e=15
 
     "Specification and Development of Interactive Systems: Focus on Streams,
     Interfaces, and Refinement" http://www4.in.tum.de/publ/html.php?e=321
   \<close>
   theories
     Fstreams
     FOCUS
     Buffer_adm
 
 session IOA (timing) in "HOLCF/IOA" = HOLCF +
   description "
     Author:     Olaf Müller
     Copyright   1997 TU München
 
     A formalization of I/O automata in HOLCF.
 
     The distribution contains simulation relations, temporal logic, and an
     abstraction theory. Everything is based upon a domain-theoretic model of
     finite and infinite sequences.
   "
   theories Abstraction
 
 session "IOA-ABP" in "HOLCF/IOA/ABP" = IOA +
   description "
     Author:     Olaf Müller
 
     The Alternating Bit Protocol performed in I/O-Automata:
     combining IOA with Model Checking.
 
     Theory Correctness contains the proof of the abstraction from unbounded
     channels to finite ones.
 
     File Check.ML contains a simple ModelChecker prototype checking Spec
     against the finite version of the ABP-protocol.
   "
   theories
     Correctness
     Spec
 
 session "IOA-NTP" in "HOLCF/IOA/NTP" = IOA +
   description "
     Author:     Tobias Nipkow & Konrad Slind
 
     A network transmission protocol, performed in the
     I/O automata formalization by Olaf Müller.
   "
   theories
     Overview
     Correctness
 
 session "IOA-Storage" in "HOLCF/IOA/Storage" = IOA +
   description "
     Author:     Olaf Müller
 
     Memory storage case study.
   "
   theories Correctness
 
 session "IOA-ex" in "HOLCF/IOA/ex" = IOA +
   description "
     Author:     Olaf Müller
   "
   theories
     TrivEx
     TrivEx2