# HG changeset patch
# User clasohm
# Date 823552146 -3600
# Node ID 608483c2122a991faf122e3fe93ca12ac23f10cf
# Parent  7f5a4cd082091d0efd0c89b955053c0f3372ff4a
expanded tabs; incorporated Konrad's changes

diff -r 7f5a4cd08209 -r 608483c2122a src/HOL/AxClasses/Lattice/OrdDefs.thy
--- a/src/HOL/AxClasses/Lattice/OrdDefs.thy	Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/AxClasses/Lattice/OrdDefs.thy	Mon Feb 05 21:29:06 1996 +0100
@@ -23,7 +23,7 @@
 
 (* duals *)
 
-subtype
+typedef
   'a dual = "{x::'a. True}"
 
 instance
diff -r 7f5a4cd08209 -r 608483c2122a src/HOL/Hoare/Arith2.ML
--- a/src/HOL/Hoare/Arith2.ML	Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/Hoare/Arith2.ML	Mon Feb 05 21:29:06 1996 +0100
@@ -30,16 +30,16 @@
 \       !!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);
-by (rtac diff_induct 1);
-by (rtac allI 1);
-by (rtac allI 2);
+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);
-by (rtac allI 7);
+br allI 7;
 by (nat_ind_tac "xa" 7);
 by (ALLGOALS (resolve_tac prems));
-by (assume_tac 1);
-by (assume_tac 1);
+ba 1;
+ba 1;
 by (fast_tac HOL_cs 1);
 by (fast_tac HOL_cs 1);
 qed "diff_induct3";
@@ -48,33 +48,33 @@
 
 val prems=goal Arith.thy "~m<n+k ==> (m - n) - k = m - ((n + k)::nat)";
 by (cut_facts_tac prems 1);
-by (rtac mp 1);
-by (assume_tac 2);
+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);
-by (dtac conjI 1);
-by (assume_tac 1);
+bd conjI 1;
+ba 1;
 by (res_inst_tac [("P","~m<n & ~n<k")] mp 1);
-by (assume_tac 2);
+ba 2;
 by (res_inst_tac [("m","m"),("n","n"),("k","k")] diff_induct3 1);
 by (ALLGOALS Asm_simp_tac);
-by (rtac impI 1);
+br impI 1;
 by (dres_inst_tac [("P","~x<y")] conjE 1);
-by (assume_tac 2);
-by (rtac (Suc_diff_n RS sym) 1);
-by (rtac le_less_trans 1);
-by (etac (not_less_eq RS subst) 2);
-by (rtac (hd ([diff_less_Suc RS lessD] RL [Suc_le_mono RS subst])) 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);
-by (rtac mp 1);
-by (assume_tac 2);
+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";
@@ -82,12 +82,12 @@
 (*** more ***)
 
 val prems = goal Arith.thy "m~=(n::nat) = (m<n | n<m)";
-by (rtac iffI 1);
+br iffI 1;
 by (cut_inst_tac [("m","m"),("n","n")] less_linear 1);
 by (Asm_full_simp_tac 1);
-by (etac disjE 1);
-by (etac (less_not_refl2 RS not_sym) 1);
-by (etac less_not_refl2 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";
@@ -115,7 +115,7 @@
 by (res_inst_tac [("n","k")] natE 1);
 by (ALLGOALS Asm_full_simp_tac);
 by (nat_ind_tac "x" 1);
-by (etac add_less_mono 2);
+be add_less_mono 2;
 by (ALLGOALS Asm_full_simp_tac);
 qed "mult_less_mono_r";
 
@@ -124,8 +124,8 @@
 by (nat_ind_tac "k" 1);
 by (ALLGOALS Simp_tac);
 by (fold_goals_tac [le_def]);
-by (etac add_le_mono 1);
-by (assume_tac 1);
+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";
@@ -137,10 +137,10 @@
 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);
-by (rtac (less_not_refl2 RS not_sym) 2);
-by (etac mult_less_mono_r 2);
-by (rtac less_not_refl2 3);
-by (etac mult_less_mono_r 3);
+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";
 
@@ -149,24 +149,29 @@
 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);
-by (dtac (less_not_sym RS (not_less_eq RS iffD1) RS less_imp_diff_is_0) 1);
-by (dtac (less_not_sym RS (not_less_eq RS iffD1) RS less_imp_diff_is_0) 1);
-by (rtac mp 2);
-by (assume_tac 3);
+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);
-by (rtac impI 1);
-by (dtac (refl RS iffD1) 1);
+br impI 1;
+bd (refl RS iffD1) 1;
 by (dres_inst_tac [("k","k")] add_not_less_mono_l 1);
-by (dtac (refl RS iffD1) 1);
-by (dtac (refl RS iffD1) 1);
-by (dtac diff_not_assoc 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 ***)
 
+goal Arith.thy "(%m. m mod n) = wfrec (trancl pred_nat) \
+             \                      (%f j. if j<n then j else f (j-n))";
+by (simp_tac (HOL_ss addsimps [mod_def]) 1);
+val mod_def = result() RS eq_reflection;
+
 (* Alternativ-Beweis zu mod_nn_is_0: Spezialfall zu mod_prod_nn_is_0 *)
 (*
 val prems = goal thy "0<n ==> n mod n = 0";
@@ -178,29 +183,29 @@
 
 val prems=goal thy "0<n ==> n mod n = 0";
 by (cut_facts_tac prems 1);
-by (rtac (mod_def RS wf_less_trans) 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);
-by (etac mod_less 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);
-by (rtac add_commute 1);
+br add_commute 1;
 by (res_inst_tac [("s","n+m-n"),("P","%x.x mod n = (n + m) mod n")] subst 1);
-by (rtac diff_add_inverse 1);
-by (rtac sym 1);
-by (etac mod_geq 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);
-by (rtac le_add1 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);
-by (etac mod_less 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";
@@ -208,37 +213,38 @@
 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);
-by (etac mod_div_equality 1);
+be mod_div_equality 1;
 by (res_inst_tac [("s","n div x * x + n mod x"),("t","n")] subst 1);
-by (etac mod_div_equality 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);
-by (rtac add_mult_distrib 1);
-by (etac mod_prod_nn_is_0 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);
-by (etac mod_div_equality 1);
+be mod_div_equality 1;
 by (res_inst_tac [("s","n div x * x + n mod x"),("t","n")] subst 1);
-by (etac mod_div_equality 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);
-by (rtac diff_mult_distrib_r 1);
-by (etac mod_prod_nn_is_0 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);
-by (rtac (mult_not_eq_mono_r RS not_imp_swap) 1);
-by (assume_tac 1);
-by (assume_tac 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);
-by (assume_tac 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";
@@ -254,32 +260,32 @@
 
 val prems=goalw thy [divides_def] "x divides n ==> x<=n";
 by (cut_facts_tac prems 1);
-by (rtac ((mod_less COMP rev_contrapos) RS (le_def RS meta_eq_to_obj_eq RS iffD2)) 1);
+br ((mod_less COMP rev_contrapos) RS (le_def RS meta_eq_to_obj_eq RS iffD2)) 1;
 by (Asm_simp_tac 1);
-by (rtac (less_not_refl2 RS not_sym) 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)));
-by (rtac conjI 1);
+br conjI 1;
 by (dres_inst_tac [("m","0"),("n","m")] less_imp_add_less 1);
-by (assume_tac 1);
-by (etac conjI 1);
-by (rtac mod0_sum 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)));
-by (rtac conjI 1);
-by (etac less_imp_diff_positive 1);
-by (etac conjI 1);
-by (rtac mod0_diff 1);
+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])));
-by (etac less_not_sym 1);
+be less_not_sym 1;
 qed "divides_diff";
 
 
@@ -288,16 +294,16 @@
 
 val prems=goalw thy [cd_def] "0<n ==> cd n n n";
 by (cut_facts_tac prems 1);
-by (dtac divides_nn 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);
-by (dtac conjE 1);
-by (assume_tac 2);
-by (dtac divides_le 1);
-by (dtac divides_le 1);
+bd conjE 1;
+ba 2;
+bd divides_le 1;
+bd divides_le 1;
 by (Asm_simp_tac 1);
 qed "cd_le";
 
@@ -307,32 +313,32 @@
 
 val prems=goalw thy [cd_def] "n<m ==> cd x m n = cd x (m-n) n";
 by (cut_facts_tac prems 1);
-by (rtac iffI 1);
-by (dtac conjE 1);
-by (assume_tac 2);
-by (rtac conjI 1);
-by (rtac divides_diff 1);
-by (dtac conjE 5);
-by (assume_tac 6);
-by (rtac conjI 5);
-by (dtac less_not_sym 5);
-by (dtac add_diff_inverse 5);
+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);
-by (rtac iffI 1);
-by (dtac conjE 1);
-by (assume_tac 2);
-by (rtac conjI 1);
-by (rtac divides_diff 2);
-by (dtac conjE 5);
-by (assume_tac 6);
-by (rtac conjI 5);
-by (dtac less_not_sym 6);
-by (dtac add_diff_inverse 6);
+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";
@@ -342,15 +348,15 @@
 
 val prems = goalw thy [gcd_def] "0<n ==> n = gcd n n";
 by (cut_facts_tac prems 1);
-by (dtac cd_nnn 1);
-by (rtac (select_equality RS sym) 1);
-by (etac conjI 1);
-by (rtac allI 1);
-by (rtac impI 1);
-by (dtac cd_le 1);
-by (dtac conjE 2);
-by (assume_tac 3);
-by (rtac le_anti_sym 2);
+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);
@@ -364,16 +370,16 @@
 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);
-by (rtac allI 1);
-by (etac cd_diff_l 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);
-by (rtac allI 1);
-by (etac cd_diff_r 1);
+br allI 1;
+be cd_diff_r 1;
 qed "gcd_diff_r";
 
 
@@ -392,7 +398,7 @@
 by (nat_ind_tac "k" 1);
 by (ALLGOALS Asm_simp_tac);
 by (fold_goals_tac [pow_def]);
-by (rtac (pow_add_reduce RS sym) 1);
+br (pow_add_reduce RS sym) 1;
 qed "pow_pow_reduce";
 
 (*** fac ***)
