# HG changeset patch
# User nipkow
# Date 816595450 -3600
# Node ID 5e1c0540f2859297d997ea0ccf7be16052ba2542
# Parent  32a9fde85699cbfa9f0092d2217bf502e0fb1398
New directory.
Hoare logic according to Mike Gordon.

diff -r 32a9fde85699 -r 5e1c0540f285 src/HOL/Hoare/Arith2.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hoare/Arith2.ML	Fri Nov 17 09:04:10 1995 +0100
@@ -0,0 +1,400 @@
+(*  Title: 	HOL/Hoare/Arith2.ML
+    ID:         $Id$
+    Author: 	Norbert Galm
+    Copyright   1995 TUM
+
+More arithmetic lemmas.
+*)
+
+open Arith2;
+
+
+(*** HOL lemmas ***)
+
+
+val [prem1,prem2]=goal HOL.thy "[|~P ==> ~Q; Q|] ==> P";
+by (cut_facts_tac [prem1 COMP impI,prem2] 1);
+by (fast_tac HOL_cs 1);
+val not_imp_swap=result();
+
+
+(*** analogue of diff_induct, for simultaneous induction over 3 vars ***)
+
+val prems = goal Nat.thy
+    "[| !!x. P x 0 0;  \
+\       !!y. P 0 (Suc y) 0;  \
+\       !!z. P 0 0 (Suc z);  \
+\       !!x y. [| P x y 0 |] ==> P (Suc x) (Suc y) 0;  \
+\       !!x z. [| P x 0 z |] ==> P (Suc x) 0 (Suc z);  \
+\       !!y z. [| P 0 y z |] ==> P 0 (Suc y) (Suc z);  \
+\       !!x y z. [| P x y z |] ==> P (Suc x) (Suc y) (Suc z)  \
+\    |] ==> P m n k";
+by (res_inst_tac [("x","m")] spec 1);
+br diff_induct 1;
+br allI 1;
+br allI 2;
+by (res_inst_tac [("m","xa"),("n","x")] diff_induct 1);
+by (res_inst_tac [("m","x"),("n","Suc y")] diff_induct 4);
+br allI 7;
+by (nat_ind_tac "xa" 7);
+by (ALLGOALS (resolve_tac prems));
+ba 1;
+ba 1;
+by (fast_tac HOL_cs 1);
+by (fast_tac HOL_cs 1);
+qed "diff_induct3";
+
+(*** interaction of + and - ***)
+
+val prems=goal Arith.thy "~m<n+k ==> (m - n) - k = m - ((n + k)::nat)";
+by (cut_facts_tac prems 1);
+br mp 1;
+ba 2;
+by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
+by (ALLGOALS Asm_simp_tac);
+qed "diff_not_assoc";
+
+val prems=goal Arith.thy "[|~m<n; ~n<k|] ==> (m - n) + k = m - ((n - k)::nat)";
+by (cut_facts_tac prems 1);
+bd conjI 1;
+ba 1;
+by (res_inst_tac [("P","~m<n & ~n<k")] mp 1);
+ba 2;
+by (res_inst_tac [("m","m"),("n","n"),("k","k")] diff_induct3 1);
+by (ALLGOALS Asm_simp_tac);
+br impI 1;
+by (dres_inst_tac [("P","~x<y")] conjE 1);
+ba 2;
+br (Suc_diff_n RS sym) 1;
+br le_less_trans 1;
+be (not_less_eq RS subst) 2;
+br (hd ([diff_less_Suc RS lessD] RL [Suc_le_mono RS subst])) 1;
+qed "diff_add_not_assoc";
+
+val prems=goal Arith.thy "~n<k ==> (m + n) - k = m + ((n - k)::nat)";
+by (cut_facts_tac prems 1);
+br mp 1;
+ba 2;
+by (res_inst_tac [("m","n"),("n","k")] diff_induct 1);
+by (ALLGOALS Asm_simp_tac);
+qed "add_diff_assoc";
+
+(*** more ***)
+
+val prems = goal Arith.thy "m~=(n::nat) = (m<n | n<m)";
+br iffI 1;
+by (cut_inst_tac [("m","m"),("n","n")] less_linear 1);
+by (Asm_full_simp_tac 1);
+be disjE 1;
+be (less_not_refl2 RS not_sym) 1;
+be less_not_refl2 1;
+qed "not_eq_eq_less_or_gr";
+
+val [prem] = goal Arith.thy "m<n ==> n-m~=0";
+by (rtac (prem RS rev_mp) 1);
+by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
+by (ALLGOALS Asm_simp_tac);
+qed "less_imp_diff_not_0";
+
+(*******************************************************************)
+
+val prems = goal Arith.thy "(i::nat)<j ==> k+i<k+j";
+by (cut_facts_tac prems 1);
+by (nat_ind_tac "k" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "add_less_mono_l";
+
+val prems = goal Arith.thy "~(i::nat)<j ==> ~k+i<k+j";
+by (cut_facts_tac prems 1);
+by (nat_ind_tac "k" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "add_not_less_mono_l";
+
+val prems = goal Arith.thy "[|0<k; m<(n::nat)|] ==> m*k<n*k";
+by (cut_facts_tac prems 1);
+by (res_inst_tac [("n","k")] natE 1);
+by (ALLGOALS Asm_full_simp_tac);
+by (nat_ind_tac "x" 1);
+be add_less_mono 2;
+by (ALLGOALS Asm_full_simp_tac);
+qed "mult_less_mono_r";
+
+val prems = goal Arith.thy "~m<(n::nat) ==> ~m*k<n*k";
+by (cut_facts_tac prems 1);
+by (nat_ind_tac "k" 1);
+by (ALLGOALS Simp_tac);
+by (fold_goals_tac [le_def]);
+be add_le_mono 1;
+ba 1;
+qed "mult_not_less_mono_r";
+
+val prems = goal Arith.thy "m=(n::nat) ==> m*k=n*k";
+by (cut_facts_tac prems 1);
+by (nat_ind_tac "k" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "mult_eq_mono_r";
+
+val prems = goal Arith.thy "[|0<k; m~=(n::nat)|] ==> m*k~=n*k";
+by (cut_facts_tac prems 1);
+by (res_inst_tac [("P","m<n"),("Q","n<m")] disjE 1);
+br (less_not_refl2 RS not_sym) 2;
+be mult_less_mono_r 2;
+br less_not_refl2 3;
+be mult_less_mono_r 3;
+by (ALLGOALS (asm_full_simp_tac ((simpset_of "Arith") addsimps [not_eq_eq_less_or_gr])));
+qed "mult_not_eq_mono_r";
+
+(******************************************************************)
+
+val prems = goal Arith.thy "(m - n)*k = (m*k) - ((n*k)::nat)";
+by (res_inst_tac [("P","m*k<n*k")] case_split_thm 1);
+by (forward_tac [mult_not_less_mono_r COMP not_imp_swap] 1);
+bd (less_not_sym RS (not_less_eq RS iffD1) RS less_imp_diff_is_0) 1;
+bd (less_not_sym RS (not_less_eq RS iffD1) RS less_imp_diff_is_0) 1;
+br mp 2;
+ba 3;
+by (res_inst_tac [("m","m"),("n","n")] diff_induct 2);
+by (ALLGOALS Asm_simp_tac);
+br impI 1;
+bd (refl RS iffD1) 1;
+by (dres_inst_tac [("k","k")] add_not_less_mono_l 1);
+bd (refl RS iffD1) 1;
+bd (refl RS iffD1) 1;
+bd diff_not_assoc 1;
+by (asm_full_simp_tac ((simpset_of "Arith") addsimps [diff_add_inverse]) 1);
+qed "diff_mult_distrib_r";
+
+
+(*** mod ***)
+
+(* Alternativ-Beweis zu mod_nn_is_0: Spezialfall zu mod_prod_nn_is_0 *)
+(*
+val prems = goal thy "0<n ==> n mod n = 0";
+by (cut_inst_tac [("m","Suc(0)")] (mod_prod_nn_is_0 COMP impI) 1);
+by (cut_facts_tac prems 1);
+by (Asm_full_simp_tac 1);
+by (fast_tac HOL_cs 1);
+*)
+
+val prems=goal thy "0<n ==> n mod n = 0";
+by (cut_facts_tac prems 1);
+br (mod_def RS wf_less_trans) 1;
+by (asm_full_simp_tac ((simpset_of "Arith") addsimps [diff_self_eq_0,cut_def,less_eq]) 1);
+be mod_less 1;
+qed "mod_nn_is_0";
+
+val prems=goal thy "0<n ==> m mod n = (m+n) mod n";
+by (cut_facts_tac prems 1);
+by (res_inst_tac [("s","n+m"),("t","m+n")] subst 1);
+br add_commute 1;
+by (res_inst_tac [("s","n+m-n"),("P","%x.x mod n = (n + m) mod n")] subst 1);
+br diff_add_inverse 1;
+br sym 1;
+be mod_geq 1;
+by (res_inst_tac [("s","n<=n+m"),("t","~n+m<n")] subst 1);
+by (simp_tac ((simpset_of "Arith") addsimps [le_def]) 1);
+br le_add1 1;
+qed "mod_eq_add";
+
+val prems=goal thy "0<n ==> m*n mod n = 0";
+by (cut_facts_tac prems 1);
+by (nat_ind_tac "m" 1);
+by (Simp_tac 1);
+be mod_less 1;
+by (dres_inst_tac [("n","n"),("m","m1*n")] mod_eq_add 1);
+by (asm_full_simp_tac ((simpset_of "Arith") addsimps [add_commute]) 1);
+qed "mod_prod_nn_is_0";
+
+val prems=goal thy "[|0<x; m mod x = 0; n mod x = 0|] ==> (m+n) mod x = 0";
+by (cut_facts_tac prems 1);
+by (res_inst_tac [("s","m div x * x + m mod x"),("t","m")] subst 1);
+be mod_div_equality 1;
+by (res_inst_tac [("s","n div x * x + n mod x"),("t","n")] subst 1);
+be mod_div_equality 1;
+by (Asm_simp_tac 1);
+by (res_inst_tac [("s","(m div x + n div x) * x"),("t","m div x * x + n div x * x")] subst 1);
+br add_mult_distrib 1;
+be mod_prod_nn_is_0 1;
+qed "mod0_sum";
+
+val prems=goal thy "[|0<x; m mod x = 0; n mod x = 0; n<=m|] ==> (m-n) mod x = 0";
+by (cut_facts_tac prems 1);
+by (res_inst_tac [("s","m div x * x + m mod x"),("t","m")] subst 1);
+be mod_div_equality 1;
+by (res_inst_tac [("s","n div x * x + n mod x"),("t","n")] subst 1);
+be mod_div_equality 1;
+by (Asm_simp_tac 1);
+by (res_inst_tac [("s","(m div x - n div x) * x"),("t","m div x * x - n div x * x")] subst 1);
+br diff_mult_distrib_r 1;
+be mod_prod_nn_is_0 1;
+qed "mod0_diff";
+
+
+(*** div ***)
+
+val prems = goal thy "0<n ==> m*n div n = m";
+by (cut_facts_tac prems 1);
+br (mult_not_eq_mono_r RS not_imp_swap) 1;
+ba 1;
+ba 1;
+by (res_inst_tac [("P","%x.m*n div n * n = x")] (mod_div_equality RS subst) 1);
+ba 1;
+by (dres_inst_tac [("m","m")] mod_prod_nn_is_0 1);
+by (Asm_simp_tac 1);
+qed "div_prod_nn_is_m";
+
+
+(*** divides ***)
+
+val prems=goalw thy [divides_def] "0<n ==> n divides n";
+by (cut_facts_tac prems 1);
+by (forward_tac [mod_nn_is_0] 1);
+by (Asm_simp_tac 1);
+qed "divides_nn";
+
+val prems=goalw thy [divides_def] "x divides n ==> x<=n";
+by (cut_facts_tac prems 1);
+br ((mod_less COMP rev_contrapos) RS (le_def RS meta_eq_to_obj_eq RS iffD2)) 1;
+by (Asm_simp_tac 1);
+br (less_not_refl2 RS not_sym) 1;
+by (Asm_simp_tac 1);
+qed "divides_le";
+
+val prems=goalw thy [divides_def] "[|x divides m; x divides n|] ==> x divides (m+n)";
+by (cut_facts_tac prems 1);
+by (REPEAT ((dtac conjE 1) THEN (atac 2)));
+br conjI 1;
+by (dres_inst_tac [("m","0"),("n","m")] less_imp_add_less 1);
+ba 1;
+be conjI 1;
+br mod0_sum 1;
+by (ALLGOALS atac);
+qed "divides_sum";
+
+val prems=goalw thy [divides_def] "[|x divides m; x divides n; n<m|] ==> x divides (m-n)";
+by (cut_facts_tac prems 1);
+by (REPEAT ((dtac conjE 1) THEN (atac 2)));
+br conjI 1;
+be less_imp_diff_positive 1;
+be conjI 1;
+br mod0_diff 1;
+by (ALLGOALS (asm_simp_tac ((simpset_of "Arith") addsimps [le_def])));
+be less_not_sym 1;
+qed "divides_diff";
+
+
+(*** cd ***)
+
+
+val prems=goalw thy [cd_def] "0<n ==> cd n n n";
+by (cut_facts_tac prems 1);
+bd divides_nn 1;
+by (Asm_simp_tac 1);
+qed "cd_nnn";
+
+val prems=goalw thy [cd_def] "cd x m n ==> x<=m & x<=n";
+by (cut_facts_tac prems 1);
+bd conjE 1;
+ba 2;
+bd divides_le 1;
+bd divides_le 1;
+by (Asm_simp_tac 1);
+qed "cd_le";
+
+val prems=goalw thy [cd_def] "cd x m n = cd x n m";
+by (fast_tac HOL_cs 1);
+qed "cd_swap";
+
+val prems=goalw thy [cd_def] "n<m ==> cd x m n = cd x (m-n) n";
+by (cut_facts_tac prems 1);
+br iffI 1;
+bd conjE 1;
+ba 2;
+br conjI 1;
+br divides_diff 1;
+bd conjE 5;
+ba 6;
+br conjI 5;
+bd less_not_sym 5;
+bd add_diff_inverse 5;
+by (dres_inst_tac [("m","n"),("n","m-n")] divides_sum 5);
+by (ALLGOALS Asm_full_simp_tac);
+qed "cd_diff_l";
+
+val prems=goalw thy [cd_def] "m<n ==> cd x m n = cd x m (n-m)";
+by (cut_facts_tac prems 1);
+br iffI 1;
+bd conjE 1;
+ba 2;
+br conjI 1;
+br divides_diff 2;
+bd conjE 5;
+ba 6;
+br conjI 5;
+bd less_not_sym 6;
+bd add_diff_inverse 6;
+by (dres_inst_tac [("n","n-m")] divides_sum 6);
+by (ALLGOALS Asm_full_simp_tac);
+qed "cd_diff_r";
+
+
+(*** gcd ***)
+
+val prems = goalw thy [gcd_def] "0<n ==> n = gcd n n";
+by (cut_facts_tac prems 1);
+bd cd_nnn 1;
+br (select_equality RS sym) 1;
+be conjI 1;
+br allI 1;
+br impI 1;
+bd cd_le 1;
+bd conjE 2;
+ba 3;
+br le_anti_sym 2;
+by (dres_inst_tac [("x","x")] cd_le 2);
+by (dres_inst_tac [("x","n")] spec 3);
+by (ALLGOALS Asm_full_simp_tac);
+qed "gcd_nnn";
+
+val prems = goalw thy [gcd_def] "gcd m n = gcd n m";
+by (simp_tac ((simpset_of "Arith") addsimps [cd_swap]) 1);
+qed "gcd_swap";
+
+val prems=goalw thy [gcd_def] "n<m ==> gcd m n = gcd (m-n) n";
+by (cut_facts_tac prems 1);
+by (subgoal_tac "n<m ==> !x.cd x m n = cd x (m-n) n" 1);
+by (Asm_simp_tac 1);
+br allI 1;
+be cd_diff_l 1;
+qed "gcd_diff_l";
+
+val prems=goalw thy [gcd_def] "m<n ==> gcd m n = gcd m (n-m)";
+by (cut_facts_tac prems 1);
+by (subgoal_tac "m<n ==> !x.cd x m n = cd x m (n-m)" 1);
+by (Asm_simp_tac 1);
+br allI 1;
+be cd_diff_r 1;
+qed "gcd_diff_r";
+
+
+(*** pow ***)
+
+val [pow_0,pow_Suc] = nat_recs pow_def;
+store_thm("pow_0",pow_0);
+store_thm("pow_Suc",pow_Suc);
+
+goalw thy [pow_def] "m pow (n+k) = m pow n * m pow k";
+by (nat_ind_tac "k" 1);
+by (ALLGOALS (asm_simp_tac ((simpset_of "Arith") addsimps [mult_left_commute])));
+qed "pow_add_reduce";
+
+goalw thy [pow_def] "m pow n pow k = m pow (n*k)";
+by (nat_ind_tac "k" 1);
+by (ALLGOALS Asm_simp_tac);
+by (fold_goals_tac [pow_def]);
+br (pow_add_reduce RS sym) 1;
+qed "pow_pow_reduce";
+
+(*** fac ***)
+
+Addsimps(nat_recs fac_def);
diff -r 32a9fde85699 -r 5e1c0540f285 src/HOL/Hoare/Arith2.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hoare/Arith2.thy	Fri Nov 17 09:04:10 1995 +0100
@@ -0,0 +1,27 @@
+(*  Title: 	HOL/Hoare/Arith2.thy
+    ID:         $Id$
+    Author: 	Norbert Galm
+    Copyright   1995 TUM
+
+More arithmetic.
+*)
+
+Arith2 = Arith +
+
+consts
+  divides :: "[nat, nat] => bool"			(infixl 70)
+  cd	  :: "[nat, nat, nat] => bool"
+  gcd	  :: "[nat, nat] => nat"
+
+  pow	  :: "[nat, nat] => nat"			(infixl 75)
+  fac	  :: "nat => nat"
+
+defs
+  divides_def	"x divides n == 0<n & 0<x & (n mod x) = 0"
+  cd_def	"cd x m n  == x divides m & x divides n"
+  gcd_def	"gcd m n     == @x.(cd x m n) & (!y.(cd y m n) --> y<=x)"
+
+  pow_def	"m pow n     == nat_rec n (Suc 0) (%u v.m*v)"
+  fac_def	"fac m       == nat_rec m (Suc 0) (%u v.(Suc u)*v)"
+
+end
diff -r 32a9fde85699 -r 5e1c0540f285 src/HOL/Hoare/Examples.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hoare/Examples.ML	Fri Nov 17 09:04:10 1995 +0100
@@ -0,0 +1,120 @@
+(*  Title: 	HOL/Hoare/Examples.thy
+    ID:         $Id$
+    Author: 	Norbert Galm
+    Copyright   1995 TUM
+
+Various arithmetic examples.
+*)
+
+open Examples;
+
+(*** multiplication by successive addition ***)
+
+goal thy
+ "{m=0 & s=0} \
+\ WHILE m ~= a DO {s = m*b} s := s+b; m := Suc(m) END\
+\ {s = a*b}";
+by(hoare_tac 1);
+by(ALLGOALS (asm_full_simp_tac (!simpset addsimps add_ac)));
+qed "multiply_by_add";
+
+
+(*** Euclid's algorithm for GCD ***)
+
+goal thy
+" {0<A & 0<B & a=A & b=B}   \
+\ WHILE a ~= b  \
+\ DO  {0<a & 0<b & gcd A B = gcd a b} \
+\      IF a<b   \
+\      THEN   \
+\           b:=b-a   \
+\      ELSE   \
+\           a:=a-b   \
+\      END   \
+\ END   \
+\ {a = gcd A B}";
+
+by (hoare_tac 1);
+
+by (safe_tac HOL_cs);
+
+be less_imp_diff_positive 1;
+be gcd_diff_r 1;
+
+by (cut_facts_tac [less_linear] 1);
+by (cut_facts_tac [less_linear] 2);
+br less_imp_diff_positive 1;
+br gcd_diff_l 2;
+
+bd gcd_nnn 3;
+
+by (ALLGOALS (fast_tac HOL_cs));
+
+qed "Euclid_GCD";
+
+
+(*** Power by interated squaring and multiplication ***)
+
+goal thy
+" {a=A & b=B}   \
+\ c:=1;   \
+\ WHILE b~=0   \
+\ DO {A pow B = c * a pow b}   \
+\      WHILE b mod 2=0   \
+\      DO  {A pow B = c * a pow b}  \
+\           a:=a*a;   \
+\           b:=b div 2   \
+\      END;   \
+\      c:=c*a;   \
+\      b:=b-1   \
+\ END   \
+\ {c = A pow B}";
+
+by (hoare_tac 1);
+
+by (simp_tac ((simpset_of "Arith") addsimps [pow_0]) 3);
+
+by (safe_tac HOL_cs);
+
+by (subgoal_tac "a*a=a pow 2" 1);
+by (Asm_simp_tac 1);
+br (pow_pow_reduce RS ssubst) 1;
+
+by (subgoal_tac "(b div 2)*2=b" 1);
+by (subgoal_tac "0<2" 2);
+by (dres_inst_tac [("m","b")] mod_div_equality 2);
+
+by (ALLGOALS (asm_full_simp_tac ((simpset_of "Arith") addsimps [pow_0,pow_Suc,mult_assoc])));
+
+by (subgoal_tac "b~=0" 1);
+by (res_inst_tac [("n","b")] natE 1);
+by (res_inst_tac [("Q","b mod 2 ~= 0")] not_imp_swap 3);
+ba 4;
+
+by (ALLGOALS (asm_full_simp_tac ((simpset_of "Arith") addsimps [pow_0,pow_Suc,mult_assoc])));
+br mod_less 1;
+by (Simp_tac 1);
+
+qed "power_by_mult";
+
+(*** factorial ***)
+
+goal thy
+" {a=A}   \
+\ b:=1;   \
+\ WHILE a~=0    \
+\ DO  {fac A = b*fac a} \
+\      b:=b*a;   \
+\      a:=a-1   \
+\ END   \
+\ {b = fac A}";
+
+by (hoare_tac 1);
+
+by (safe_tac HOL_cs);
+
+by (res_inst_tac [("n","a")] natE 1);
+by (ALLGOALS (asm_simp_tac (!simpset addsimps [mult_assoc])));
+by (fast_tac HOL_cs 1);
+
+qed"factorial";
diff -r 32a9fde85699 -r 5e1c0540f285 src/HOL/Hoare/Examples.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hoare/Examples.thy	Fri Nov 17 09:04:10 1995 +0100
@@ -0,0 +1,20 @@
+(*  Title: 	HOL/Hoare/Examples.thy
+    ID:         $Id$
+    Author: 	Norbert Galm
+    Copyright   1995 TUM
+
+Various arithmetic examples.
+*)
+
+Examples = Hoare + Arith2 +
+
+syntax
+  "@1"	:: "nat"	("1")
+  "@2"	:: "nat"	("2")
+
+translations
+  "1" == "Suc(0)"
+  "2" == "Suc(Suc(0))"
+end
+
+
diff -r 32a9fde85699 -r 5e1c0540f285 src/HOL/Hoare/Hoare.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hoare/Hoare.ML	Fri Nov 17 09:04:10 1995 +0100
@@ -0,0 +1,254 @@
+(*  Title: 	HOL/Hoare/Hoare.ML
+    ID:         $Id$
+    Author: 	Norbert Galm & Tobias Nipkow
+    Copyright   1995 TUM
+
+The verification condition generation tactics.
+*)
+
+open Hoare;
+
+(*** Hoare rules ***)
+
+val SkipRule = prove_goalw thy [SpecDef,SkipDef]
+  "(!!s.p(s) ==> q(s)) ==> Spec p Skip q"
+  (fn prems => [fast_tac (HOL_cs addIs prems) 1]);
+
+val AssignRule = prove_goalw thy [SpecDef,AssignDef]
+  "(!!s. p s ==> q(%x.if x=v then e s else s x)) ==> Spec p (Assign v e) q"
+  (fn prems => [fast_tac (HOL_cs addIs prems) 1]);
+
+val SeqRule = prove_goalw thy [SpecDef,SeqDef]
+  "[| Spec p c (%s.q s); Spec (%s.q s) c' r |] ==> Spec p (Seq c c') r"
+  (fn prems => [cut_facts_tac prems 1, fast_tac HOL_cs 1]);
+
+val IfRule = prove_goalw thy [SpecDef,CondDef]
+  "[| !!s. p s ==> (b s --> q s) & (~b s --> q' s); \
+\     Spec (%s.q s) c r; Spec (%s.q' s) c' r |] \
+\  ==> Spec p (Cond b c c') r"
+  (fn [prem1,prem2,prem3] =>
+     [REPEAT (rtac allI 1),
+      REPEAT (rtac impI 1),
+      dresolve_tac [prem1] 1,
+      cut_facts_tac [prem2,prem3] 1,
+      fast_tac (HOL_cs addIs [prem1]) 1]);
+
+val strenthen_pre = prove_goalw thy [SpecDef]
+  "[| !!s. p s ==> p' s; Spec p' c q |] ==> Spec p c q"
+  (fn [prem1,prem2] =>[cut_facts_tac [prem2] 1,
+		       fast_tac (HOL_cs addIs [prem1]) 1]);
+
+val [iter_0,iter_Suc] = nat_recs IterDef;
+
+val lemma = prove_goalw thy [SpecDef,WhileDef]
+  "[| Spec (%s.inv s & b s) c inv; !!s. [| inv s; ~b s |] ==> q s |] \
+\  ==> Spec inv (While b inv c) q"
+  (fn [prem1,prem2] =>
+     [REPEAT(rtac allI 1), rtac impI 1, etac exE 1, rtac mp 1, atac 2,
+      etac thin_rl 1, res_inst_tac[("x","s")]spec 1,
+      res_inst_tac[("x","s'")]spec 1, nat_ind_tac "n" 1,
+      simp_tac (!simpset addsimps [iter_0]) 1,
+      fast_tac (HOL_cs addIs [prem2]) 1,
+      simp_tac (!simpset addsimps [iter_Suc,SeqDef]) 1,
+      cut_facts_tac [prem1] 1, fast_tac (HOL_cs addIs [prem2]) 1]);
+
+val WhileRule = lemma RSN (2,strenthen_pre);
+
+
+(*** meta_spec used in StateElimTac ***)
+
+val meta_spec = prove_goal HOL.thy
+  "(!!s x. PROP P s x) ==> (!!s. PROP P s (x s))"
+  (fn prems => [resolve_tac prems 1]);
+
+
+(**************************************************************************************************)
+(*** Funktion zum Generieren eines Theorems durch Umbennenen von Namen von Lambda-Abstraktionen ***)
+(*** in einem bestehenden Theorem. Bsp.: "!a.?P(a) ==> ?P(?x)" aus "!x.?P(x) ==> ?P(?x)"        ***)
+(**************************************************************************************************)
+
+(* rename_abs:term (von:string,nach:string,trm:term) benennt in trm alle Lambda-Abstraktionen
+   mit Namen von in nach um *)
+
+fun rename_abs (von,nach,Abs (s,t,trm))	=if von=s
+						then Abs (nach,t,rename_abs (von,nach,trm))
+						else Abs (s,t,rename_abs (von,nach,trm))
+  | rename_abs (von,nach,trm1 $ trm2)	=rename_abs (von,nach,trm1) $ rename_abs (von,nach,trm2)
+  | rename_abs (_,_,trm)		=trm;
+
+(* ren_abs_thm:thm (von:string,nach:string,theorem:thm) benennt in theorem alle Lambda-Abstraktionen
+   mit Namen von in nach um. Vorgehen:
+	- Term t zu thoerem bestimmen
+	- Term t' zu t durch Umbenennen der Namen generieren
+	- Certified Term ct' zu t' erstellen
+	- Thoerem ct'==ct' anlegen
+	- Nach der Regel "[|P==Q; P|] ==> Q" wird aus "ct'==ct'" und theorem das Theorem zu ct'
+	  abgeleitet (ist moeglich, da t' mit t unifiziert werden kann, da nur Umnbenennungen) *)
+
+fun ren_abs_thm (von,nach,theorem)	=
+	equal_elim
+		(
+			reflexive (
+				cterm_of
+					(#sign (rep_thm theorem))
+					(rename_abs (von,nach,#prop (rep_thm theorem)))
+			)
+		)
+		theorem;
+
+
+(**************************************************************************************************)
+(*** Taktik zum Anwenden eines Theorems theorem auf ein Subgoal i durch                         ***)
+(***  - Umbenennen von Lambda-Abstraktionen im Theorem                                          ***)
+(***  - Instanziieren von freien Variablen im Theorem                                           ***)
+(***  - Composing des Subgoals mit dem Theorem                                                  ***)
+(**************************************************************************************************)
+
+(* - rens:(string*string) list, d.h. es koennen verschiedene Lambda-Abstraktionen umbenannt werden
+   - insts:(cterm*cterm) list, d.h. es koennen verschiedene Variablen instanziiert werden *)
+
+fun comp_inst_ren_tac rens insts theorem i	=
+	let
+		fun compose_inst_ren_tac [] insts theorem i			=
+			compose_tac (false,cterm_instantiate insts theorem,nprems_of theorem) i
+		  | compose_inst_ren_tac ((von,nach)::rl) insts theorem i	=
+			compose_inst_ren_tac rl insts (ren_abs_thm (von,nach,theorem)) i
+	in
+		compose_inst_ren_tac rens insts theorem i
+	end;
+
+
+(**************************************************************************************************)
+(*** Taktik zum Eliminieren des Zustandes waehrend Hoare-Beweisen                               ***)
+(***    Bsp.: "!!s. s(Suc(0))=0 --> s(Suc(0))+1=1" wird zu "!!s b. b=0 --> b+1=1"               ***)
+(**************************************************************************************************)
+
+(* pvars_of_term:term list (name:string,trm:term) gibt die Liste aller Programm-Variablen
+   aus trm zurueck. name gibt dabei den Namen der Zustandsvariablen an.
+	Bsp.: bei name="s" und dem Term "s(Suc(Suc(0)))=s(0)" (entspricht "c=a")
+	      wird [0,Suc(Suc(0))] geliefert (Liste ist i.A. unsortiert) *)
+
+fun pvars_of_term (name,trm)	=
+	let
+		fun add_vars (name,Free (s,t) $ trm,vl)	=if name=s
+								then if trm mem vl
+									then vl
+									else trm::vl
+								else add_vars (name,trm,vl)
+		  | add_vars (name,Abs (s,t,trm),vl)	=add_vars (name,trm,vl)
+		  | add_vars (name,trm1 $ trm2,vl)	=add_vars (name,trm2,add_vars (name,trm1,vl))
+		  | add_vars (_,_,vl)			=vl
+	in
+		add_vars (name,trm,[])
+	end;
+
+(* VarsElimTac: Taktik zum Eliminieren von bestimmten Programmvariablen aus dem Subgoal i
+   - v::vl:(term) list	Liste der zu eliminierenden Programmvariablen
+   - meta_spec:thm	Theorem, welches zur Entfernung der Variablen benutzt wird
+			z.B.: "(!!s x.PROP P(s,x)) ==> (!!s.PROP P(s,x(s)))"
+   - namexAll:string	Name von    ^                                  (hier "x")
+   - varx:term		Term zu                                      ^ (hier Var(("x",0),...))
+   - varP:term		Term zu                                  ^     (hier Var(("P",0),...))
+   - type_pvar:typ	Typ der Programmvariablen (d.h. 'a bei 'a prog, z.B.: nat, bool, ...)
+
+   Vorgehen:
+	- eliminiere jede pvar durch Anwendung von comp_inst_ren_tac. Dazu:
+	- Unbenennung in meta_spec: namexAll wird in den Namen der Prog.-Var. umbenannt
+	  z.B.: fuer die Prog.-Var. mit Namen "a" ergibt sich
+		meta_spec zu "(!! s a.PROP P(s,a)) ==> (!! s.PROP P(s,x(s)))"
+	- Instanziierungen in meta_spec:
+		varx wird mit "%s:(type_pvar) state.s(pvar)" instanziiert
+		varP wird entsprechend instanziiert. Beispiel fuer Prog.-Var. "a":
+		 -	zu Subgoal "!!s.s(Suc(0)) = s(0) ==> s(0) = 1" bestimme Term ohne "!!s.":
+			trm0 = "s(Suc(0)) = s(0) ==> s(0) = 1" (s ist hier freie Variable)
+		 -	substituiere alle Vorkommen von s(pvar) durch eine freie Var. xs:
+			trm1 = "s(Suc(0)) = xs ==> xs = 1"
+		 -	abstrahiere ueber xs:
+			trm2 = "%xs.s(Suc(0)) = xs ==> xs = 1"
+		 -	abstrahiere ueber restliche Vorkommen von s:
+			trm3 = "%s xs.s(Suc(0)) = xs ==> xs = 1"
+		 -	instanziiere varP mit trm3
+*)
+
+fun VarsElimTac ([],_,_,_,_,_) i					=all_tac
+  | VarsElimTac (v::vl,meta_spec,namexAll,varx,varP,type_pvar) i	=
+	STATE (
+		fn state =>
+		comp_inst_ren_tac
+			[(namexAll,pvar2pvarID v)]
+			[(
+				cterm_of (#sign (rep_thm state)) varx,
+				cterm_of (#sign (rep_thm state)) (
+					Abs  ("s",Type ("nat",[]) --> type_pvar,Bound 0 $ v)
+				)
+			),(
+				cterm_of (#sign (rep_thm state)) varP,
+				cterm_of (#sign (rep_thm state)) (
+					let
+						val (_,_,_ $ Abs (_,_,trm),_) = dest_state (state,i);
+						val (sname,trm0) = variant_abs ("s",dummyT,trm);
+						val xsname = variant_name ("xs",trm0);
+						val trm1 = subst_term (Free (sname,dummyT) $ v,Syntax.free xsname,trm0)
+						val trm2 = Abs ("xs",type_pvar,abstract_over (Syntax.free xsname,trm1))
+					in
+						Abs ("s",Type ("nat",[]) --> type_pvar,abstract_over (Free (sname,dummyT),trm2))
+					end
+				)
+			)]
+			meta_spec i
+	)
+	THEN
+	(VarsElimTac (vl,meta_spec,namexAll,varx,varP,type_pvar) i);
+
+(* StateElimTac: Taktik zum Eliminieren aller Programmvariablen aus dem Subgoal i
+
+   zur Erinnerung:
+    -	das Subgoal hat vor Anwendung dieser Taktik die Form "!!s:('a) state.P(s)",
+	d.h. den Term Const("all",_) $ Abs ("s",pvar --> 'a,_)
+    -   meta_spec hat die Form "(!!s x.PROP P(s,x)) ==> (!!s.PROP P(s,x(s)))"
+*)
+
+fun StateElimTac i	=
+	STATE (
+		fn state =>
+		let
+			val (_,_,_ $ Abs (_,Type ("fun",[_,type_pvar]),trm),_) = dest_state (state,i);
+			val _ $ (_ $ Abs (_,_,_ $ Abs (namexAll,_,_))) $
+			        (_ $ Abs (_,_,varP $ _ $ (varx $ _))) = #prop (rep_thm meta_spec)
+		in
+			VarsElimTac (pvars_of_term (variant_abs ("s",dummyT,trm)),meta_spec,namexAll,varx,varP,type_pvar) i
+		end
+	);
+
+
+
+(*** tactics for verification condition generation ***)
+
+(* pre_cond:bool gibt an, ob das Subgoal von der Form Spec(?Q,c,p) ist oder nicht. Im Fall
+   von pre_cond=false besteht die Vorbedingung nur nur aus einer scheme-Variable. Die dann
+   generierte Verifikationsbedingung hat die Form "!!s.?Q --> ...". "?Q" kann deshalb zu gegebenen
+   Zeitpunkt mittels "rtac impI" und "atac" gebunden werden, die Bedingung loest sich dadurch auf. *)
+
+fun WlpTac i = (rtac SeqRule i) THEN (HoareRuleTac (i+1) false)
+and HoareRuleTac i pre_cond =
+      STATE(fn state =>
+		((WlpTac i) THEN (HoareRuleTac i pre_cond))
+                ORELSE
+		(FIRST[rtac SkipRule i,
+		       rtac AssignRule i,
+		       EVERY[rtac IfRule i,
+                             HoareRuleTac (i+2) false,
+                             HoareRuleTac (i+1) false],
+		       EVERY[rtac WhileRule i,
+                             Asm_full_simp_tac (i+2),
+                             HoareRuleTac (i+1) true]]
+		 THEN
+                 (if pre_cond then (Asm_full_simp_tac i) else (atac i))
+		)
+	);
+
+val HoareTac1 =
+  EVERY[HoareRuleTac 1 true, ALLGOALS StateElimTac, prune_params_tac];
+
+val hoare_tac = SELECT_GOAL (HoareTac1);
+
diff -r 32a9fde85699 -r 5e1c0540f285 src/HOL/Hoare/Hoare.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hoare/Hoare.thy	Fri Nov 17 09:04:10 1995 +0100
@@ -0,0 +1,178 @@
+(*  Title: 	HOL/Hoare/Hoare.thy
+    ID:         $Id$
+    Author: 	Norbert Galm & Tobias Nipkow
+    Copyright   1995 TUM
+
+Sugared semantic embedding of Hoare logic.
+*)
+
+Hoare = Arith +
+
+types
+  'a prog			(* program syntax *)
+  pvar = "nat"			(* encoding of program variables ( < 26! ) *)
+  'a state = "pvar => 'a"	(* program state *)
+  'a exp ="'a state => 'a"	(* denotation of expressions *)
+  'a bexp = "'a state => bool"  (* denotation of boolean expressions *)
+  'a com = "'a state => 'a state => bool" (* denotation of programs *)
+
+syntax
+  "@Skip"       :: "'a prog"				("SKIP")
+  "@Assign"	:: "[id, 'a] => 'a prog"		("_ := _")
+  "@Seq"	:: "['a prog, 'a prog] => 'a prog"	("_;//_" [0,1000] 999)
+  "@If"		:: "[bool, 'a prog, 'a prog] => 'a prog"
+                   ("IF _//THEN//  (_)//ELSE//  (_)//END")
+  "@While"	:: "[bool, bool, 'a prog] => 'a prog"
+                   ("WHILE _//DO {_}//  (_)//END")
+
+  "@Spec"	:: "[bool, 'a prog, bool] => bool"	("{_}//_//{_}")
+
+consts
+  (* semantics *)
+
+  Skip		:: "'a com"
+  Assign	:: "[pvar, 'a exp] => 'a com"
+  Seq		:: "['a com, 'a com] => 'a com"
+  Cond		:: "['a bexp, 'a com, 'a com] => 'a com"
+  While		:: "['a bexp, 'a bexp, 'a com] => 'a com"
+  Iter		:: "[nat, 'a bexp, 'a com] => 'a com"
+
+  Spec		:: "['a bexp, 'a com, 'a bexp] => bool"
+
+defs
+  (* denotational semantics *)
+
+  SkipDef	"Skip s s' == (s=s')"
+  AssignDef	"Assign v e s s' == (s' = (%x.if x=v then e(s) else s(x)))"
+  SeqDef	"Seq c c' s s' == ? s''. c s s'' & c' s'' s'"
+  CondDef	"Cond b c c' s s' == (b(s) --> c s s') & (~b s --> c' s s')"
+  WhileDef	"While b inv c s s' == ? n. Iter n b c s s'"
+
+  IterDef	"Iter n b c == nat_rec n (%s s'.~b(s) & (s=s'))
+		           (%n_rec iter_rec.%s s'.b(s) & Seq c iter_rec s s')"
+
+  SpecDef	"Spec p c q == !s s'. c s s' --> p s --> q s'"
+
+end
+
+ML
+
+
+(*** term manipulation ***)
+
+(* name_in_term:bool (name:string,trm:term) bestimmt, ob in trm der Name name als Konstante,
+   freie Var., scheme-Variable oder als Name fuer eine Lambda-Abstraktion vorkommt *)
+
+fun name_in_term (name,Const (s,t))	=(name=s)
+  | name_in_term (name,Free (s,t))	=(name=s)
+  | name_in_term (name,Var ((s,i),t))	=(name=s ^ makestring i)
+  | name_in_term (name,Abs (s,t,trm))	=(name=s) orelse (name_in_term (name,trm))
+  | name_in_term (name,trm1 $ trm2)	=(name_in_term (name,trm1)) orelse (name_in_term (name,trm2))
+  | name_in_term (_,_)			=false;
+
+(* variant_name:string (name:string,trm:term) liefert einen von name abgewandelten Namen (durch Anhaengen
+   von genuegend vielen "_"), der nicht in trm vorkommt. Im Gegensatz zu variant_abs beruecktsichtigt es
+   auch Namen von scheme-Variablen und von Lambda-Abstraktionen in trm *)
+
+fun variant_name (name,trm)	=if name_in_term (name,trm)
+					then variant_name (name ^ "_",trm)
+					else name;
+
+(* subst_term:term (von:term,nach:term,trm:term) liefert den Term, der aus
+trm entsteht, wenn alle Teilterme, die gleich von sind, durch nach ersetzt
+wurden *)
+
+fun subst_term (von,nach,Abs (s,t,trm))	=if von=Abs (s,t,trm)
+						then nach
+						else Abs (s,t,subst_term (von,nach,trm))
+  | subst_term (von,nach,trm1 $ trm2)	=if von=trm1 $ trm2
+						then nach
+						else subst_term (von,nach,trm1) $ subst_term (von,nach,trm2)
+  | subst_term (von,nach,trm)		=if von=trm
+						then nach
+						else trm;
+
+
+(* Translation between program vars ("a" - "z") and their encoding as
+   natural numbers: "a" <==> 0, "b" <==> Suc(0), ..., "z" <==> 25 *)
+
+fun is_pvarID s	= size s=1 andalso "a"<=s andalso s<="z";
+
+fun pvarID2pvar s =
+  let fun rest2pvar (i,arg) =
+            if i=0 then arg else rest2pvar(i-1, Syntax.const "Suc" $ arg)
+  in rest2pvar(ord s - ord "a", Syntax.const "0") end;
+
+fun pvar2pvarID trm	=
+	let
+		fun rest2pvarID (Const("0",_),i)		=chr (i + ord "a")
+		  | rest2pvarID (Const("Suc",_) $ trm,i)	=rest2pvarID (trm,i+1)
+	in
+		rest2pvarID (trm,0)
+	end;
+
+
+(*** parse translations: syntax -> semantics ***)
+
+(* term_tr:term (name:string,trm:term) ersetzt in trm alle freien Variablen, die eine pvarID
+   darstellen, durch name $ pvarID2pvar(pvarID). Beispiel:
+   bei name="s" und dem Term "a=b & a=X" wird der Term "s(0)=s(Suc(0)) & s(0)=X" geliefert *)
+
+fun term_tr (name,Free (s,t)) = if is_pvarID s
+				then Syntax.free name $ pvarID2pvar s
+				else Free (s,t)
+  | term_tr (name,Abs (s,t,trm)) = Abs (s,t,term_tr (name,trm))
+  | term_tr (name,trm1 $ trm2)	= term_tr (name,trm1) $ term_tr (name,trm2)
+  | term_tr (name,trm) = trm;
+
+fun bool_tr B =
+  let val name = variant_name("s",B)
+  in Abs (name,dummyT,abstract_over (Syntax.free name,term_tr (name,B))) end;
+
+fun exp_tr E =
+  let val name = variant_name("s",E)
+  in Abs (name,dummyT,abstract_over (Syntax.free name,term_tr (name,E))) end;
+
+fun prog_tr (Const ("@Skip",_))	= Syntax.const "Skip"
+  | prog_tr (Const ("@Assign",_) $ Free (V,_) $ E) =
+      if is_pvarID V
+      then Syntax.const "Assign" $ pvarID2pvar V $ exp_tr E
+      else error("Not a valid program variable: " ^ quote V)
+  | prog_tr (Const ("@Seq",_) $ C $ C')	=
+      Syntax.const "Seq" $ prog_tr C $ prog_tr C'
+  | prog_tr (Const ("@If",_) $ B $ C $ C') =
+      Syntax.const "Cond" $ bool_tr B $ prog_tr C $ prog_tr C'
+  | prog_tr (Const ("@While",_) $ B $ INV $ C) =
+      Syntax.const "While" $ bool_tr B $ bool_tr INV $ prog_tr C;
+
+fun spec_tr [P,C,Q] = Syntax.const "Spec" $ bool_tr P $ prog_tr C $ bool_tr Q;
+
+val parse_translation = [("@Spec",spec_tr)];
+
+
+(*** print translations: semantics -> syntax ***)
+
+(* term_tr':term (name:string,trm:term) ersetzt in trm alle Vorkommen von name $ pvar durch
+   entsprechende freie Variablen, welche die pvarID zu pvar darstellen. Beispiel:
+	bei name="s" und dem Term "s(0)=s(Suc(0)) & s(0)=X" wird der Term "a=b & a=X" geliefert *)
+
+fun term_tr' (name,Free (s,t) $ trm)	=if name=s
+						then Syntax.free (pvar2pvarID trm)
+						else Free (s,t) $ term_tr' (name,trm)
+  | term_tr' (name,Abs (s,t,trm))	=Abs (s,t,term_tr' (name,trm))
+  | term_tr' (name,trm1 $ trm2)		=term_tr' (name,trm1) $ term_tr' (name,trm2)
+  | term_tr' (name,trm)			=trm;
+
+fun bexp_tr' (Abs(_,_,b))	=term_tr' (variant_abs ("s",dummyT,b));
+
+fun exp_tr' (Abs(_,_,e))	=term_tr' (variant_abs ("s",dummyT,e));
+
+fun com_tr' (Const ("Skip",_))			=Syntax.const "@Skip"
+  | com_tr' (Const ("Assign",_) $ v $ e)		=Syntax.const "@Assign" $ Syntax.free (pvar2pvarID v) $ exp_tr' e
+  | com_tr' (Const ("Seq",_) $ c $ c')		=Syntax.const "@Seq" $ com_tr' c $ com_tr' c'
+  | com_tr' (Const ("Cond",_) $ b $ c $ c')		=Syntax.const "@If" $ bexp_tr' b $ com_tr' c $ com_tr' c'
+  | com_tr' (Const ("While",_) $ b $ inv $ c)	=Syntax.const "@While" $ bexp_tr' b $ bexp_tr' inv $ com_tr' c;
+
+fun spec_tr' [p,c,q]		=Syntax.const "@Spec" $ bexp_tr' p $ com_tr' c $ bexp_tr' q;
+
+val print_translation	=[("Spec",spec_tr')];
diff -r 32a9fde85699 -r 5e1c0540f285 src/HOL/Hoare/README.html
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hoare/README.html	Fri Nov 17 09:04:10 1995 +0100
@@ -0,0 +1,36 @@
+<HTML><HEAD><TITLE>HOL/Hoare/ReadMe</TITLE></HEAD><BODY>
+
+<H2>Semantic Embedding of Hoare Logic</H2>
+
+This directory contains a sugared shallow semantic embedding of Hoare logic
+for a while language. The implementation closely follows<P>
+
+
+Mike Gordon.
+<cite>Mechanizing Programming Logics in Higher Order Logic.</cite><BR>
+University of Cambridge, Computer Laboratory, TR 145, 1988.<P>
+
+published as<P>
+
+Mike Gordon.
+<cite>Mechanizing Programming Logics in Higher Order Logic.</cite><BR>
+In
+<cite>Current Trends in Hardware Verification and Automated Theorem Proving
+</cite>,<BR>
+edited by G. Birtwistle and P.A. Subrahmanyam, Springer-Verlag, 1989. 
+<P>
+
+At the top level, it provides a tactic <B>hoare_tac</B>, which transforms a
+goal
+<BLOCKQUOTE>
+<KBD>{P} prog {Q}</KBD>
+</BLOCKQUOTE>
+into a set of HOL-level verification conditions.
+<DL>
+<DT>Syntax:
+<DD> the letters a-z are interpreted as program variables,
+     all other identifiers as mathematical variables.<P>
+</DL>
+The pre/post conditions can be arbitrary HOL formulae including program
+variables. The program text should only refer to program variables.
+</BODY></HTML>
diff -r 32a9fde85699 -r 5e1c0540f285 src/HOL/Hoare/ROOT.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hoare/ROOT.ML	Fri Nov 17 09:04:10 1995 +0100
@@ -0,0 +1,12 @@
+(*  Title: 	HOL/IMP/ROOT.ML
+    ID:         $Id$
+    Author: 	Tobias Nipkow
+    Copyright   1995 TUM
+*)
+
+HOL_build_completed;	(*Make examples fail if HOL did*)
+
+loadpath := ["Hoare"];
+use_thy "Examples";
+
+make_chart ();   (*make HTML chart*)