diff -r 7f5a4cd08209 -r 608483c2122a src/HOL/Hoare/Arith2.thy
--- a/src/HOL/Hoare/Arith2.thy	Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/Hoare/Arith2.thy	Mon Feb 05 21:29:06 1996 +0100
@@ -1,6 +1,6 @@
-(*  Title: 	HOL/Hoare/Arith2.thy
+(*  Title:      HOL/Hoare/Arith2.thy
     ID:         $Id$
-    Author: 	Norbert Galm
+    Author:     Norbert Galm
     Copyright   1995 TUM
 
 More arithmetic.
@@ -9,19 +9,19 @@
 Arith2 = Arith +
 
 consts
-  divides :: [nat, nat] => bool			(infixl 70)
-  cd	  :: [nat, nat, nat] => bool
-  gcd	  :: [nat, nat] => nat
+  divides :: [nat, nat] => bool                 (infixl 70)
+  cd      :: [nat, nat, nat] => bool
+  gcd     :: [nat, nat] => nat
 
-  pow	  :: [nat, nat] => nat			(infixl 75)
-  fac	  :: 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)"
+  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)"
+  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 7f5a4cd08209 -r 608483c2122a src/HOL/Hoare/Examples.thy
--- a/src/HOL/Hoare/Examples.thy	Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/Hoare/Examples.thy	Mon Feb 05 21:29:06 1996 +0100
@@ -1,6 +1,6 @@
-(*  Title: 	HOL/Hoare/Examples.thy
+(*  Title:      HOL/Hoare/Examples.thy
     ID:         $Id$
-    Author: 	Norbert Galm
+    Author:     Norbert Galm
     Copyright   1995 TUM
 
 Various arithmetic examples.
@@ -9,8 +9,8 @@
 Examples = Hoare + Arith2 +
 
 syntax
-  "@1"	:: nat	("1")
-  "@2"	:: nat	("2")
+  "@1"  :: nat  ("1")
+  "@2"  :: nat  ("2")
 
 translations
   "1" == "Suc(0)"
diff -r 7f5a4cd08209 -r 608483c2122a src/HOL/Hoare/Hoare.thy
--- a/src/HOL/Hoare/Hoare.thy	Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/Hoare/Hoare.thy	Mon Feb 05 21:29:06 1996 +0100
@@ -1,6 +1,6 @@
-(*  Title: 	HOL/Hoare/Hoare.thy
+(*  Title:      HOL/Hoare/Hoare.thy
     ID:         $Id$
-    Author: 	Norbert Galm & Tobias Nipkow
+    Author:     Norbert Galm & Tobias Nipkow
     Copyright   1995 TUM
 
 Sugared semantic embedding of Hoare logic.
@@ -9,49 +9,49 @@
 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 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
+  "@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"      :: [bool, bool, 'a prog] => 'a prog
                    ("WHILE _//DO {_}//  (_)//END")
 
-  "@Spec"	:: [bool, 'a prog, bool] => bool	("{_}//_//{_}")
+  "@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
+  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
+  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'"
+  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')"
+  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'"
+  SpecDef       "Spec p c q == !s s'. c s s' --> p s --> q s'"
 
 end
 
@@ -63,53 +63,53 @@
 (* 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;
+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;
+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;
+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 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;
+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 ***)
@@ -119,10 +119,10 @@
    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)
+                                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,trm1 $ trm2)  = term_tr (name,trm1) $ term_tr (name,trm2)
   | term_tr (name,trm) = trm;
 
 fun bool_tr B =
@@ -133,12 +133,12 @@
   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"
+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')	=
+  | 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'
@@ -154,25 +154,25 @@
 
 (* 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 *)
+        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 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 bexp_tr' (Abs(_,_,b))       =term_tr' (variant_abs ("s",dummyT,b));
 
-fun exp_tr' (Abs(_,_,e))	=term_tr' (variant_abs ("s",dummyT,e));
+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 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;
+fun spec_tr' [p,c,q]            =Syntax.const "@Spec" $ bexp_tr' p $ com_tr' c $ bexp_tr' q;
 
-val print_translation	=[("Spec",spec_tr')];
+val print_translation   =[("Spec",spec_tr')];
diff -r 7f5a4cd08209 -r 608483c2122a src/HOL/IMP/Com.thy
--- a/src/HOL/IMP/Com.thy	Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/IMP/Com.thy	Mon Feb 05 21:29:06 1996 +0100
@@ -1,6 +1,6 @@
-(*  Title: 	HOL/IMP/Com.thy
+(*  Title:      HOL/IMP/Com.thy
     ID:         $Id$
-    Author: 	Heiko Loetzbeyer & Robert Sandner, TUM
+    Author:     Heiko Loetzbeyer & Robert Sandner, TUM
     Copyright   1994 TUM
 
 Arithmetic expressions, Boolean expressions, Commands
@@ -32,7 +32,7 @@
 inductive "evala"
   intrs 
     N   "<N(n),s> -a-> n"
-    X  	"<X(x),s> -a-> s(x)"
+    X   "<X(x),s> -a-> s(x)"
     Op1 "<e,s> -a-> n ==> <Op1 f e,s> -a-> f(n)"
     Op2 "[| <e0,s> -a-> n0;  <e1,s>  -a-> n1 |] 
            ==> <Op2 f e0 e1,s> -a-> f n0 n1"
@@ -46,11 +46,11 @@
        | false
        | ROp  n2n2b aexp aexp
        | noti bexp
-       | andi bexp bexp 	(infixl 60)
-       | ori  bexp bexp 	(infixl 60)
+       | andi bexp bexp         (infixl 60)
+       | ori  bexp bexp         (infixl 60)
 
 (** Evaluation of boolean expressions **)
-consts evalb	:: "(bexp*state*bool)set"	
+consts evalb    :: "(bexp*state*bool)set"       
        "@evalb" :: [bexp,state,bool] => bool ("<_,_>/ -b-> _"  [0,0,50] 50)
 
 translations
@@ -61,32 +61,32 @@
     tru   "<true,s> -b-> True"
     fls   "<false,s> -b-> False"
     ROp   "[| <a0,s> -a-> n0; <a1,s> -a-> n1 |] 
-	   ==> <ROp f a0 a1,s> -b-> f n0 n1"
+           ==> <ROp f a0 a1,s> -b-> f n0 n1"
     noti  "<b,s> -b-> w ==> <noti(b),s> -b-> (~w)"
     andi  "[| <b0,s> -b-> w0; <b1,s> -b-> w1 |] 
           ==> <b0 andi b1,s> -b-> (w0 & w1)"
     ori   "[| <b0,s> -b-> w0; <b1,s> -b-> w1 |] 
-	    ==> <b0 ori b1,s> -b-> (w0 | w1)"
+            ==> <b0 ori b1,s> -b-> (w0 | w1)"
 
 (** Commands **)
 
 datatype
   com = skip
-      | ":="   loc aexp	         (infixl  60)
-      | semic  com com	         ("_; _"  [60, 60] 10)
-      | whileC bexp com	         ("while _ do _"  60)
-      | ifC    bexp com com	 ("ifc _ then _ else _"  60)
+      | ":="   loc aexp          (infixl  60)
+      | semic  com com           ("_; _"  [60, 60] 10)
+      | whileC bexp com          ("while _ do _"  60)
+      | ifC    bexp com com      ("ifc _ then _ else _"  60)
 
 (** Execution of commands **)
 consts  evalc    :: "(com*state*state)set"
         "@evalc" :: [com,state,state] => bool ("<_,_>/ -c-> _" [0,0,50] 50)
-	"assign" :: [state,nat,loc] => state  ("_[_'/_]"       [95,0,0] 95)
+        "assign" :: [state,nat,loc] => state  ("_[_'/_]"       [95,0,0] 95)
 
 translations
        "<ce,sig> -c-> s" == "(ce,sig,s) : evalc"
 
 rules 
-	assign_def	"s[m/x] == (%y. if y=x then m else s y)"
+        assign_def      "s[m/x] == (%y. if y=x then m else s y)"
 
 inductive "evalc"
   intrs
diff -r 7f5a4cd08209 -r 608483c2122a src/HOL/IMP/Denotation.thy
--- a/src/HOL/IMP/Denotation.thy	Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/IMP/Denotation.thy	Mon Feb 05 21:29:06 1996 +0100
@@ -1,6 +1,6 @@
-(*  Title: 	HOL/IMP/Denotation.thy
+(*  Title:      HOL/IMP/Denotation.thy
     ID:         $Id$
-    Author: 	Heiko Loetzbeyer & Robert Sandner, TUM
+    Author:     Heiko Loetzbeyer & Robert Sandner, TUM
     Copyright   1994 TUM
 
 Denotational semantics of expressions & commands
@@ -16,31 +16,31 @@
   Gamma :: [bexp,com_den] => (com_den => com_den)
 
 primrec A aexp
-  A_nat	"A(N(n)) = (%s. n)"
-  A_loc	"A(X(x)) = (%s. s(x))" 
-  A_op1	"A(Op1 f a) = (%s. f(A a s))"
-  A_op2	"A(Op2 f a0 a1) = (%s. f (A a0 s) (A a1 s))"
+  A_nat "A(N(n)) = (%s. n)"
+  A_loc "A(X(x)) = (%s. s(x))" 
+  A_op1 "A(Op1 f a) = (%s. f(A a s))"
+  A_op2 "A(Op2 f a0 a1) = (%s. f (A a0 s) (A a1 s))"
 
 primrec B bexp
   B_true  "B(true) = (%s. True)"
   B_false "B(false) = (%s. False)"
-  B_op	  "B(ROp f a0 a1) = (%s. f (A a0 s) (A a1 s))" 
-  B_not	  "B(noti(b)) = (%s. ~(B b s))"
-  B_and	  "B(b0 andi b1) = (%s. (B b0 s) & (B b1 s))"
-  B_or	  "B(b0 ori b1) = (%s. (B b0 s) | (B b1 s))"
+  B_op    "B(ROp f a0 a1) = (%s. f (A a0 s) (A a1 s))" 
+  B_not   "B(noti(b)) = (%s. ~(B b s))"
+  B_and   "B(b0 andi b1) = (%s. (B b0 s) & (B b1 s))"
+  B_or    "B(b0 ori b1) = (%s. (B b0 s) | (B b1 s))"
 
 defs
-  Gamma_def	"Gamma b cd ==   
-		   (%phi.{st. st : (phi O cd) & B b (fst st)} Un 
-	                 {st. st : id & ~B b (fst st)})"
+  Gamma_def     "Gamma b cd ==   
+                   (%phi.{st. st : (phi O cd) & B b (fst st)} Un 
+                         {st. st : id & ~B b (fst st)})"
 
 primrec C com
   C_skip    "C(skip) = id"
   C_assign  "C(x := a) = {st . snd(st) = fst(st)[A a (fst st)/x]}"
   C_comp    "C(c0 ; c1) = C(c1) O C(c0)"
-  C_if	    "C(ifc b then c0 else c1) =   
-		   {st. st:C(c0) & (B b (fst st))} Un 
-	           {st. st:C(c1) & ~(B b (fst st))}"
+  C_if      "C(ifc b then c0 else c1) =   
+                   {st. st:C(c0) & (B b (fst st))} Un 
+                   {st. st:C(c1) & ~(B b (fst st))}"
   C_while   "C(while b do c) = lfp (Gamma b (C c))"
 
 end
diff -r 7f5a4cd08209 -r 608483c2122a src/HOL/IMP/Equiv.thy
--- a/src/HOL/IMP/Equiv.thy	Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/IMP/Equiv.thy	Mon Feb 05 21:29:06 1996 +0100
@@ -1,6 +1,6 @@
-(*  Title: 	HOL/IMP/Equiv.thy
+(*  Title:      HOL/IMP/Equiv.thy
     ID:         $Id$
-    Author: 	Heiko Loetzbeyer & Robert Sandner, TUM
+    Author:     Heiko Loetzbeyer & Robert Sandner, TUM
     Copyright   1994 TUM
 *)
 
diff -r 7f5a4cd08209 -r 608483c2122a src/HOL/IMP/Hoare.thy
--- a/src/HOL/IMP/Hoare.thy	Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/IMP/Hoare.thy	Mon Feb 05 21:29:06 1996 +0100
@@ -1,6 +1,6 @@
-(*  Title: 	HOL/IMP/Hoare.thy
+(*  Title:      HOL/IMP/Hoare.thy
     ID:         $Id$
-    Author: 	Tobias Nipkow
+    Author:     Tobias Nipkow
     Copyright   1995 TUM
 
 Inductive definition of Hoare logic
@@ -27,8 +27,8 @@
   hoare_if   "[| {{%s. P s & B b s}}c{{Q}}; {{%s. P s & ~B b s}}d{{Q}} |] ==>
               {{P}} ifc b then c else d {{Q}}"
   hoare_while "[| {{%s. P s & B b s}} c {{P}} |] ==>
-	       {{P}} while b do c {{%s. P s & ~B b s}}"
+               {{P}} while b do c {{%s. P s & ~B b s}}"
   hoare_conseq "[| !s. P' s --> P s; {{P}}c{{Q}}; !s. Q s --> Q' s |] ==>
-		{{P'}}c{{Q'}}"
+                {{P'}}c{{Q'}}"
 
 end
diff -r 7f5a4cd08209 -r 608483c2122a src/HOL/IMP/VC.thy
--- a/src/HOL/IMP/VC.thy	Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/IMP/VC.thy	Mon Feb 05 21:29:06 1996 +0100
@@ -1,6 +1,6 @@
-(*  Title: 	HOL/IMP/VC.thy
+(*  Title:      HOL/IMP/VC.thy
     ID:         $Id$
-    Author: 	Tobias Nipkow
+    Author:     Tobias Nipkow
     Copyright   1996 TUM
 
 acom: annotated commands
diff -r 7f5a4cd08209 -r 608483c2122a src/HOL/IOA/ABP/Abschannel.thy
--- a/src/HOL/IOA/ABP/Abschannel.thy	Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/IOA/ABP/Abschannel.thy	Mon Feb 05 21:29:06 1996 +0100
@@ -56,8 +56,8 @@
       case fst(snd(tr))                                        
         of S(b) => ((t = s) | (t = s @ [b]))  |                
            R(b) => s ~= [] &                                   
-	            b = hd(s) &                                 
-	            ((t = s) | (t = tl(s)))    }"
+                    b = hd(s) &                                 
+                    ((t = s) | (t = tl(s)))    }"
   
 ch_ioa_def "ch_ioa == (ch_asig, {[]}, ch_trans)"
 
@@ -66,24 +66,24 @@
  *********************************************************)
   
 rsch_actions_def "rsch_actions (akt) ==                      
-	    case akt of   
+            case akt of   
            Next    =>  None |          
            S_msg(m) => None |         
-	    R_msg(m) => None |         
+            R_msg(m) => None |         
            S_pkt(packet) => None |    
-	    R_pkt(packet) => None |    
-	    S_ack(b) => Some(S(b)) |   
-	    R_ack(b) => Some(R(b))"
+            R_pkt(packet) => None |    
+            S_ack(b) => Some(S(b)) |   
+            R_ack(b) => Some(R(b))"
 
 srch_actions_def "srch_actions (akt) ==                      
-	    case akt of   
-	    Next    =>  None |          
+            case akt of   
+            Next    =>  None |          
            S_msg(m) => None |         
-	    R_msg(m) => None |         
+            R_msg(m) => None |         
            S_pkt(p) => Some(S(p)) |   
-	    R_pkt(p) => Some(R(p)) |   
-	    S_ack(b) => None |         
-	    R_ack(b) => None"
+            R_pkt(p) => Some(R(p)) |   
+            S_ack(b) => None |         
+            R_ack(b) => None"
 
 
 end  
diff -r 7f5a4cd08209 -r 608483c2122a src/HOL/IOA/ABP/Abschannel_finite.thy
--- a/src/HOL/IOA/ABP/Abschannel_finite.thy	Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/IOA/ABP/Abschannel_finite.thy	Mon Feb 05 21:29:06 1996 +0100
@@ -54,8 +54,8 @@
         of S(b) => ((t = s) |                                    
                    (if (b=hd(reverse(s)) & s~=[]) then  t=s else  t=s@[b])) |    
            R(b) => s ~= [] &                                   
-	            b = hd(s) &                                 
-	            ((t = s) | (t = tl(s)))    }"
+                    b = hd(s) &                                 
+                    ((t = s) | (t = tl(s)))    }"
   
 ch_fin_ioa_def "ch_fin_ioa == (ch_fin_asig, {[]}, ch_fin_trans)"
 
diff -r 7f5a4cd08209 -r 608483c2122a src/HOL/IOA/ABP/Correctness.thy
--- a/src/HOL/IOA/ABP/Correctness.thy	Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/IOA/ABP/Correctness.thy	Mon Feb 05 21:29:06 1996 +0100
@@ -20,11 +20,11 @@
   reduce List.list  
   reduce_Nil  "reduce [] = []"
   reduce_Cons "reduce(x#xs) =   
-	         (case xs of   
-	             [] => [x]   
-	       |   y#ys => (if (x=y)   
-	                      then reduce xs   
-	                      else (x#(reduce xs))))"
+                 (case xs of   
+                     [] => [x]   
+               |   y#ys => (if (x=y)   
+                              then reduce xs   
+                              else (x#(reduce xs))))"
 
   
 defs
@@ -36,8 +36,8 @@
   "system_fin_ioa == (env_ioa || impl_fin_ioa)"
   
 abs_def "abs  ==   
-	(%p.(fst(p),(fst(snd(p)),(fst(snd(snd(p))),   
-	 (reduce(fst(snd(snd(snd(p))))),reduce(snd(snd(snd(snd(p))))))))))"
+        (%p.(fst(p),(fst(snd(p)),(fst(snd(snd(p))),   
+         (reduce(fst(snd(snd(snd(p))))),reduce(snd(snd(snd(snd(p))))))))))"
 
 rules
 
diff -r 7f5a4cd08209 -r 608483c2122a src/HOL/IOA/ABP/Receiver.thy
--- a/src/HOL/IOA/ABP/Receiver.thy	Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/IOA/ABP/Receiver.thy	Mon Feb 05 21:29:06 1996 +0100
@@ -41,13 +41,13 @@
       Next    =>  False |     
       S_msg(m) => False |                                               
       R_msg(m) => (rq(s) ~= [])  &                                     
-		   m = hd(rq(s))  &                             
-		   rq(t) = tl(rq(s))   &                              
+                   m = hd(rq(s))  &                             
+                   rq(t) = tl(rq(s))   &                              
                   rbit(t)=rbit(s)  |                                 
       S_pkt(pkt) => False |                                          
       R_pkt(pkt) => if (hdr(pkt) ~= rbit(s))&rq(s)=[] then            
-		         rq(t) = (rq(s)@[msg(pkt)]) &rbit(t) = (~rbit(s)) else  
-		         rq(t) =rq(s) & rbit(t)=rbit(s)  |   
+                         rq(t) = (rq(s)@[msg(pkt)]) &rbit(t) = (~rbit(s)) else  
+                         rq(t) =rq(s) & rbit(t)=rbit(s)  |   
       S_ack(b) => b = rbit(s)                        &               
                       rq(t) = rq(s)                    &             
                       rbit(t)=rbit(s) |                              
diff -r 7f5a4cd08209 -r 608483c2122a src/HOL/IOA/ABP/Sender.thy
--- a/src/HOL/IOA/ABP/Sender.thy	Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/IOA/ABP/Sender.thy	Mon Feb 05 21:29:06 1996 +0100
@@ -41,15 +41,15 @@
                   sbit(t)=sbit(s)  |                                 
       R_msg(m) => False |                                            
       S_pkt(pkt) => sq(s) ~= []  &                                   
-		     hdr(pkt) = sbit(s)      &                        
+                     hdr(pkt) = sbit(s)      &                        
                     msg(pkt) = hd(sq(s))    &                   
                     sq(t) = sq(s)           &                        
                     sbit(t) = sbit(s) |                              
       R_pkt(pkt) => False |                                          
       S_ack(b)   => False |                                          
       R_ack(b)   => if b = sbit(s) then                              
-		     sq(t)=tl(sq(s)) & sbit(t)=(~sbit(s)) else   
-		     sq(t)=sq(s) & sbit(t)=sbit(s)}"
+                     sq(t)=tl(sq(s)) & sbit(t)=(~sbit(s)) else   
+                     sq(t)=sq(s) & sbit(t)=sbit(s)}"
 
 sender_ioa_def "sender_ioa == 
  (sender_asig, {([],True)}, sender_trans)"
diff -r 7f5a4cd08209 -r 608483c2122a src/HOL/IOA/NTP/Abschannel.thy
--- a/src/HOL/IOA/NTP/Abschannel.thy	Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/IOA/NTP/Abschannel.thy	Mon Feb 05 21:29:06 1996 +0100
@@ -57,26 +57,26 @@
 
 
 rsch_actions_def "rsch_actions (act) ==        
-	    case act of                
+            case act of                
            S_msg(m) => None |         
-	    R_msg(m) => None |         
+            R_msg(m) => None |         
            S_pkt(packet) => None |    
-	    R_pkt(packet) => None |    
-	    S_ack(b) => Some(S(b)) |   
-	    R_ack(b) => Some(R(b)) |   
+            R_pkt(packet) => None |    
+            S_ack(b) => Some(S(b)) |   
+            R_ack(b) => Some(R(b)) |   
            C_m_s =>  None  |          
            C_m_r =>  None |           
            C_r_s =>  None  |          
            C_r_r(m) => None"
 
 srch_actions_def "srch_actions (act) ==         
-	    case act of                
+            case act of                
            S_msg(m) => None |         
-	    R_msg(m) => None |         
+            R_msg(m) => None |         
            S_pkt(p) => Some(S(p)) |   
-	    R_pkt(p) => Some(R(p)) |   
-	    S_ack(b) => None |         
-	    R_ack(b) => None |         
+            R_pkt(p) => Some(R(p)) |   
+            S_ack(b) => None |         
+            R_ack(b) => None |         
            C_m_s => None |            
            C_m_r => None |            
            C_r_s => None |            
diff -r 7f5a4cd08209 -r 608483c2122a src/HOL/IOA/meta_theory/IOA.thy
--- a/src/HOL/IOA/meta_theory/IOA.thy	Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/IOA/meta_theory/IOA.thy	Mon Feb 05 21:29:06 1996 +0100
@@ -22,7 +22,7 @@
   asig_of    ::"('action,'state)ioa => 'action signature"
   starts_of  ::"('action,'state)ioa => 'state set"
   trans_of   ::"('action,'state)ioa => ('action,'state)transition set"
-  IOA	     ::"('action,'state)ioa => bool"
+  IOA        ::"('action,'state)ioa => bool"
 
   (* Executions, schedules, and traces *)
 
diff -r 7f5a4cd08209 -r 608483c2122a src/HOL/Integ/Equiv.thy
--- a/src/HOL/Integ/Equiv.thy	Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/Integ/Equiv.thy	Mon Feb 05 21:29:06 1996 +0100
@@ -1,7 +1,7 @@
-(*  Title: 	Equiv.thy
+(*  Title:      Equiv.thy
     ID:         $Id$
-    Authors: 	Riccardo Mattolini, Dip. Sistemi e Informatica
-        	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Authors:    Riccardo Mattolini, Dip. Sistemi e Informatica
+                Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994 Universita' di Firenze
     Copyright   1993  University of Cambridge
 
@@ -10,11 +10,11 @@
 
 Equiv = Relation +
 consts
-    refl,equiv 	::      "['a set,('a*'a) set]=>bool"
+    refl,equiv  ::      "['a set,('a*'a) set]=>bool"
     sym         ::      "('a*'a) set=>bool"
     "'/"        ::      "['a set,('a*'a) set]=>'a set set"  (infixl 90) 
                         (*set of equiv classes*)
-    congruent	::	"[('a*'a) set,'a=>'b]=>bool"
+    congruent   ::      "[('a*'a) set,'a=>'b]=>bool"
     congruent2  ::      "[('a*'a) set,['a,'a]=>'b]=>bool"
 
 defs
diff -r 7f5a4cd08209 -r 608483c2122a src/HOL/Integ/Integ.thy
--- a/src/HOL/Integ/Integ.thy	Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/Integ/Integ.thy	Mon Feb 05 21:29:06 1996 +0100
@@ -1,7 +1,7 @@
-(*  Title: 	Integ.thy
+(*  Title:      Integ.thy
     ID:         $Id$
-    Authors: 	Riccardo Mattolini, Dip. Sistemi e Informatica
-        	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Authors:    Riccardo Mattolini, Dip. Sistemi e Informatica
+                Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994 Universita' di Firenze
     Copyright   1993  University of Cambridge
 
@@ -16,16 +16,16 @@
   intrel_def
    "intrel == {p. ? x1 y1 x2 y2. p=((x1::nat,y1),(x2,y2)) & x1+y2 = x2+y1}"
 
-subtype (Integ)
-  int = "{x::(nat*nat).True}/intrel"		(Equiv.quotient_def)
+typedef (Integ)
+  int = "{x::(nat*nat).True}/intrel"            (Equiv.quotient_def)
 
 instance
   int :: {ord, plus, times, minus}
 
 consts
   zNat        :: nat set
-  znat	      :: nat => int	   ("$# _" [80] 80)
-  zminus      :: int => int	   ("$~ _" [80] 80)
+  znat        :: nat => int        ("$# _" [80] 80)
+  zminus      :: int => int        ("$~ _" [80] 80)
   znegative   :: int => bool
   zmagnitude  :: int => int
   zdiv,zmod   :: [int,int]=>int  (infixl 70)
@@ -37,7 +37,7 @@
   znat_def    "$# m == Abs_Integ(intrel ^^ {(m,0)})"
 
   zminus_def
-	"$~ Z == Abs_Integ(UN p:Rep_Integ(Z). split (%x y. intrel^^{(y,x)}) p)"
+        "$~ Z == Abs_Integ(UN p:Rep_Integ(Z). split (%x y. intrel^^{(y,x)}) p)"
 
   znegative_def
       "znegative(Z) == EX x y. x<y & (x,y::nat):Rep_Integ(Z)"
diff -r 7f5a4cd08209 -r 608483c2122a src/HOL/Lambda/Commutation.thy
--- a/src/HOL/Lambda/Commutation.thy	Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/Lambda/Commutation.thy	Mon Feb 05 21:29:06 1996 +0100
@@ -1,6 +1,6 @@
-(*  Title: 	HOL/Lambda/Commutation.thy
+(*  Title:      HOL/Lambda/Commutation.thy
     ID:         $Id$
-    Author: 	Tobias Nipkow
+    Author:     Tobias Nipkow
     Copyright   1995  TU Muenchen
 
 Abstract commutation and confluence notions.
diff -r 7f5a4cd08209 -r 608483c2122a src/HOL/Lex/Auto.thy
--- a/src/HOL/Lex/Auto.thy	Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/Lex/Auto.thy	Mon Feb 05 21:29:06 1996 +0100
@@ -1,6 +1,6 @@
-(*  Title: 	HOL/Lex/Auto.thy
+(*  Title:      HOL/Lex/Auto.thy
     ID:         $Id$
-    Author: 	Tobias Nipkow
+    Author:     Tobias Nipkow
     Copyright   1995 TUM
 
 Automata expressed as triples of
diff -r 7f5a4cd08209 -r 608483c2122a src/HOL/Lex/AutoChopper.thy
--- a/src/HOL/Lex/AutoChopper.thy	Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/Lex/AutoChopper.thy	Mon Feb 05 21:29:06 1996 +0100
@@ -1,6 +1,6 @@
-(*  Title: 	HOL/Lex/AutoChopper.thy
+(*  Title:      HOL/Lex/AutoChopper.thy
     ID:         $Id$
-    Author: 	Tobias Nipkow
+    Author:     Tobias Nipkow
     Copyright   1995 TUM
 
 auto_chopper turns an automaton into a chopper. Tricky, because primrec.
@@ -20,19 +20,19 @@
   is_auto_chopper :: (('a,'b)auto => 'a chopper) => bool
   auto_chopper :: ('a,'b)auto => 'a chopper
   acc :: "['a list, 'b, 'a list, 'a list, 'a list list*'a list, ('a,'b)auto]
-	  => 'a list list * 'a list"
+          => 'a list list * 'a list"
 
 defs
   is_auto_chopper_def "is_auto_chopper(chopperf) ==
-		       !A. is_longest_prefix_chopper(accepts A)(chopperf A)"
+                       !A. is_longest_prefix_chopper(accepts A)(chopperf A)"
 
   auto_chopper_def "auto_chopper A xs == acc xs (start A) [] [] ([],xs) A"
 
 primrec acc List.list
   acc_Nil  "acc [] st ys zs chopsr A =
-	      (if ys=[] then chopsr else (ys#fst(chopsr),snd(chopsr)))" 
+              (if ys=[] then chopsr else (ys#fst(chopsr),snd(chopsr)))" 
   acc_Cons "acc(x#xs) st ys zs chopsr A =
-	    (let s0 = start(A); nxt = next(A); fin = fin(A)
+            (let s0 = start(A); nxt = next(A); fin = fin(A)
              in if fin(nxt st x)
                 then acc xs (nxt st x) (zs@[x]) (zs@[x])
                          (acc xs s0 [] [] ([],xs) A) A
diff -r 7f5a4cd08209 -r 608483c2122a src/HOL/Lex/Chopper.thy
--- a/src/HOL/Lex/Chopper.thy	Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/Lex/Chopper.thy	Mon Feb 05 21:29:06 1996 +0100
@@ -1,6 +1,6 @@
-(*  Title: 	HOL/Lex/Chopper.thy
+(*  Title:      HOL/Lex/Chopper.thy
     ID:         $Id$
-    Author: 	Tobias Nipkow
+    Author:     Tobias Nipkow
     Copyright   1995 TUM
 
 A 'chopper' is a function which returns
@@ -25,10 +25,10 @@
 defs
   is_longest_prefix_chopper_def
     "is_longest_prefix_chopper L chopper == !xs.   \
-\	 (!zs. chopper(xs) = ([],zs) --> \
-\	       zs=xs & (!ys. ys ~= [] & ys <= xs --> ~L(ys))) &  \
-\ 	 (!ys yss zs. chopper(xs) = (ys#yss,zs) -->                \
-\	    ys ~= [] & L(ys) & xs=ys@flat(yss)@zs &   \
+\        (!zs. chopper(xs) = ([],zs) --> \
+\              zs=xs & (!ys. ys ~= [] & ys <= xs --> ~L(ys))) &  \
+\        (!ys yss zs. chopper(xs) = (ys#yss,zs) -->                \
+\           ys ~= [] & L(ys) & xs=ys@flat(yss)@zs &   \
 \           chopper(flat(yss)@zs) = (yss,zs) &     \
 \           (!as. as <= xs & ys <= as & ys ~= as --> ~L(as)))"
 end
diff -r 7f5a4cd08209 -r 608483c2122a src/HOL/Lex/Prefix.thy
--- a/src/HOL/Lex/Prefix.thy	Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/Lex/Prefix.thy	Mon Feb 05 21:29:06 1996 +0100
@@ -1,6 +1,6 @@
-(*  Title: 	HOL/Lex/Prefix.thy
+(*  Title:      HOL/Lex/Prefix.thy
     ID:         $Id$
-    Author: 	Tobias Nipkow
+    Author:     Tobias Nipkow
     Copyright   1995 TUM
 *)
 
@@ -9,5 +9,5 @@
 arities list :: (term)ord
 
 defs
-	prefix_def     "xs <= zs  ==  ? ys. zs = xs@ys"
+        prefix_def     "xs <= zs  ==  ? ys. zs = xs@ys"
 end
diff -r 7f5a4cd08209 -r 608483c2122a src/HOL/MiniML/I.thy
--- a/src/HOL/MiniML/I.thy	Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/MiniML/I.thy	Mon Feb 05 21:29:06 1996 +0100
@@ -8,16 +8,16 @@
 I = W +
 
 consts
-	I :: [expr, typ list, nat, subst] => result_W
+        I :: [expr, typ list, nat, subst] => result_W
 
 primrec I expr
-        I_Var	"I (Var i) a n s = (if i < length a then Ok(s, nth i a, n)
+        I_Var   "I (Var i) a n s = (if i < length a then Ok(s, nth i a, n)
                                     else Fail)"
-        I_Abs	"I (Abs e) a n s = ( (s,t,m) := I e ((TVar n)#a) (Suc n) s;
+        I_Abs   "I (Abs e) a n s = ( (s,t,m) := I e ((TVar n)#a) (Suc n) s;
                                      Ok(s, TVar n -> t, m) )"
-        I_App	"I (App e1 e2) a n s =
- 		   ( (s1,t1,m1) := I e1 a n s;
-		     (s2,t2,m2) := I e2 a m1 s1;
-		     u := mgu ($s2 t1) ($s2 t2 -> TVar m2);
-		     Ok($u o s2, TVar m2, Suc m2) )"
+        I_App   "I (App e1 e2) a n s =
+                   ( (s1,t1,m1) := I e1 a n s;
+                     (s2,t2,m2) := I e2 a m1 s1;
+                     u := mgu ($s2 t1) ($s2 t2 -> TVar m2);
+                     Ok($u o s2, TVar m2, Suc m2) )"
 end
diff -r 7f5a4cd08209 -r 608483c2122a src/HOL/MiniML/MiniML.thy
--- a/src/HOL/MiniML/MiniML.thy	Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/MiniML/MiniML.thy	Mon Feb 05 21:29:06 1996 +0100
@@ -10,11 +10,11 @@
 
 (* expressions *)
 datatype
-	expr = Var nat | Abs expr | App expr expr
+        expr = Var nat | Abs expr | App expr expr
 
 (* type inference rules *)
 consts
-	has_type :: "(typ list * expr * typ)set"
+        has_type :: "(typ list * expr * typ)set"
 syntax
         "@has_type" :: [typ list, expr, typ] => bool
                        ("((_) |-/ (_) :: (_))" 60)
@@ -23,10 +23,10 @@
 
 inductive "has_type"
 intrs
-	VarI "[| n < length a |] ==> a |- Var n :: nth n a"
-	AbsI "[| t1#a |- e :: t2 |] ==> a |- Abs e :: t1 -> t2"
-	AppI "[| a |- e1 :: t2 -> t1; a |- e2 :: t2 |] 
-     	      ==> a |- App e1 e2 :: t1"
+        VarI "[| n < length a |] ==> a |- Var n :: nth n a"
+        AbsI "[| t1#a |- e :: t2 |] ==> a |- Abs e :: t1 -> t2"
+        AppI "[| a |- e1 :: t2 -> t1; a |- e2 :: t2 |] 
+              ==> a |- App e1 e2 :: t1"
 
 end
 
diff -r 7f5a4cd08209 -r 608483c2122a src/HOL/MiniML/Type.thy
--- a/src/HOL/MiniML/Type.thy	Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/MiniML/Type.thy	Mon Feb 05 21:29:06 1996 +0100
@@ -10,81 +10,81 @@
 
 (* new class for structures containing type variables *)
 classes
-	type_struct < term 
+        type_struct < term 
 
 (* type expressions *)
 datatype
-	typ = TVar nat | "->" typ typ (infixr 70)
+        typ = TVar nat | "->" typ typ (infixr 70)
 
 (* type variable substitution *)
 types
-	subst = nat => typ
+        subst = nat => typ
 
 arities
-	typ::type_struct
-	list::(type_struct)type_struct
-	fun::(term,type_struct)type_struct
+        typ::type_struct
+        list::(type_struct)type_struct
+        fun::(term,type_struct)type_struct
 
 (* substitutions *)
 
 (* identity *)
 consts
-	id_subst :: subst
+        id_subst :: subst
 defs
-	id_subst_def "id_subst == (%n.TVar n)"
+        id_subst_def "id_subst == (%n.TVar n)"
 
 (* extension of substitution to type structures *)
 consts
-	app_subst :: [subst, 'a::type_struct] => 'a::type_struct ("$")
+        app_subst :: [subst, 'a::type_struct] => 'a::type_struct ("$")
 
 rules
-	app_subst_TVar  "$ s (TVar n) = s n" 
-	app_subst_Fun	"$ s (t1 -> t2) = ($ s t1) -> ($ s t2)" 
+        app_subst_TVar  "$ s (TVar n) = s n" 
+        app_subst_Fun   "$ s (t1 -> t2) = ($ s t1) -> ($ s t2)" 
 defs
-        app_subst_list	"$ s == map ($ s)"
+        app_subst_list  "$ s == map ($ s)"
   
 (* free_tv s: the type variables occuring freely in the type structure s *)
 consts
-	free_tv :: ['a::type_struct] => nat set
+        free_tv :: ['a::type_struct] => nat set
 
 rules
-	free_tv_TVar	"free_tv (TVar m) = {m}"
-	free_tv_Fun	"free_tv (t1 -> t2) = (free_tv t1) Un (free_tv t2)"
-	free_tv_Nil	"free_tv [] = {}"
-	free_tv_Cons	"free_tv (x#l) = (free_tv x) Un (free_tv l)"
+        free_tv_TVar    "free_tv (TVar m) = {m}"
+        free_tv_Fun     "free_tv (t1 -> t2) = (free_tv t1) Un (free_tv t2)"
+        free_tv_Nil     "free_tv [] = {}"
+        free_tv_Cons    "free_tv (x#l) = (free_tv x) Un (free_tv l)"
 
 (* domain of a substitution *)
 consts
-	dom :: subst => nat set
+        dom :: subst => nat set
 defs
-	dom_def 	"dom s == {n. s n ~= TVar n}" 
+        dom_def         "dom s == {n. s n ~= TVar n}" 
 
 (* codomain of a substitutions: the introduced variables *)
 consts
      cod :: subst => nat set
 defs
-	cod_def		"cod s == (UN m:dom s. free_tv (s m))"
+        cod_def         "cod s == (UN m:dom s. free_tv (s m))"
 
 defs
-	free_tv_subst	"free_tv s == (dom s) Un (cod s)"
+        free_tv_subst   "free_tv s == (dom s) Un (cod s)"
 
 (* new_tv s n computes whether n is a new type variable w.r.t. a type 
    structure s, i.e. whether n is greater than any type variable 
    occuring in the type structure *)
 consts
-	new_tv :: [nat,'a::type_struct] => bool
+        new_tv :: [nat,'a::type_struct] => bool
 defs
         new_tv_def      "new_tv n ts == ! m. m:free_tv ts --> m<n"
 
 (* unification algorithm mgu *)
 consts
-	mgu :: [typ,typ] => subst maybe
+        mgu :: [typ,typ] => subst maybe
 rules
-	mgu_eq 	 "mgu t1 t2 = Ok u ==> $u t1 = $u t2"
-	mgu_mg 	 "[| (mgu t1 t2) = Ok u; $s t1 = $s t2 |] ==>
-		  ? r. s = $r o u"
-	mgu_Ok	 "$s t1 = $s t2 ==> ? u. mgu t1 t2 = Ok u"
-	mgu_free "mgu t1 t2 = Ok u ==> free_tv u <= free_tv t1 Un free_tv t2"
+        mgu_eq   "mgu t1 t2 = Ok u ==> $u t1 = $u t2"
+        mgu_mg   "[| (mgu t1 t2) = Ok u; $s t1 = $s t2 |] ==>
+                  ? r. s = $r o u"
+        mgu_Ok   "$s t1 = $s t2 ==> ? u. mgu t1 t2 = Ok u"
+        mgu_free "mgu t1 t2 = Ok u ==> free_tv u <= free_tv t1 Un free_tv t2"
 
 end
 
diff -r 7f5a4cd08209 -r 608483c2122a src/HOL/MiniML/W.thy
--- a/src/HOL/MiniML/W.thy	Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/MiniML/W.thy	Mon Feb 05 21:29:06 1996 +0100
@@ -13,16 +13,16 @@
 
 (* type inference algorithm W *)
 consts
-	W :: [expr, typ list, nat] => result_W
+        W :: [expr, typ list, nat] => result_W
 
 primrec W expr
-  W_Var	"W (Var i) a n = (if i < length a then Ok(id_subst, nth i a, n)
-		          else Fail)"
-  W_Abs	"W (Abs e) a n = ( (s,t,m) := W e ((TVar n)#a) (Suc n);
-		           Ok(s, (s n) -> t, m) )"
-  W_App	"W (App e1 e2) a n =
- 		 ( (s1,t1,m1) := W e1 a n;
-		   (s2,t2,m2) := W e2 ($s1 a) m1;
-		   u := mgu ($s2 t1) (t2 -> (TVar m2));
-		   Ok( $u o $s2 o s1, $u (TVar m2), Suc m2) )"
+  W_Var "W (Var i) a n = (if i < length a then Ok(id_subst, nth i a, n)
+                          else Fail)"
+  W_Abs "W (Abs e) a n = ( (s,t,m) := W e ((TVar n)#a) (Suc n);
+                           Ok(s, (s n) -> t, m) )"
+  W_App "W (App e1 e2) a n =
+                 ( (s1,t1,m1) := W e1 a n;
+                   (s2,t2,m2) := W e2 ($s1 a) m1;
+                   u := mgu ($s2 t1) (t2 -> (TVar m2));
+                   Ok( $u o $s2 o s1, $u (TVar m2), Suc m2) )"
 end
diff -r 7f5a4cd08209 -r 608483c2122a src/HOL/Subst/AList.thy
--- a/src/HOL/Subst/AList.thy	Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/Subst/AList.thy	Mon Feb 05 21:29:06 1996 +0100
@@ -1,5 +1,5 @@
-(*  Title: 	Substitutions/alist.thy
-    Author: 	Martin Coen, Cambridge University Computer Laboratory
+(*  Title:      Substitutions/alist.thy
+    Author:     Martin Coen, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
 Association lists.
diff -r 7f5a4cd08209 -r 608483c2122a src/HOL/Subst/Setplus.thy
--- a/src/HOL/Subst/Setplus.thy	Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/Subst/Setplus.thy	Mon Feb 05 21:29:06 1996 +0100
@@ -1,5 +1,5 @@
-(*  Title: 	Substitutions/setplus.thy
-    Author: 	Martin Coen, Cambridge University Computer Laboratory
+(*  Title:      Substitutions/setplus.thy
+    Author:     Martin Coen, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
 Minor additions to HOL's set theory
diff -r 7f5a4cd08209 -r 608483c2122a src/HOL/Subst/Subst.thy
--- a/src/HOL/Subst/Subst.thy	Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/Subst/Subst.thy	Mon Feb 05 21:29:06 1996 +0100
@@ -1,5 +1,5 @@
-(*  Title: 	Substitutions/subst.thy
-    Author: 	Martin Coen, Cambridge University Computer Laboratory
+(*  Title:      Substitutions/subst.thy
+    Author:     Martin Coen, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
 Substitutions on uterms
@@ -22,8 +22,8 @@
   subst_eq_def  "r =s= s == ALL t.t <| r = t <| s"
 
   subst_def    
-  "t <| al == uterm_rec t (%x.assoc x (Var x) al)	
-                         (%x.Const(x))			
+  "t <| al == uterm_rec t (%x.assoc x (Var x) al)       
+                         (%x.Const(x))                  
                          (%u v q r.Comb q r)"
 
   comp_def    "al <> bl == alist_rec al bl (%x y xs g.(x,y <| bl)#g)"
diff -r 7f5a4cd08209 -r 608483c2122a src/HOL/Subst/UTLemmas.thy
--- a/src/HOL/Subst/UTLemmas.thy	Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/Subst/UTLemmas.thy	Mon Feb 05 21:29:06 1996 +0100
@@ -1,5 +1,5 @@
-(*  Title: 	Substitutions/utermlemmas.thy
-    Author: 	Martin Coen, Cambridge University Computer Laboratory
+(*  Title:      Substitutions/utermlemmas.thy
+    Author:     Martin Coen, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
 Additional definitions for uterms that are not part of the basic inductive definition.
diff -r 7f5a4cd08209 -r 608483c2122a src/HOL/Subst/UTerm.ML
--- a/src/HOL/Subst/UTerm.ML	Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/Subst/UTerm.ML	Mon Feb 05 21:29:06 1996 +0100
@@ -206,8 +206,18 @@
 
 (*** UTerm_rec -- by wf recursion on pred_sexp ***)
 
-val UTerm_rec_unfold =
-    [UTerm_rec_def, wf_pred_sexp RS wf_trancl] MRS def_wfrec;
+goal UTerm.thy
+   "(%M. UTerm_rec M b c d) = wfrec (trancl pred_sexp) \
+   \ (%g. Case (%x.b(x)) (Case (%y. c(y)) (Split (%x y. d x y (g x) (g y)))))";
+by (simp_tac (HOL_ss addsimps [UTerm_rec_def]) 1);
+bind_thm("UTerm_rec_unfold", (wf_pred_sexp RS wf_trancl) RS 
+                            ((result() RS eq_reflection) RS def_wfrec));
+
+(*---------------------------------------------------------------------------
+ * Old:
+ * val UTerm_rec_unfold =
+ *   [UTerm_rec_def, wf_pred_sexp RS wf_trancl] MRS def_wfrec;
+ *---------------------------------------------------------------------------*)
 
 (** conversion rules **)
 
diff -r 7f5a4cd08209 -r 608483c2122a src/HOL/Subst/UTerm.thy
--- a/src/HOL/Subst/UTerm.thy	Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/Subst/UTerm.thy	Mon Feb 05 21:29:06 1996 +0100
@@ -1,8 +1,8 @@
-(*  Title: 	Substitutions/UTerm.thy
-    Author: 	Martin Coen, Cambridge University Computer Laboratory
+(*  Title:      Substitutions/UTerm.thy
+    Author:     Martin Coen, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
-Simple term structure for unifiation.
+Simple term structure for unification.
 Binary trees with leaves that are constants or variables.
 *)
 
@@ -30,32 +30,32 @@
 
 defs
      (*defining the concrete constructors*)
-  VAR_def  	"VAR(v) == In0(v)"
-  CONST_def  	"CONST(v) == In1(In0(v))"
-  COMB_def 	"COMB t u == In1(In1(t $ u))"
+  VAR_def       "VAR(v) == In0(v)"
+  CONST_def     "CONST(v) == In1(In0(v))"
+  COMB_def      "COMB t u == In1(In1(t $ u))"
 
 inductive "uterm(A)"
   intrs
-    VAR_I	   "v:A ==> VAR(v) : uterm(A)"
+    VAR_I          "v:A ==> VAR(v) : uterm(A)"
     CONST_I  "c:A ==> CONST(c) : uterm(A)"
     COMB_I   "[| M:uterm(A);  N:uterm(A) |] ==> COMB M N : uterm(A)"
 
 rules
     (*faking a type definition...*)
-  Rep_uterm 		"Rep_uterm(xs): uterm(range(Leaf))"
-  Rep_uterm_inverse 	"Abs_uterm(Rep_uterm(xs)) = xs"
-  Abs_uterm_inverse 	"M: uterm(range(Leaf)) ==> Rep_uterm(Abs_uterm(M)) = M"
+  Rep_uterm             "Rep_uterm(xs): uterm(range(Leaf))"
+  Rep_uterm_inverse     "Abs_uterm(Rep_uterm(xs)) = xs"
+  Abs_uterm_inverse     "M: uterm(range(Leaf)) ==> Rep_uterm(Abs_uterm(M)) = M"
 
 defs
      (*defining the abstract constructors*)
-  Var_def  	"Var(v) == Abs_uterm(VAR(Leaf(v)))"
-  Const_def  	"Const(c) == Abs_uterm(CONST(Leaf(c)))"
-  Comb_def 	"Comb t u == Abs_uterm (COMB (Rep_uterm t) (Rep_uterm u))"
+  Var_def       "Var(v) == Abs_uterm(VAR(Leaf(v)))"
+  Const_def     "Const(c) == Abs_uterm(CONST(Leaf(c)))"
+  Comb_def      "Comb t u == Abs_uterm (COMB (Rep_uterm t) (Rep_uterm u))"
 
      (*uterm recursion*)
-  UTerm_rec_def	
-   "UTerm_rec M b c d == wfrec (trancl pred_sexp) M 
-          (Case (%x g.b(x)) (Case (%y g. c(y)) (Split (%x y g. d x y (g x) (g y)))))"
+  UTerm_rec_def 
+   "UTerm_rec M b c d == wfrec (trancl pred_sexp) 
+    (%g. Case (%x.b(x)) (Case (%y. c(y)) (Split (%x y. d x y (g x) (g y))))) M"
 
   uterm_rec_def
    "uterm_rec t b c d == 
diff -r 7f5a4cd08209 -r 608483c2122a src/HOL/Subst/Unifier.thy
--- a/src/HOL/Subst/Unifier.thy	Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/Subst/Unifier.thy	Mon Feb 05 21:29:06 1996 +0100
@@ -1,5 +1,5 @@
-(*  Title: 	Subst/unifier.thy
-    Author: 	Martin Coen, Cambridge University Computer Laboratory
+(*  Title:      Subst/unifier.thy
+    Author:     Martin Coen, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
 Definition of most general idempotent unifier
@@ -22,7 +22,7 @@
   Unifier_def      "Unifier s t u == t <| s = u <| s"
   MoreGeneral_def  "r >> s == ? q.s =s= r <> q"
   MGUnifier_def    "MGUnifier s t u == Unifier s t u & 
-		    (! r.Unifier r t u --> s >> r)"
+                    (! r.Unifier r t u --> s >> r)"
   MGIUnifier_def   "MGIUnifier s t u == MGUnifier s t u & Idem(s)"
 
   UWFD_def
diff -r 7f5a4cd08209 -r 608483c2122a src/HOL/ex/Acc.thy
--- a/src/HOL/ex/Acc.thy	Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/ex/Acc.thy	Mon Feb 05 21:29:06 1996 +0100
@@ -1,6 +1,6 @@
-(*  Title: 	HOL/ex/Acc.thy
+(*  Title:      HOL/ex/Acc.thy
     ID:         $Id$
-    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
 
 Inductive definition of acc(r)
@@ -12,8 +12,8 @@
 Acc = WF + 
 
 consts
-  pred :: "['b, ('a * 'b)set] => 'a set"	(*Set of predecessors*)
-  acc  :: "('a * 'a)set => 'a set"		(*Accessible part*)
+  pred :: "['b, ('a * 'b)set] => 'a set"        (*Set of predecessors*)
+  acc  :: "('a * 'a)set => 'a set"              (*Accessible part*)
 
 defs
   pred_def  "pred x r == {y. (y,x):r}"
diff -r 7f5a4cd08209 -r 608483c2122a src/HOL/ex/BT.thy
--- a/src/HOL/ex/BT.thy	Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/ex/BT.thy	Mon Feb 05 21:29:06 1996 +0100
@@ -1,6 +1,6 @@
-(*  Title: 	HOL/ex/BT.thy
+(*  Title:      HOL/ex/BT.thy
     ID:         $Id$
-    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1995  University of Cambridge
 
 Binary trees (based on the ZF version)
@@ -11,9 +11,9 @@
 datatype 'a bt = Lf  |  Br 'a ('a bt) ('a bt)
   
 consts
-    n_nodes	:: 'a bt => nat
-    n_leaves   	:: 'a bt => nat
-    reflect 	:: 'a bt => 'a bt
+    n_nodes     :: 'a bt => nat
+    n_leaves    :: 'a bt => nat
+    reflect     :: 'a bt => 'a bt
     bt_map      :: ('a=>'b) => ('a bt => 'b bt)
     preorder    :: 'a bt => 'a list
     inorder     :: 'a bt => 'a list
diff -r 7f5a4cd08209 -r 608483c2122a src/HOL/ex/InSort.thy
--- a/src/HOL/ex/InSort.thy	Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/ex/InSort.thy	Mon Feb 05 21:29:06 1996 +0100
@@ -1,6 +1,6 @@
-(*  Title: 	HOL/ex/insort.thy
+(*  Title:      HOL/ex/insort.thy
     ID:         $Id$
-    Author: 	Tobias Nipkow
+    Author:     Tobias Nipkow
     Copyright   1994 TU Muenchen
 
 Insertion sort
diff -r 7f5a4cd08209 -r 608483c2122a src/HOL/ex/LList.thy
--- a/src/HOL/ex/LList.thy	Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/ex/LList.thy	Mon Feb 05 21:29:06 1996 +0100
@@ -1,6 +1,6 @@
-(*  Title: 	HOL/LList.thy
+(*  Title:      HOL/LList.thy
     ID:         $Id$
-    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
 
 Definition of type 'a llist by a greatest fixed point
@@ -18,8 +18,8 @@
 
 Previous definition of llistD_Fun was explicit:
   llistD_Fun_def
-   "llistD_Fun(r) == 	
-       {(LNil,LNil)}  Un  	
+   "llistD_Fun(r) ==    
+       {(LNil,LNil)}  Un        
        (UN x. (split(%l1 l2.(LCons(x,l1),LCons(x,l2))))``r)"
 *)
 
@@ -52,8 +52,8 @@
   LList_corec     :: "['a, 'a => unit + ('b item * 'a)] => 'b item"
   llist_corec     :: "['a, 'a => unit + ('b * 'a)] => 'b llist"
 
-  Lmap	     :: ('a item => 'b item) => ('a item => 'b item)
-  lmap	     :: ('a=>'b) => ('a llist => 'b llist)
+  Lmap       :: ('a item => 'b item) => ('a item => 'b item)
+  lmap       :: ('a=>'b) => ('a llist => 'b llist)
 
   iterates   :: ['a => 'a, 'a] => 'a llist
 
@@ -71,21 +71,21 @@
   intrs
     NIL_I  "(NIL, NIL) : LListD(r)"
     CONS_I "[| (a,b): r;  (M,N) : LListD(r)   
-	    |] ==> (CONS a M, CONS b N) : LListD(r)"
+            |] ==> (CONS a M, CONS b N) : LListD(r)"
 
 defs
   (*Now used exclusively for abbreviating the coinduction rule*)
   list_Fun_def   "list_Fun A X ==   
-		  {z. z = NIL | (? M a. z = CONS a M & a : A & M : X)}"
+                  {z. z = NIL | (? M a. z = CONS a M & a : A & M : X)}"
 
   LListD_Fun_def "LListD_Fun r X ==   
-		  {z. z = (NIL, NIL) |   
-		      (? M N a b. z = (CONS a M, CONS b N) &   
-		                  (a, b) : r & (M, N) : X)}"
+                  {z. z = (NIL, NIL) |   
+                      (? M N a b. z = (CONS a M, CONS b N) &   
+                                  (a, b) : r & (M, N) : X)}"
 
   (*defining the abstract constructors*)
-  LNil_def  	"LNil == Abs_llist(NIL)"
-  LCons_def 	"LCons x xs == Abs_llist(CONS (Leaf x) (Rep_llist xs))"
+  LNil_def      "LNil == Abs_llist(NIL)"
+  LCons_def     "LCons x xs == Abs_llist(CONS (Leaf x) (Rep_llist xs))"
 
   llist_case_def
    "llist_case c d l == 
@@ -93,8 +93,8 @@
 
   LList_corec_fun_def
     "LList_corec_fun k f == 
-     nat_rec k (%x. {}) 			
-	      (%j r x. sum_case (%u.NIL) (split(%z w. CONS z (r w))) (f x))"
+     nat_rec k (%x. {})                         
+              (%j r x. sum_case (%u.NIL) (split(%z w. CONS z (r w))) (f x))"
 
   LList_corec_def
     "LList_corec a f == UN k. LList_corec_fun k f a"
@@ -105,12 +105,12 @@
                                     (split(%v w. Inr((Leaf(v), w)))) (f z)))"
 
   llistD_Fun_def
-   "llistD_Fun(r) == 	
-	prod_fun Abs_llist Abs_llist ``  	
-                LListD_Fun (diag(range Leaf))	
-		            (prod_fun Rep_llist Rep_llist `` r)"
+   "llistD_Fun(r) ==    
+        prod_fun Abs_llist Abs_llist ``         
+                LListD_Fun (diag(range Leaf))   
+                            (prod_fun Rep_llist Rep_llist `` r)"
 
-  Lconst_def	"Lconst(M) == lfp(%N. CONS M N)"     
+  Lconst_def    "Lconst(M) == lfp(%N. CONS M N)"     
 
   Lmap_def
    "Lmap f M == LList_corec M (List_case (Inl ()) (%x M'. Inr((f(x), M'))))"
@@ -118,7 +118,7 @@
   lmap_def
    "lmap f l == llist_corec l (llist_case (Inl ()) (%y z. Inr((f(y), z))))"
 
-  iterates_def	"iterates f a == llist_corec a (%x. Inr((x, f(x))))"     
+  iterates_def  "iterates f a == llist_corec a (%x. Inr((x, f(x))))"     
 
 (*Append generates its result by applying f, where
     f((NIL,NIL)) = Inl(())
@@ -127,18 +127,18 @@
 *)
 
   Lappend_def
-   "Lappend M N == LList_corec (M,N)	   				     
+   "Lappend M N == LList_corec (M,N)                                         
      (split(List_case (List_case (Inl ()) (%N1 N2. Inr((N1, (NIL,N2))))) 
                       (%M1 M2 N. Inr((M1, (M2,N))))))"
 
   lappend_def
-   "lappend l n == llist_corec (l,n)	   				     
+   "lappend l n == llist_corec (l,n)                                         
    (split(llist_case (llist_case (Inl ()) (%n1 n2. Inr((n1, (LNil,n2))))) 
                      (%l1 l2 n. Inr((l1, (l2,n))))))"
 
 rules
     (*faking a type definition...*)
-  Rep_llist 	    "Rep_llist(xs): llist(range(Leaf))"
+  Rep_llist         "Rep_llist(xs): llist(range(Leaf))"
   Rep_llist_inverse "Abs_llist(Rep_llist(xs)) = xs"
   Abs_llist_inverse "M: llist(range(Leaf)) ==> Rep_llist(Abs_llist(M)) = M"
 
diff -r 7f5a4cd08209 -r 608483c2122a src/HOL/ex/LexProd.thy
--- a/src/HOL/ex/LexProd.thy	Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/ex/LexProd.thy	Mon Feb 05 21:29:06 1996 +0100
@@ -1,6 +1,6 @@
-(*  Title: 	HOL/ex/lex-prod.thy
+(*  Title:      HOL/ex/lex-prod.thy
     ID:         $Id$
-    Author: 	Tobias Nipkow, TU Munich
+    Author:     Tobias Nipkow, TU Munich
     Copyright   1993  TU Munich
 
 The lexicographic product of two relations.
@@ -10,6 +10,6 @@
 consts "**" :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set" (infixl 70)
 rules
 lex_prod_def "ra**rb == {p. ? a a' b b'. 
-	p = ((a,b),(a',b')) & ((a,a') : ra | a=a' & (b,b') : rb)}"
+        p = ((a,b),(a',b')) & ((a,a') : ra | a=a' & (b,b') : rb)}"
 end
 
diff -r 7f5a4cd08209 -r 608483c2122a src/HOL/ex/MT.thy
--- a/src/HOL/ex/MT.thy	Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/ex/MT.thy	Mon Feb 05 21:29:06 1996 +0100
@@ -1,6 +1,6 @@
-(*  Title: 	HOL/ex/mt.thy
+(*  Title:      HOL/ex/mt.thy
     ID:         $Id$
-    Author: 	Jacob Frost, Cambridge University Computer Laboratory
+    Author:     Jacob Frost, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
 Based upon the article
diff -r 7f5a4cd08209 -r 608483c2122a src/HOL/ex/NatSum.thy
--- a/src/HOL/ex/NatSum.thy	Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/ex/NatSum.thy	Mon Feb 05 21:29:06 1996 +0100
@@ -1,6 +1,6 @@
-(*  Title: 	HOL/ex/natsum.thy
+(*  Title:      HOL/ex/natsum.thy
     ID:         $Id$
-    Author: 	Tobias Nipkow
+    Author:     Tobias Nipkow
     Copyright   1994 TU Muenchen
 
 A summation operator. sum(f,n+1) is the sum of all f(i), i=0...n.
diff -r 7f5a4cd08209 -r 608483c2122a src/HOL/ex/Perm.thy
--- a/src/HOL/ex/Perm.thy	Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/ex/Perm.thy	Mon Feb 05 21:29:06 1996 +0100
@@ -1,6 +1,6 @@
-(*  Title: 	HOL/ex/Perm.thy
+(*  Title:      HOL/ex/Perm.thy
     ID:         $Id$
-    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1995  University of Cambridge
 
 Permutations: example of an inductive definition
diff -r 7f5a4cd08209 -r 608483c2122a src/HOL/ex/PropLog.thy
--- a/src/HOL/ex/PropLog.thy	Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/ex/PropLog.thy	Mon Feb 05 21:29:06 1996 +0100
@@ -1,6 +1,6 @@
-(*  Title: 	HOL/ex/PropLog.thy
+(*  Title:      HOL/ex/PropLog.thy
     ID:         $Id$
-    Author: 	Tobias Nipkow
+    Author:     Tobias Nipkow
     Copyright   1994  TU Muenchen
 
 Inductive definition of propositional logic.
@@ -11,11 +11,11 @@
     'a pl = false | var 'a ("#_" [1000]) | "->" ('a pl) ('a pl) (infixr 90)
 consts
   thms :: 'a pl set => 'a pl set
-  "|-" 	:: ['a pl set, 'a pl] => bool	(infixl 50)
-  "|="	:: ['a pl set, 'a pl] => bool	(infixl 50)
-  eval2	:: ['a pl, 'a set] => bool
-  eval	:: ['a set, 'a pl] => bool	("_[_]" [100,0] 100)
-  hyps	:: ['a pl, 'a set] => 'a pl set
+  "|-"  :: ['a pl set, 'a pl] => bool   (infixl 50)
+  "|="  :: ['a pl set, 'a pl] => bool   (infixl 50)
+  eval2 :: ['a pl, 'a set] => bool
+  eval  :: ['a set, 'a pl] => bool      ("_[_]" [100,0] 100)
+  hyps  :: ['a pl, 'a set] => 'a pl set
 
 translations
   "H |- p" == "p : thms(H)"
diff -r 7f5a4cd08209 -r 608483c2122a src/HOL/ex/Puzzle.thy
--- a/src/HOL/ex/Puzzle.thy	Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/ex/Puzzle.thy	Mon Feb 05 21:29:06 1996 +0100
@@ -1,6 +1,6 @@
-(*  Title: 	HOL/ex/puzzle.thy
+(*  Title:      HOL/ex/puzzle.thy
     ID:         $Id$
-    Author: 	Tobias Nipkow
+    Author:     Tobias Nipkow
     Copyright   1993 TU Muenchen
 
 An question from "Bundeswettbewerb Mathematik"
diff -r 7f5a4cd08209 -r 608483c2122a src/HOL/ex/Qsort.thy
--- a/src/HOL/ex/Qsort.thy	Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/ex/Qsort.thy	Mon Feb 05 21:29:06 1996 +0100
@@ -1,6 +1,6 @@
-(*  Title: 	HOL/ex/qsort.thy
+(*  Title:      HOL/ex/qsort.thy
     ID:         $Id$
-    Author: 	Tobias Nipkow
+    Author:     Tobias Nipkow
     Copyright   1994 TU Muenchen
 
 Quicksort
diff -r 7f5a4cd08209 -r 608483c2122a src/HOL/ex/Rec.thy
--- a/src/HOL/ex/Rec.thy	Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/ex/Rec.thy	Mon Feb 05 21:29:06 1996 +0100
@@ -1,8 +1,8 @@
 Rec = Fixedpt +
 consts
-fix	:: ('a=>'a) => 'a
-Dom	:: (('a=>'b) => ('a=>'b)) => 'a set
-Domf	:: (('a=>'b) => ('a=>'b)) => 'a set => 'a set
+fix     :: ('a=>'a) => 'a
+Dom     :: (('a=>'b) => ('a=>'b)) => 'a set
+Domf    :: (('a=>'b) => ('a=>'b)) => 'a set => 'a set
 rules
 Domf_def "Domf(F,D) == {y . !f g. (!x:D. f(x)=g(x)) --> F(f,y)=F(g,y)}"
 Dom_def  "Dom(F) == lfp(Domf(F))"
diff -r 7f5a4cd08209 -r 608483c2122a src/HOL/ex/SList.ML
--- a/src/HOL/ex/SList.ML	Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/ex/SList.ML	Mon Feb 05 21:29:06 1996 +0100
@@ -148,8 +148,18 @@
 (* The trancl(pred_sexp) is essential because pred_sexp_CONS_I1,2 would not
    hold if pred_sexp^+ were changed to pred_sexp. *)
 
-val List_rec_unfold = [List_rec_def, wf_pred_sexp RS wf_trancl] MRS def_wfrec
-                      |> standard;
+goal SList.thy
+   "(%M. List_rec M c d) = wfrec (trancl pred_sexp) \
+                           \     (%g. List_case c (%x y. d x y (g y)))";
+by (simp_tac (HOL_ss addsimps [List_rec_def]) 1);
+val List_rec_unfold = standard 
+  ((wf_pred_sexp RS wf_trancl) RS ((result() RS eq_reflection) RS def_wfrec));
+
+(*---------------------------------------------------------------------------
+ * Old:
+ * val List_rec_unfold = [List_rec_def,wf_pred_sexp RS wf_trancl] MRS def_wfrec
+ *                     |> standard;
+ *---------------------------------------------------------------------------*)
 
 (** pred_sexp lemmas **)
 
diff -r 7f5a4cd08209 -r 608483c2122a src/HOL/ex/SList.thy
--- a/src/HOL/ex/SList.thy	Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/ex/SList.thy	Mon Feb 05 21:29:06 1996 +0100
@@ -27,7 +27,7 @@
   NIL       :: 'a item
   CONS      :: ['a item, 'a item] => 'a item
   Nil       :: 'a list
-  "#"       :: ['a, 'a list] => 'a list                   	(infixr 65)
+  "#"       :: ['a, 'a list] => 'a list                         (infixr 65)
   List_case :: ['b, ['a item, 'a item]=>'b, 'a item] => 'b
   List_rec  :: ['a item, 'b, ['a item, 'a item, 'b]=>'b] => 'b
   list_case :: ['b, ['a, 'a list]=>'b, 'a list] => 'b
@@ -37,10 +37,10 @@
   null      :: 'a list => bool
   hd        :: 'a list => 'a
   tl,ttl    :: 'a list => 'a list
-  mem		:: ['a, 'a list] => bool			(infixl 55)
+  mem           :: ['a, 'a list] => bool                        (infixl 55)
   list_all  :: ('a => bool) => ('a list => bool)
   map       :: ('a=>'b) => ('a list => 'b list)
-  "@"	    :: ['a list, 'a list] => 'a list			(infixr 65)
+  "@"       :: ['a list, 'a list] => 'a list                    (infixr 65)
   filter    :: ['a => bool, 'a list] => 'a list
 
   (* list Enumeration *)
@@ -49,8 +49,8 @@
   "@list"   :: args => 'a list                    ("[(_)]")
 
   (* Special syntax for list_all and filter *)
-  "@Alls"	:: [idt, 'a list, bool] => bool	("(2Alls _:_./ _)" 10)
-  "@filter"	:: [idt, 'a list, bool] => 'a list	("(1[_:_ ./ _])")
+  "@Alls"       :: [idt, 'a list, bool] => bool ("(2Alls _:_./ _)" 10)
+  "@filter"     :: [idt, 'a list, bool] => 'a list      ("(1[_:_ ./ _])")
 
 translations
   "[x, xs]"     == "x#[xs]"
@@ -59,8 +59,8 @@
 
   "case xs of Nil => a | y#ys => b" == "list_case a (%y ys.b) xs"
 
-  "[x:xs . P]"	== "filter (%x.P) xs"
-  "Alls x:xs.P"	== "list_all (%x.P) xs"
+  "[x:xs . P]"  == "filter (%x.P) xs"
+  "Alls x:xs.P" == "list_all (%x.P) xs"
 
 defs
   (* Defining the Concrete Constructors *)
@@ -89,8 +89,8 @@
   (* list Recursion -- the trancl is Essential; see list.ML *)
 
   List_rec_def
-   "List_rec M c d == wfrec (trancl pred_sexp) M 
-                           (List_case (%g.c) (%x y g. d x y (g y)))"
+   "List_rec M c d == wfrec (trancl pred_sexp)
+                            (%g. List_case c (%x y. d x y (g y))) M"
 
   list_rec_def
    "list_rec l c d == 
@@ -105,14 +105,14 @@
   hd_def        "hd(xs)              == list_rec xs (@x.True) (%x xs r.x)"
   tl_def        "tl(xs)              == list_rec xs (@xs.True) (%x xs r.xs)"
   (* a total version of tl: *)
-  ttl_def 	"ttl(xs)             == list_rec xs [] (%x xs r.xs)"
+  ttl_def       "ttl(xs)             == list_rec xs [] (%x xs r.xs)"
 
-  mem_def 	"x mem xs            == 
-		   list_rec xs False (%y ys r. if y=x then True else r)"
+  mem_def       "x mem xs            == 
+                   list_rec xs False (%y ys r. if y=x then True else r)"
   list_all_def  "list_all P xs       == list_rec xs True (%x l r. P(x) & r)"
   map_def       "map f xs            == list_rec xs [] (%x l r. f(x)#r)"
-  append_def 	"xs@ys               == list_rec xs ys (%x l r. x#r)"
-  filter_def 	"filter P xs         == 
+  append_def    "xs@ys               == list_rec xs ys (%x l r. x#r)"
+  filter_def    "filter P xs         == 
                   list_rec xs [] (%x xs r. if P(x) then x#r else r)"
 
   list_case_def  "list_case a f xs == list_rec xs a (%x xs r.f x xs)"
diff -r 7f5a4cd08209 -r 608483c2122a src/HOL/ex/Simult.ML
--- a/src/HOL/ex/Simult.ML	Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/ex/Simult.ML	Mon Feb 05 21:29:06 1996 +0100
@@ -227,8 +227,19 @@
 
 (*** TF_rec -- by wf recursion on pred_sexp ***)
 
-val TF_rec_unfold =
-    wf_pred_sexp RS wf_trancl RS (TF_rec_def RS def_wfrec);
+goal Simult.thy
+   "(%M. TF_rec M b c d) = wfrec (trancl pred_sexp) \
+                         \       (%g. Case (Split(%x y. b x y (g y))) \
+                         \           (List_case c (%x y. d x y (g x) (g y))))";
+by (simp_tac (HOL_ss addsimps [TF_rec_def]) 1);
+val TF_rec_unfold = (wf_pred_sexp RS wf_trancl) RS 
+                    ((result() RS eq_reflection) RS def_wfrec);
+
+(*---------------------------------------------------------------------------
+ * Old: 
+ * val TF_rec_unfold =
+ *   wf_pred_sexp RS wf_trancl RS (TF_rec_def RS def_wfrec);
+ *---------------------------------------------------------------------------*)
 
 (** conversion rules for TF_rec **)
 
diff -r 7f5a4cd08209 -r 608483c2122a src/HOL/ex/Simult.thy
--- a/src/HOL/ex/Simult.thy	Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/ex/Simult.thy	Mon Feb 05 21:29:06 1996 +0100
@@ -1,6 +1,6 @@
-(*  Title: 	HOL/ex/Simult
+(*  Title:      HOL/ex/Simult
     ID:         $Id$
-    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
 A simultaneous recursive type definition: trees & forests
@@ -40,35 +40,35 @@
 
 defs
      (*the concrete constants*)
-  TCONS_def 	"TCONS M N == In0(M $ N)"
-  FNIL_def	"FNIL      == In1(NIL)"
-  FCONS_def	"FCONS M N == In1(CONS M N)"
+  TCONS_def     "TCONS M N == In0(M $ N)"
+  FNIL_def      "FNIL      == In1(NIL)"
+  FCONS_def     "FCONS M N == In1(CONS M N)"
      (*the abstract constants*)
-  Tcons_def 	"Tcons a ts == Abs_Tree(TCONS (Leaf a) (Rep_Forest ts))"
-  Fnil_def  	"Fnil       == Abs_Forest(FNIL)"
-  Fcons_def 	"Fcons t ts == Abs_Forest(FCONS (Rep_Tree t) (Rep_Forest ts))"
+  Tcons_def     "Tcons a ts == Abs_Tree(TCONS (Leaf a) (Rep_Forest ts))"
+  Fnil_def      "Fnil       == Abs_Forest(FNIL)"
+  Fcons_def     "Fcons t ts == Abs_Forest(FCONS (Rep_Tree t) (Rep_Forest ts))"
 
-  TF_def	"TF(A) == lfp(%Z. A <*> Part Z In1 
+  TF_def        "TF(A) == lfp(%Z. A <*> Part Z In1 
                            <+> ({Numb(0)} <+> Part Z In0 <*> Part Z In1))"
 
 rules
   (*faking a type definition for tree...*)
-  Rep_Tree 	   "Rep_Tree(n): Part (TF(range Leaf)) In0"
+  Rep_Tree         "Rep_Tree(n): Part (TF(range Leaf)) In0"
   Rep_Tree_inverse "Abs_Tree(Rep_Tree(t)) = t"
   Abs_Tree_inverse "z: Part (TF(range Leaf)) In0 ==> Rep_Tree(Abs_Tree(z)) = z"
     (*faking a type definition for forest...*)
-  Rep_Forest 	     "Rep_Forest(n): Part (TF(range Leaf)) In1"
+  Rep_Forest         "Rep_Forest(n): Part (TF(range Leaf)) In1"
   Rep_Forest_inverse "Abs_Forest(Rep_Forest(ts)) = ts"
   Abs_Forest_inverse 
-	"z: Part (TF(range Leaf)) In1 ==> Rep_Forest(Abs_Forest(z)) = z"
+        "z: Part (TF(range Leaf)) In1 ==> Rep_Forest(Abs_Forest(z)) = z"
 
 
 defs
      (*recursion*)
-  TF_rec_def	
-   "TF_rec M b c d == wfrec (trancl pred_sexp) M   
-               (Case (Split(%x y g. b x y (g y))) 
-	              (List_case (%g.c) (%x y g. d x y (g x) (g y))))"
+  TF_rec_def    
+   "TF_rec M b c d == wfrec (trancl pred_sexp)
+               (%g. Case (Split(%x y. b x y (g y))) 
+                      (List_case c (%x y. d x y (g x) (g y)))) M"
 
   tree_rec_def
    "tree_rec t b c d == 
diff -r 7f5a4cd08209 -r 608483c2122a src/HOL/ex/Sorting.thy
--- a/src/HOL/ex/Sorting.thy	Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/ex/Sorting.thy	Mon Feb 05 21:29:06 1996 +0100
@@ -1,6 +1,6 @@
-(*  Title: 	HOL/ex/sorting.thy
+(*  Title:      HOL/ex/sorting.thy
     ID:         $Id$
-    Author: 	Tobias Nipkow
+    Author:     Tobias Nipkow
     Copyright   1994 TU Muenchen
 
 Specification of sorting
diff -r 7f5a4cd08209 -r 608483c2122a src/HOL/ex/Term.ML
--- a/src/HOL/ex/Term.ML	Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/ex/Term.ML	Mon Feb 05 21:29:06 1996 +0100
@@ -110,8 +110,18 @@
 
 (*** Term_rec -- by wf recursion on pred_sexp ***)
 
-val Term_rec_unfold =
-    wf_pred_sexp RS wf_trancl RS (Term_rec_def RS def_wfrec);
+goal Term.thy
+   "(%M. Term_rec M d) = wfrec (trancl pred_sexp) \
+                             \ (%g. Split(%x y. d x y (Abs_map g y)))";
+by (simp_tac (HOL_ss addsimps [Term_rec_def]) 1);
+bind_thm("Term_rec_unfold", (wf_pred_sexp RS wf_trancl) RS 
+                            ((result() RS eq_reflection) RS def_wfrec));
+
+(*---------------------------------------------------------------------------
+ * Old:
+ * val Term_rec_unfold =
+ *     wf_pred_sexp RS wf_trancl RS (Term_rec_def RS def_wfrec);
+ *---------------------------------------------------------------------------*)
 
 (** conversion rules **)
 
diff -r 7f5a4cd08209 -r 608483c2122a src/HOL/ex/Term.thy
--- a/src/HOL/ex/Term.thy	Mon Feb 05 21:27:16 1996 +0100
+++ b/src/HOL/ex/Term.thy	Mon Feb 05 21:29:06 1996 +0100
@@ -1,6 +1,6 @@
-(*  Title: 	HOL/ex/Term
+(*  Title:      HOL/ex/Term
     ID:         $Id$
-    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 
 Terms over a given alphabet -- function applications; illustrates list functor
@@ -16,14 +16,14 @@
 arities term :: (term)term
 
 consts
-  term		:: 'a item set => 'a item set
-  Rep_term	:: 'a term => 'a item
-  Abs_term	:: 'a item => 'a term
-  Rep_Tlist	:: 'a term list => 'a item
-  Abs_Tlist	:: 'a item => 'a term list
-  App		:: ['a, ('a term)list] => 'a term
-  Term_rec	:: ['a item, ['a item , 'a item, 'b list]=>'b] => 'b
-  term_rec	:: ['a term, ['a ,'a term list, 'b list]=>'b] => 'b
+  term          :: 'a item set => 'a item set
+  Rep_term      :: 'a term => 'a item
+  Abs_term      :: 'a item => 'a term
+  Rep_Tlist     :: 'a term list => 'a item
+  Abs_Tlist     :: 'a item => 'a term list
+  App           :: ['a, ('a term)list] => 'a term
+  Term_rec      :: ['a item, ['a item , 'a item, 'b list]=>'b] => 'b
+  term_rec      :: ['a term, ['a ,'a term list, 'b list]=>'b] => 'b
 
 inductive "term(A)"
   intrs
@@ -32,16 +32,16 @@
 
 defs
   (*defining abstraction/representation functions for term list...*)
-  Rep_Tlist_def	"Rep_Tlist == Rep_map(Rep_term)"
-  Abs_Tlist_def	"Abs_Tlist == Abs_map(Abs_term)"
+  Rep_Tlist_def "Rep_Tlist == Rep_map(Rep_term)"
+  Abs_Tlist_def "Abs_Tlist == Abs_map(Abs_term)"
 
   (*defining the abstract constants*)
-  App_def 	"App a ts == Abs_term(Leaf(a) $ Rep_Tlist(ts))"
+  App_def       "App a ts == Abs_term(Leaf(a) $ Rep_Tlist(ts))"
 
   (*list recursion*)
-  Term_rec_def	
-   "Term_rec M d == wfrec (trancl pred_sexp) M 
-           (Split(%x y g. d x y (Abs_map g y)))"
+  Term_rec_def  
+   "Term_rec M d == wfrec (trancl pred_sexp)
+           (%g. Split(%x y. d x y (Abs_map g y))) M"
 
   term_rec_def
    "term_rec t d == 
@@ -49,7 +49,7 @@
 
 rules
     (*faking a type definition for term...*)
-  Rep_term 		"Rep_term(n): term(range(Leaf))"
-  Rep_term_inverse 	"Abs_term(Rep_term(t)) = t"
-  Abs_term_inverse 	"M: term(range(Leaf)) ==> Rep_term(Abs_term(M)) = M"
+  Rep_term              "Rep_term(n): term(range(Leaf))"
+  Rep_term_inverse      "Abs_term(Rep_term(t)) = t"
+  Abs_term_inverse      "M: term(range(Leaf)) ==> Rep_term(Abs_term(M)) = M"
 end