expanded tabs; incorporated Konrad's changes
authorclasohm
Mon Feb 05 21:29:06 1996 +0100 (1996-02-05)
changeset 1476608483c2122a
parent 1475 7f5a4cd08209
child 1477 4c51ab632cda
expanded tabs; incorporated Konrad's changes
src/HOL/AxClasses/Lattice/OrdDefs.thy
src/HOL/Hoare/Arith2.ML
src/HOL/Hoare/Arith2.thy
src/HOL/Hoare/Examples.thy
src/HOL/Hoare/Hoare.thy
src/HOL/IMP/Com.thy
src/HOL/IMP/Denotation.thy
src/HOL/IMP/Equiv.thy
src/HOL/IMP/Hoare.thy
src/HOL/IMP/VC.thy
src/HOL/IOA/ABP/Abschannel.thy
src/HOL/IOA/ABP/Abschannel_finite.thy
src/HOL/IOA/ABP/Correctness.thy
src/HOL/IOA/ABP/Receiver.thy
src/HOL/IOA/ABP/Sender.thy
src/HOL/IOA/NTP/Abschannel.thy
src/HOL/IOA/meta_theory/IOA.thy
src/HOL/Integ/Equiv.thy
src/HOL/Integ/Integ.thy
src/HOL/Lambda/Commutation.thy
src/HOL/Lex/Auto.thy
src/HOL/Lex/AutoChopper.thy
src/HOL/Lex/Chopper.thy
src/HOL/Lex/Prefix.thy
src/HOL/MiniML/I.thy
src/HOL/MiniML/MiniML.thy
src/HOL/MiniML/Type.thy
src/HOL/MiniML/W.thy
src/HOL/Subst/AList.thy
src/HOL/Subst/Setplus.thy
src/HOL/Subst/Subst.thy
src/HOL/Subst/UTLemmas.thy
src/HOL/Subst/UTerm.ML
src/HOL/Subst/UTerm.thy
src/HOL/Subst/Unifier.thy
src/HOL/ex/Acc.thy
src/HOL/ex/BT.thy
src/HOL/ex/InSort.thy
src/HOL/ex/LList.thy
src/HOL/ex/LexProd.thy
src/HOL/ex/MT.thy
src/HOL/ex/NatSum.thy
src/HOL/ex/Perm.thy
src/HOL/ex/PropLog.thy
src/HOL/ex/Puzzle.thy
src/HOL/ex/Qsort.thy
src/HOL/ex/Rec.thy
src/HOL/ex/SList.ML
src/HOL/ex/SList.thy
src/HOL/ex/Simult.ML
src/HOL/ex/Simult.thy
src/HOL/ex/Sorting.thy
src/HOL/ex/Term.ML
src/HOL/ex/Term.thy
     1.1 --- a/src/HOL/AxClasses/Lattice/OrdDefs.thy	Mon Feb 05 21:27:16 1996 +0100
     1.2 +++ b/src/HOL/AxClasses/Lattice/OrdDefs.thy	Mon Feb 05 21:29:06 1996 +0100
     1.3 @@ -23,7 +23,7 @@
     1.4  
     1.5  (* duals *)
     1.6  
     1.7 -subtype
     1.8 +typedef
     1.9    'a dual = "{x::'a. True}"
    1.10  
    1.11  instance
     2.1 --- a/src/HOL/Hoare/Arith2.ML	Mon Feb 05 21:27:16 1996 +0100
     2.2 +++ b/src/HOL/Hoare/Arith2.ML	Mon Feb 05 21:29:06 1996 +0100
     2.3 @@ -30,16 +30,16 @@
     2.4  \       !!x y z. [| P x y z |] ==> P (Suc x) (Suc y) (Suc z)  \
     2.5  \    |] ==> P m n k";
     2.6  by (res_inst_tac [("x","m")] spec 1);
     2.7 -by (rtac diff_induct 1);
     2.8 -by (rtac allI 1);
     2.9 -by (rtac allI 2);
    2.10 +br diff_induct 1;
    2.11 +br allI 1;
    2.12 +br allI 2;
    2.13  by (res_inst_tac [("m","xa"),("n","x")] diff_induct 1);
    2.14  by (res_inst_tac [("m","x"),("n","Suc y")] diff_induct 4);
    2.15 -by (rtac allI 7);
    2.16 +br allI 7;
    2.17  by (nat_ind_tac "xa" 7);
    2.18  by (ALLGOALS (resolve_tac prems));
    2.19 -by (assume_tac 1);
    2.20 -by (assume_tac 1);
    2.21 +ba 1;
    2.22 +ba 1;
    2.23  by (fast_tac HOL_cs 1);
    2.24  by (fast_tac HOL_cs 1);
    2.25  qed "diff_induct3";
    2.26 @@ -48,33 +48,33 @@
    2.27  
    2.28  val prems=goal Arith.thy "~m<n+k ==> (m - n) - k = m - ((n + k)::nat)";
    2.29  by (cut_facts_tac prems 1);
    2.30 -by (rtac mp 1);
    2.31 -by (assume_tac 2);
    2.32 +br mp 1;
    2.33 +ba 2;
    2.34  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    2.35  by (ALLGOALS Asm_simp_tac);
    2.36  qed "diff_not_assoc";
    2.37  
    2.38  val prems=goal Arith.thy "[|~m<n; ~n<k|] ==> (m - n) + k = m - ((n - k)::nat)";
    2.39  by (cut_facts_tac prems 1);
    2.40 -by (dtac conjI 1);
    2.41 -by (assume_tac 1);
    2.42 +bd conjI 1;
    2.43 +ba 1;
    2.44  by (res_inst_tac [("P","~m<n & ~n<k")] mp 1);
    2.45 -by (assume_tac 2);
    2.46 +ba 2;
    2.47  by (res_inst_tac [("m","m"),("n","n"),("k","k")] diff_induct3 1);
    2.48  by (ALLGOALS Asm_simp_tac);
    2.49 -by (rtac impI 1);
    2.50 +br impI 1;
    2.51  by (dres_inst_tac [("P","~x<y")] conjE 1);
    2.52 -by (assume_tac 2);
    2.53 -by (rtac (Suc_diff_n RS sym) 1);
    2.54 -by (rtac le_less_trans 1);
    2.55 -by (etac (not_less_eq RS subst) 2);
    2.56 -by (rtac (hd ([diff_less_Suc RS lessD] RL [Suc_le_mono RS subst])) 1);
    2.57 +ba 2;
    2.58 +br (Suc_diff_n RS sym) 1;
    2.59 +br le_less_trans 1;
    2.60 +be (not_less_eq RS subst) 2;
    2.61 +br (hd ([diff_less_Suc RS lessD] RL [Suc_le_mono RS subst])) 1;
    2.62  qed "diff_add_not_assoc";
    2.63  
    2.64  val prems=goal Arith.thy "~n<k ==> (m + n) - k = m + ((n - k)::nat)";
    2.65  by (cut_facts_tac prems 1);
    2.66 -by (rtac mp 1);
    2.67 -by (assume_tac 2);
    2.68 +br mp 1;
    2.69 +ba 2;
    2.70  by (res_inst_tac [("m","n"),("n","k")] diff_induct 1);
    2.71  by (ALLGOALS Asm_simp_tac);
    2.72  qed "add_diff_assoc";
    2.73 @@ -82,12 +82,12 @@
    2.74  (*** more ***)
    2.75  
    2.76  val prems = goal Arith.thy "m~=(n::nat) = (m<n | n<m)";
    2.77 -by (rtac iffI 1);
    2.78 +br iffI 1;
    2.79  by (cut_inst_tac [("m","m"),("n","n")] less_linear 1);
    2.80  by (Asm_full_simp_tac 1);
    2.81 -by (etac disjE 1);
    2.82 -by (etac (less_not_refl2 RS not_sym) 1);
    2.83 -by (etac less_not_refl2 1);
    2.84 +be disjE 1;
    2.85 +be (less_not_refl2 RS not_sym) 1;
    2.86 +be less_not_refl2 1;
    2.87  qed "not_eq_eq_less_or_gr";
    2.88  
    2.89  val [prem] = goal Arith.thy "m<n ==> n-m~=0";
    2.90 @@ -115,7 +115,7 @@
    2.91  by (res_inst_tac [("n","k")] natE 1);
    2.92  by (ALLGOALS Asm_full_simp_tac);
    2.93  by (nat_ind_tac "x" 1);
    2.94 -by (etac add_less_mono 2);
    2.95 +be add_less_mono 2;
    2.96  by (ALLGOALS Asm_full_simp_tac);
    2.97  qed "mult_less_mono_r";
    2.98  
    2.99 @@ -124,8 +124,8 @@
   2.100  by (nat_ind_tac "k" 1);
   2.101  by (ALLGOALS Simp_tac);
   2.102  by (fold_goals_tac [le_def]);
   2.103 -by (etac add_le_mono 1);
   2.104 -by (assume_tac 1);
   2.105 +be add_le_mono 1;
   2.106 +ba 1;
   2.107  qed "mult_not_less_mono_r";
   2.108  
   2.109  val prems = goal Arith.thy "m=(n::nat) ==> m*k=n*k";
   2.110 @@ -137,10 +137,10 @@
   2.111  val prems = goal Arith.thy "[|0<k; m~=(n::nat)|] ==> m*k~=n*k";
   2.112  by (cut_facts_tac prems 1);
   2.113  by (res_inst_tac [("P","m<n"),("Q","n<m")] disjE 1);
   2.114 -by (rtac (less_not_refl2 RS not_sym) 2);
   2.115 -by (etac mult_less_mono_r 2);
   2.116 -by (rtac less_not_refl2 3);
   2.117 -by (etac mult_less_mono_r 3);
   2.118 +br (less_not_refl2 RS not_sym) 2;
   2.119 +be mult_less_mono_r 2;
   2.120 +br less_not_refl2 3;
   2.121 +be mult_less_mono_r 3;
   2.122  by (ALLGOALS (asm_full_simp_tac ((simpset_of "Arith") addsimps [not_eq_eq_less_or_gr])));
   2.123  qed "mult_not_eq_mono_r";
   2.124  
   2.125 @@ -149,24 +149,29 @@
   2.126  val prems = goal Arith.thy "(m - n)*k = (m*k) - ((n*k)::nat)";
   2.127  by (res_inst_tac [("P","m*k<n*k")] case_split_thm 1);
   2.128  by (forward_tac [mult_not_less_mono_r COMP not_imp_swap] 1);
   2.129 -by (dtac (less_not_sym RS (not_less_eq RS iffD1) RS less_imp_diff_is_0) 1);
   2.130 -by (dtac (less_not_sym RS (not_less_eq RS iffD1) RS less_imp_diff_is_0) 1);
   2.131 -by (rtac mp 2);
   2.132 -by (assume_tac 3);
   2.133 +bd (less_not_sym RS (not_less_eq RS iffD1) RS less_imp_diff_is_0) 1;
   2.134 +bd (less_not_sym RS (not_less_eq RS iffD1) RS less_imp_diff_is_0) 1;
   2.135 +br mp 2;
   2.136 +ba 3;
   2.137  by (res_inst_tac [("m","m"),("n","n")] diff_induct 2);
   2.138  by (ALLGOALS Asm_simp_tac);
   2.139 -by (rtac impI 1);
   2.140 -by (dtac (refl RS iffD1) 1);
   2.141 +br impI 1;
   2.142 +bd (refl RS iffD1) 1;
   2.143  by (dres_inst_tac [("k","k")] add_not_less_mono_l 1);
   2.144 -by (dtac (refl RS iffD1) 1);
   2.145 -by (dtac (refl RS iffD1) 1);
   2.146 -by (dtac diff_not_assoc 1);
   2.147 +bd (refl RS iffD1) 1;
   2.148 +bd (refl RS iffD1) 1;
   2.149 +bd diff_not_assoc 1;
   2.150  by (asm_full_simp_tac ((simpset_of "Arith") addsimps [diff_add_inverse]) 1);
   2.151  qed "diff_mult_distrib_r";
   2.152  
   2.153  
   2.154  (*** mod ***)
   2.155  
   2.156 +goal Arith.thy "(%m. m mod n) = wfrec (trancl pred_nat) \
   2.157 +             \                      (%f j. if j<n then j else f (j-n))";
   2.158 +by (simp_tac (HOL_ss addsimps [mod_def]) 1);
   2.159 +val mod_def = result() RS eq_reflection;
   2.160 +
   2.161  (* Alternativ-Beweis zu mod_nn_is_0: Spezialfall zu mod_prod_nn_is_0 *)
   2.162  (*
   2.163  val prems = goal thy "0<n ==> n mod n = 0";
   2.164 @@ -178,29 +183,29 @@
   2.165  
   2.166  val prems=goal thy "0<n ==> n mod n = 0";
   2.167  by (cut_facts_tac prems 1);
   2.168 -by (rtac (mod_def RS wf_less_trans) 1);
   2.169 +br (mod_def RS wf_less_trans) 1;
   2.170  by (asm_full_simp_tac ((simpset_of "Arith") addsimps [diff_self_eq_0,cut_def,less_eq]) 1);
   2.171 -by (etac mod_less 1);
   2.172 +be mod_less 1;
   2.173  qed "mod_nn_is_0";
   2.174  
   2.175  val prems=goal thy "0<n ==> m mod n = (m+n) mod n";
   2.176  by (cut_facts_tac prems 1);
   2.177  by (res_inst_tac [("s","n+m"),("t","m+n")] subst 1);
   2.178 -by (rtac add_commute 1);
   2.179 +br add_commute 1;
   2.180  by (res_inst_tac [("s","n+m-n"),("P","%x.x mod n = (n + m) mod n")] subst 1);
   2.181 -by (rtac diff_add_inverse 1);
   2.182 -by (rtac sym 1);
   2.183 -by (etac mod_geq 1);
   2.184 +br diff_add_inverse 1;
   2.185 +br sym 1;
   2.186 +be mod_geq 1;
   2.187  by (res_inst_tac [("s","n<=n+m"),("t","~n+m<n")] subst 1);
   2.188  by (simp_tac ((simpset_of "Arith") addsimps [le_def]) 1);
   2.189 -by (rtac le_add1 1);
   2.190 +br le_add1 1;
   2.191  qed "mod_eq_add";
   2.192  
   2.193  val prems=goal thy "0<n ==> m*n mod n = 0";
   2.194  by (cut_facts_tac prems 1);
   2.195  by (nat_ind_tac "m" 1);
   2.196  by (Simp_tac 1);
   2.197 -by (etac mod_less 1);
   2.198 +be mod_less 1;
   2.199  by (dres_inst_tac [("n","n"),("m","m1*n")] mod_eq_add 1);
   2.200  by (asm_full_simp_tac ((simpset_of "Arith") addsimps [add_commute]) 1);
   2.201  qed "mod_prod_nn_is_0";
   2.202 @@ -208,37 +213,38 @@
   2.203  val prems=goal thy "[|0<x; m mod x = 0; n mod x = 0|] ==> (m+n) mod x = 0";
   2.204  by (cut_facts_tac prems 1);
   2.205  by (res_inst_tac [("s","m div x * x + m mod x"),("t","m")] subst 1);
   2.206 -by (etac mod_div_equality 1);
   2.207 +be mod_div_equality 1;
   2.208  by (res_inst_tac [("s","n div x * x + n mod x"),("t","n")] subst 1);
   2.209 -by (etac mod_div_equality 1);
   2.210 +be mod_div_equality 1;
   2.211  by (Asm_simp_tac 1);
   2.212  by (res_inst_tac [("s","(m div x + n div x) * x"),("t","m div x * x + n div x * x")] subst 1);
   2.213 -by (rtac add_mult_distrib 1);
   2.214 -by (etac mod_prod_nn_is_0 1);
   2.215 +br add_mult_distrib 1;
   2.216 +be mod_prod_nn_is_0 1;
   2.217  qed "mod0_sum";
   2.218  
   2.219  val prems=goal thy "[|0<x; m mod x = 0; n mod x = 0; n<=m|] ==> (m-n) mod x = 0";
   2.220  by (cut_facts_tac prems 1);
   2.221  by (res_inst_tac [("s","m div x * x + m mod x"),("t","m")] subst 1);
   2.222 -by (etac mod_div_equality 1);
   2.223 +be mod_div_equality 1;
   2.224  by (res_inst_tac [("s","n div x * x + n mod x"),("t","n")] subst 1);
   2.225 -by (etac mod_div_equality 1);
   2.226 +be mod_div_equality 1;
   2.227  by (Asm_simp_tac 1);
   2.228  by (res_inst_tac [("s","(m div x - n div x) * x"),("t","m div x * x - n div x * x")] subst 1);
   2.229 -by (rtac diff_mult_distrib_r 1);
   2.230 -by (etac mod_prod_nn_is_0 1);
   2.231 +br diff_mult_distrib_r 1;
   2.232 +be mod_prod_nn_is_0 1;
   2.233  qed "mod0_diff";
   2.234  
   2.235  
   2.236  (*** div ***)
   2.237  
   2.238 +
   2.239  val prems = goal thy "0<n ==> m*n div n = m";
   2.240  by (cut_facts_tac prems 1);
   2.241 -by (rtac (mult_not_eq_mono_r RS not_imp_swap) 1);
   2.242 -by (assume_tac 1);
   2.243 -by (assume_tac 1);
   2.244 +br (mult_not_eq_mono_r RS not_imp_swap) 1;
   2.245 +ba 1;
   2.246 +ba 1;
   2.247  by (res_inst_tac [("P","%x.m*n div n * n = x")] (mod_div_equality RS subst) 1);
   2.248 -by (assume_tac 1);
   2.249 +ba 1;
   2.250  by (dres_inst_tac [("m","m")] mod_prod_nn_is_0 1);
   2.251  by (Asm_simp_tac 1);
   2.252  qed "div_prod_nn_is_m";
   2.253 @@ -254,32 +260,32 @@
   2.254  
   2.255  val prems=goalw thy [divides_def] "x divides n ==> x<=n";
   2.256  by (cut_facts_tac prems 1);
   2.257 -by (rtac ((mod_less COMP rev_contrapos) RS (le_def RS meta_eq_to_obj_eq RS iffD2)) 1);
   2.258 +br ((mod_less COMP rev_contrapos) RS (le_def RS meta_eq_to_obj_eq RS iffD2)) 1;
   2.259  by (Asm_simp_tac 1);
   2.260 -by (rtac (less_not_refl2 RS not_sym) 1);
   2.261 +br (less_not_refl2 RS not_sym) 1;
   2.262  by (Asm_simp_tac 1);
   2.263  qed "divides_le";
   2.264  
   2.265  val prems=goalw thy [divides_def] "[|x divides m; x divides n|] ==> x divides (m+n)";
   2.266  by (cut_facts_tac prems 1);
   2.267  by (REPEAT ((dtac conjE 1) THEN (atac 2)));
   2.268 -by (rtac conjI 1);
   2.269 +br conjI 1;
   2.270  by (dres_inst_tac [("m","0"),("n","m")] less_imp_add_less 1);
   2.271 -by (assume_tac 1);
   2.272 -by (etac conjI 1);
   2.273 -by (rtac mod0_sum 1);
   2.274 +ba 1;
   2.275 +be conjI 1;
   2.276 +br mod0_sum 1;
   2.277  by (ALLGOALS atac);
   2.278  qed "divides_sum";
   2.279  
   2.280  val prems=goalw thy [divides_def] "[|x divides m; x divides n; n<m|] ==> x divides (m-n)";
   2.281  by (cut_facts_tac prems 1);
   2.282  by (REPEAT ((dtac conjE 1) THEN (atac 2)));
   2.283 -by (rtac conjI 1);
   2.284 -by (etac less_imp_diff_positive 1);
   2.285 -by (etac conjI 1);
   2.286 -by (rtac mod0_diff 1);
   2.287 +br conjI 1;
   2.288 +be less_imp_diff_positive 1;
   2.289 +be conjI 1;
   2.290 +br mod0_diff 1;
   2.291  by (ALLGOALS (asm_simp_tac ((simpset_of "Arith") addsimps [le_def])));
   2.292 -by (etac less_not_sym 1);
   2.293 +be less_not_sym 1;
   2.294  qed "divides_diff";
   2.295  
   2.296  
   2.297 @@ -288,16 +294,16 @@
   2.298  
   2.299  val prems=goalw thy [cd_def] "0<n ==> cd n n n";
   2.300  by (cut_facts_tac prems 1);
   2.301 -by (dtac divides_nn 1);
   2.302 +bd divides_nn 1;
   2.303  by (Asm_simp_tac 1);
   2.304  qed "cd_nnn";
   2.305  
   2.306  val prems=goalw thy [cd_def] "cd x m n ==> x<=m & x<=n";
   2.307  by (cut_facts_tac prems 1);
   2.308 -by (dtac conjE 1);
   2.309 -by (assume_tac 2);
   2.310 -by (dtac divides_le 1);
   2.311 -by (dtac divides_le 1);
   2.312 +bd conjE 1;
   2.313 +ba 2;
   2.314 +bd divides_le 1;
   2.315 +bd divides_le 1;
   2.316  by (Asm_simp_tac 1);
   2.317  qed "cd_le";
   2.318  
   2.319 @@ -307,32 +313,32 @@
   2.320  
   2.321  val prems=goalw thy [cd_def] "n<m ==> cd x m n = cd x (m-n) n";
   2.322  by (cut_facts_tac prems 1);
   2.323 -by (rtac iffI 1);
   2.324 -by (dtac conjE 1);
   2.325 -by (assume_tac 2);
   2.326 -by (rtac conjI 1);
   2.327 -by (rtac divides_diff 1);
   2.328 -by (dtac conjE 5);
   2.329 -by (assume_tac 6);
   2.330 -by (rtac conjI 5);
   2.331 -by (dtac less_not_sym 5);
   2.332 -by (dtac add_diff_inverse 5);
   2.333 +br iffI 1;
   2.334 +bd conjE 1;
   2.335 +ba 2;
   2.336 +br conjI 1;
   2.337 +br divides_diff 1;
   2.338 +bd conjE 5;
   2.339 +ba 6;
   2.340 +br conjI 5;
   2.341 +bd less_not_sym 5;
   2.342 +bd add_diff_inverse 5;
   2.343  by (dres_inst_tac [("m","n"),("n","m-n")] divides_sum 5);
   2.344  by (ALLGOALS Asm_full_simp_tac);
   2.345  qed "cd_diff_l";
   2.346  
   2.347  val prems=goalw thy [cd_def] "m<n ==> cd x m n = cd x m (n-m)";
   2.348  by (cut_facts_tac prems 1);
   2.349 -by (rtac iffI 1);
   2.350 -by (dtac conjE 1);
   2.351 -by (assume_tac 2);
   2.352 -by (rtac conjI 1);
   2.353 -by (rtac divides_diff 2);
   2.354 -by (dtac conjE 5);
   2.355 -by (assume_tac 6);
   2.356 -by (rtac conjI 5);
   2.357 -by (dtac less_not_sym 6);
   2.358 -by (dtac add_diff_inverse 6);
   2.359 +br iffI 1;
   2.360 +bd conjE 1;
   2.361 +ba 2;
   2.362 +br conjI 1;
   2.363 +br divides_diff 2;
   2.364 +bd conjE 5;
   2.365 +ba 6;
   2.366 +br conjI 5;
   2.367 +bd less_not_sym 6;
   2.368 +bd add_diff_inverse 6;
   2.369  by (dres_inst_tac [("n","n-m")] divides_sum 6);
   2.370  by (ALLGOALS Asm_full_simp_tac);
   2.371  qed "cd_diff_r";
   2.372 @@ -342,15 +348,15 @@
   2.373  
   2.374  val prems = goalw thy [gcd_def] "0<n ==> n = gcd n n";
   2.375  by (cut_facts_tac prems 1);
   2.376 -by (dtac cd_nnn 1);
   2.377 -by (rtac (select_equality RS sym) 1);
   2.378 -by (etac conjI 1);
   2.379 -by (rtac allI 1);
   2.380 -by (rtac impI 1);
   2.381 -by (dtac cd_le 1);
   2.382 -by (dtac conjE 2);
   2.383 -by (assume_tac 3);
   2.384 -by (rtac le_anti_sym 2);
   2.385 +bd cd_nnn 1;
   2.386 +br (select_equality RS sym) 1;
   2.387 +be conjI 1;
   2.388 +br allI 1;
   2.389 +br impI 1;
   2.390 +bd cd_le 1;
   2.391 +bd conjE 2;
   2.392 +ba 3;
   2.393 +br le_anti_sym 2;
   2.394  by (dres_inst_tac [("x","x")] cd_le 2);
   2.395  by (dres_inst_tac [("x","n")] spec 3);
   2.396  by (ALLGOALS Asm_full_simp_tac);
   2.397 @@ -364,16 +370,16 @@
   2.398  by (cut_facts_tac prems 1);
   2.399  by (subgoal_tac "n<m ==> !x.cd x m n = cd x (m-n) n" 1);
   2.400  by (Asm_simp_tac 1);
   2.401 -by (rtac allI 1);
   2.402 -by (etac cd_diff_l 1);
   2.403 +br allI 1;
   2.404 +be cd_diff_l 1;
   2.405  qed "gcd_diff_l";
   2.406  
   2.407  val prems=goalw thy [gcd_def] "m<n ==> gcd m n = gcd m (n-m)";
   2.408  by (cut_facts_tac prems 1);
   2.409  by (subgoal_tac "m<n ==> !x.cd x m n = cd x m (n-m)" 1);
   2.410  by (Asm_simp_tac 1);
   2.411 -by (rtac allI 1);
   2.412 -by (etac cd_diff_r 1);
   2.413 +br allI 1;
   2.414 +be cd_diff_r 1;
   2.415  qed "gcd_diff_r";
   2.416  
   2.417  
   2.418 @@ -392,7 +398,7 @@
   2.419  by (nat_ind_tac "k" 1);
   2.420  by (ALLGOALS Asm_simp_tac);
   2.421  by (fold_goals_tac [pow_def]);
   2.422 -by (rtac (pow_add_reduce RS sym) 1);
   2.423 +br (pow_add_reduce RS sym) 1;
   2.424  qed "pow_pow_reduce";
   2.425  
   2.426  (*** fac ***)
     3.1 --- a/src/HOL/Hoare/Arith2.thy	Mon Feb 05 21:27:16 1996 +0100
     3.2 +++ b/src/HOL/Hoare/Arith2.thy	Mon Feb 05 21:29:06 1996 +0100
     3.3 @@ -1,6 +1,6 @@
     3.4 -(*  Title: 	HOL/Hoare/Arith2.thy
     3.5 +(*  Title:      HOL/Hoare/Arith2.thy
     3.6      ID:         $Id$
     3.7 -    Author: 	Norbert Galm
     3.8 +    Author:     Norbert Galm
     3.9      Copyright   1995 TUM
    3.10  
    3.11  More arithmetic.
    3.12 @@ -9,19 +9,19 @@
    3.13  Arith2 = Arith +
    3.14  
    3.15  consts
    3.16 -  divides :: [nat, nat] => bool			(infixl 70)
    3.17 -  cd	  :: [nat, nat, nat] => bool
    3.18 -  gcd	  :: [nat, nat] => nat
    3.19 +  divides :: [nat, nat] => bool                 (infixl 70)
    3.20 +  cd      :: [nat, nat, nat] => bool
    3.21 +  gcd     :: [nat, nat] => nat
    3.22  
    3.23 -  pow	  :: [nat, nat] => nat			(infixl 75)
    3.24 -  fac	  :: nat => nat
    3.25 +  pow     :: [nat, nat] => nat                  (infixl 75)
    3.26 +  fac     :: nat => nat
    3.27  
    3.28  defs
    3.29 -  divides_def	"x divides n == 0<n & 0<x & (n mod x) = 0"
    3.30 -  cd_def	"cd x m n  == x divides m & x divides n"
    3.31 -  gcd_def	"gcd m n     == @x.(cd x m n) & (!y.(cd y m n) --> y<=x)"
    3.32 +  divides_def   "x divides n == 0<n & 0<x & (n mod x) = 0"
    3.33 +  cd_def        "cd x m n  == x divides m & x divides n"
    3.34 +  gcd_def       "gcd m n     == @x.(cd x m n) & (!y.(cd y m n) --> y<=x)"
    3.35  
    3.36 -  pow_def	"m pow n     == nat_rec n (Suc 0) (%u v.m*v)"
    3.37 -  fac_def	"fac m       == nat_rec m (Suc 0) (%u v.(Suc u)*v)"
    3.38 +  pow_def       "m pow n     == nat_rec n (Suc 0) (%u v.m*v)"
    3.39 +  fac_def       "fac m       == nat_rec m (Suc 0) (%u v.(Suc u)*v)"
    3.40  
    3.41  end
     4.1 --- a/src/HOL/Hoare/Examples.thy	Mon Feb 05 21:27:16 1996 +0100
     4.2 +++ b/src/HOL/Hoare/Examples.thy	Mon Feb 05 21:29:06 1996 +0100
     4.3 @@ -1,6 +1,6 @@
     4.4 -(*  Title: 	HOL/Hoare/Examples.thy
     4.5 +(*  Title:      HOL/Hoare/Examples.thy
     4.6      ID:         $Id$
     4.7 -    Author: 	Norbert Galm
     4.8 +    Author:     Norbert Galm
     4.9      Copyright   1995 TUM
    4.10  
    4.11  Various arithmetic examples.
    4.12 @@ -9,8 +9,8 @@
    4.13  Examples = Hoare + Arith2 +
    4.14  
    4.15  syntax
    4.16 -  "@1"	:: nat	("1")
    4.17 -  "@2"	:: nat	("2")
    4.18 +  "@1"  :: nat  ("1")
    4.19 +  "@2"  :: nat  ("2")
    4.20  
    4.21  translations
    4.22    "1" == "Suc(0)"
     5.1 --- a/src/HOL/Hoare/Hoare.thy	Mon Feb 05 21:27:16 1996 +0100
     5.2 +++ b/src/HOL/Hoare/Hoare.thy	Mon Feb 05 21:29:06 1996 +0100
     5.3 @@ -1,6 +1,6 @@
     5.4 -(*  Title: 	HOL/Hoare/Hoare.thy
     5.5 +(*  Title:      HOL/Hoare/Hoare.thy
     5.6      ID:         $Id$
     5.7 -    Author: 	Norbert Galm & Tobias Nipkow
     5.8 +    Author:     Norbert Galm & Tobias Nipkow
     5.9      Copyright   1995 TUM
    5.10  
    5.11  Sugared semantic embedding of Hoare logic.
    5.12 @@ -9,49 +9,49 @@
    5.13  Hoare = Arith +
    5.14  
    5.15  types
    5.16 -  'a prog			(* program syntax *)
    5.17 -  pvar = nat			(* encoding of program variables ( < 26! ) *)
    5.18 -  'a state = pvar => 'a		(* program state *)
    5.19 -  'a exp = 'a state => 'a	(* denotation of expressions *)
    5.20 -  'a bexp = 'a state => bool	(* denotation of boolean expressions *)
    5.21 +  'a prog                       (* program syntax *)
    5.22 +  pvar = nat                    (* encoding of program variables ( < 26! ) *)
    5.23 +  'a state = pvar => 'a         (* program state *)
    5.24 +  'a exp = 'a state => 'a       (* denotation of expressions *)
    5.25 +  'a bexp = 'a state => bool    (* denotation of boolean expressions *)
    5.26    'a com = 'a state => 'a state => bool (* denotation of programs *)
    5.27  
    5.28  syntax
    5.29 -  "@Skip"       :: 'a prog				("SKIP")
    5.30 -  "@Assign"	:: [id, 'a] => 'a prog		("_ := _")
    5.31 -  "@Seq"	:: ['a prog, 'a prog] => 'a prog	("_;//_" [0,1000] 999)
    5.32 -  "@If"		:: [bool, 'a prog, 'a prog] => 'a prog
    5.33 +  "@Skip"       :: 'a prog                              ("SKIP")
    5.34 +  "@Assign"     :: [id, 'a] => 'a prog          ("_ := _")
    5.35 +  "@Seq"        :: ['a prog, 'a prog] => 'a prog        ("_;//_" [0,1000] 999)
    5.36 +  "@If"         :: [bool, 'a prog, 'a prog] => 'a prog
    5.37                     ("IF _//THEN//  (_)//ELSE//  (_)//END")
    5.38 -  "@While"	:: [bool, bool, 'a prog] => 'a prog
    5.39 +  "@While"      :: [bool, bool, 'a prog] => 'a prog
    5.40                     ("WHILE _//DO {_}//  (_)//END")
    5.41  
    5.42 -  "@Spec"	:: [bool, 'a prog, bool] => bool	("{_}//_//{_}")
    5.43 +  "@Spec"       :: [bool, 'a prog, bool] => bool        ("{_}//_//{_}")
    5.44  
    5.45  consts
    5.46    (* semantics *)
    5.47  
    5.48 -  Skip		:: 'a com
    5.49 -  Assign	:: [pvar, 'a exp] => 'a com
    5.50 -  Seq		:: ['a com, 'a com] => 'a com
    5.51 -  Cond		:: ['a bexp, 'a com, 'a com] => 'a com
    5.52 -  While		:: ['a bexp, 'a bexp, 'a com] => 'a com
    5.53 -  Iter		:: [nat, 'a bexp, 'a com] => 'a com
    5.54 +  Skip          :: 'a com
    5.55 +  Assign        :: [pvar, 'a exp] => 'a com
    5.56 +  Seq           :: ['a com, 'a com] => 'a com
    5.57 +  Cond          :: ['a bexp, 'a com, 'a com] => 'a com
    5.58 +  While         :: ['a bexp, 'a bexp, 'a com] => 'a com
    5.59 +  Iter          :: [nat, 'a bexp, 'a com] => 'a com
    5.60  
    5.61 -  Spec		:: ['a bexp, 'a com, 'a bexp] => bool
    5.62 +  Spec          :: ['a bexp, 'a com, 'a bexp] => bool
    5.63  
    5.64  defs
    5.65    (* denotational semantics *)
    5.66  
    5.67 -  SkipDef	"Skip s s' == (s=s')"
    5.68 -  AssignDef	"Assign v e s s' == (s' = (%x.if x=v then e(s) else s(x)))"
    5.69 -  SeqDef	"Seq c c' s s' == ? s''. c s s'' & c' s'' s'"
    5.70 -  CondDef	"Cond b c c' s s' == (b(s) --> c s s') & (~b s --> c' s s')"
    5.71 -  WhileDef	"While b inv c s s' == ? n. Iter n b c s s'"
    5.72 +  SkipDef       "Skip s s' == (s=s')"
    5.73 +  AssignDef     "Assign v e s s' == (s' = (%x.if x=v then e(s) else s(x)))"
    5.74 +  SeqDef        "Seq c c' s s' == ? s''. c s s'' & c' s'' s'"
    5.75 +  CondDef       "Cond b c c' s s' == (b(s) --> c s s') & (~b s --> c' s s')"
    5.76 +  WhileDef      "While b inv c s s' == ? n. Iter n b c s s'"
    5.77  
    5.78 -  IterDef	"Iter n b c == nat_rec n (%s s'.~b(s) & (s=s'))
    5.79 -		           (%n_rec iter_rec.%s s'.b(s) & Seq c iter_rec s s')"
    5.80 +  IterDef       "Iter n b c == nat_rec n (%s s'.~b(s) & (s=s'))
    5.81 +                           (%n_rec iter_rec.%s s'.b(s) & Seq c iter_rec s s')"
    5.82  
    5.83 -  SpecDef	"Spec p c q == !s s'. c s s' --> p s --> q s'"
    5.84 +  SpecDef       "Spec p c q == !s s'. c s s' --> p s --> q s'"
    5.85  
    5.86  end
    5.87  
    5.88 @@ -63,53 +63,53 @@
    5.89  (* name_in_term:bool (name:string,trm:term) bestimmt, ob in trm der Name name als Konstante,
    5.90     freie Var., scheme-Variable oder als Name fuer eine Lambda-Abstraktion vorkommt *)
    5.91  
    5.92 -fun name_in_term (name,Const (s,t))	=(name=s)
    5.93 -  | name_in_term (name,Free (s,t))	=(name=s)
    5.94 -  | name_in_term (name,Var ((s,i),t))	=(name=s ^ makestring i)
    5.95 -  | name_in_term (name,Abs (s,t,trm))	=(name=s) orelse (name_in_term (name,trm))
    5.96 -  | name_in_term (name,trm1 $ trm2)	=(name_in_term (name,trm1)) orelse (name_in_term (name,trm2))
    5.97 -  | name_in_term (_,_)			=false;
    5.98 +fun name_in_term (name,Const (s,t))     =(name=s)
    5.99 +  | name_in_term (name,Free (s,t))      =(name=s)
   5.100 +  | name_in_term (name,Var ((s,i),t))   =(name=s ^ makestring i)
   5.101 +  | name_in_term (name,Abs (s,t,trm))   =(name=s) orelse (name_in_term (name,trm))
   5.102 +  | name_in_term (name,trm1 $ trm2)     =(name_in_term (name,trm1)) orelse (name_in_term (name,trm2))
   5.103 +  | name_in_term (_,_)                  =false;
   5.104  
   5.105  (* variant_name:string (name:string,trm:term) liefert einen von name abgewandelten Namen (durch Anhaengen
   5.106     von genuegend vielen "_"), der nicht in trm vorkommt. Im Gegensatz zu variant_abs beruecktsichtigt es
   5.107     auch Namen von scheme-Variablen und von Lambda-Abstraktionen in trm *)
   5.108  
   5.109 -fun variant_name (name,trm)	=if name_in_term (name,trm)
   5.110 -					then variant_name (name ^ "_",trm)
   5.111 -					else name;
   5.112 +fun variant_name (name,trm)     =if name_in_term (name,trm)
   5.113 +                                        then variant_name (name ^ "_",trm)
   5.114 +                                        else name;
   5.115  
   5.116  (* subst_term:term (von:term,nach:term,trm:term) liefert den Term, der aus
   5.117  trm entsteht, wenn alle Teilterme, die gleich von sind, durch nach ersetzt
   5.118  wurden *)
   5.119  
   5.120 -fun subst_term (von,nach,Abs (s,t,trm))	=if von=Abs (s,t,trm)
   5.121 -						then nach
   5.122 -						else Abs (s,t,subst_term (von,nach,trm))
   5.123 -  | subst_term (von,nach,trm1 $ trm2)	=if von=trm1 $ trm2
   5.124 -						then nach
   5.125 -						else subst_term (von,nach,trm1) $ subst_term (von,nach,trm2)
   5.126 -  | subst_term (von,nach,trm)		=if von=trm
   5.127 -						then nach
   5.128 -						else trm;
   5.129 +fun subst_term (von,nach,Abs (s,t,trm)) =if von=Abs (s,t,trm)
   5.130 +                                                then nach
   5.131 +                                                else Abs (s,t,subst_term (von,nach,trm))
   5.132 +  | subst_term (von,nach,trm1 $ trm2)   =if von=trm1 $ trm2
   5.133 +                                                then nach
   5.134 +                                                else subst_term (von,nach,trm1) $ subst_term (von,nach,trm2)
   5.135 +  | subst_term (von,nach,trm)           =if von=trm
   5.136 +                                                then nach
   5.137 +                                                else trm;
   5.138  
   5.139  
   5.140  (* Translation between program vars ("a" - "z") and their encoding as
   5.141     natural numbers: "a" <==> 0, "b" <==> Suc(0), ..., "z" <==> 25 *)
   5.142  
   5.143 -fun is_pvarID s	= size s=1 andalso "a"<=s andalso s<="z";
   5.144 +fun is_pvarID s = size s=1 andalso "a"<=s andalso s<="z";
   5.145  
   5.146  fun pvarID2pvar s =
   5.147    let fun rest2pvar (i,arg) =
   5.148              if i=0 then arg else rest2pvar(i-1, Syntax.const "Suc" $ arg)
   5.149    in rest2pvar(ord s - ord "a", Syntax.const "0") end;
   5.150  
   5.151 -fun pvar2pvarID trm	=
   5.152 -	let
   5.153 -		fun rest2pvarID (Const("0",_),i)		=chr (i + ord "a")
   5.154 -		  | rest2pvarID (Const("Suc",_) $ trm,i)	=rest2pvarID (trm,i+1)
   5.155 -	in
   5.156 -		rest2pvarID (trm,0)
   5.157 -	end;
   5.158 +fun pvar2pvarID trm     =
   5.159 +        let
   5.160 +                fun rest2pvarID (Const("0",_),i)                =chr (i + ord "a")
   5.161 +                  | rest2pvarID (Const("Suc",_) $ trm,i)        =rest2pvarID (trm,i+1)
   5.162 +        in
   5.163 +                rest2pvarID (trm,0)
   5.164 +        end;
   5.165  
   5.166  
   5.167  (*** parse translations: syntax -> semantics ***)
   5.168 @@ -119,10 +119,10 @@
   5.169     bei name="s" und dem Term "a=b & a=X" wird der Term "s(0)=s(Suc(0)) & s(0)=X" geliefert *)
   5.170  
   5.171  fun term_tr (name,Free (s,t)) = if is_pvarID s
   5.172 -				then Syntax.free name $ pvarID2pvar s
   5.173 -				else Free (s,t)
   5.174 +                                then Syntax.free name $ pvarID2pvar s
   5.175 +                                else Free (s,t)
   5.176    | term_tr (name,Abs (s,t,trm)) = Abs (s,t,term_tr (name,trm))
   5.177 -  | term_tr (name,trm1 $ trm2)	= term_tr (name,trm1) $ term_tr (name,trm2)
   5.178 +  | term_tr (name,trm1 $ trm2)  = term_tr (name,trm1) $ term_tr (name,trm2)
   5.179    | term_tr (name,trm) = trm;
   5.180  
   5.181  fun bool_tr B =
   5.182 @@ -133,12 +133,12 @@
   5.183    let val name = variant_name("s",E)
   5.184    in Abs (name,dummyT,abstract_over (Syntax.free name,term_tr (name,E))) end;
   5.185  
   5.186 -fun prog_tr (Const ("@Skip",_))	= Syntax.const "Skip"
   5.187 +fun prog_tr (Const ("@Skip",_)) = Syntax.const "Skip"
   5.188    | prog_tr (Const ("@Assign",_) $ Free (V,_) $ E) =
   5.189        if is_pvarID V
   5.190        then Syntax.const "Assign" $ pvarID2pvar V $ exp_tr E
   5.191        else error("Not a valid program variable: " ^ quote V)
   5.192 -  | prog_tr (Const ("@Seq",_) $ C $ C')	=
   5.193 +  | prog_tr (Const ("@Seq",_) $ C $ C') =
   5.194        Syntax.const "Seq" $ prog_tr C $ prog_tr C'
   5.195    | prog_tr (Const ("@If",_) $ B $ C $ C') =
   5.196        Syntax.const "Cond" $ bool_tr B $ prog_tr C $ prog_tr C'
   5.197 @@ -154,25 +154,25 @@
   5.198  
   5.199  (* term_tr':term (name:string,trm:term) ersetzt in trm alle Vorkommen von name $ pvar durch
   5.200     entsprechende freie Variablen, welche die pvarID zu pvar darstellen. Beispiel:
   5.201 -	bei name="s" und dem Term "s(0)=s(Suc(0)) & s(0)=X" wird der Term "a=b & a=X" geliefert *)
   5.202 +        bei name="s" und dem Term "s(0)=s(Suc(0)) & s(0)=X" wird der Term "a=b & a=X" geliefert *)
   5.203  
   5.204 -fun term_tr' (name,Free (s,t) $ trm)	=if name=s
   5.205 -						then Syntax.free (pvar2pvarID trm)
   5.206 -						else Free (s,t) $ term_tr' (name,trm)
   5.207 -  | term_tr' (name,Abs (s,t,trm))	=Abs (s,t,term_tr' (name,trm))
   5.208 -  | term_tr' (name,trm1 $ trm2)		=term_tr' (name,trm1) $ term_tr' (name,trm2)
   5.209 -  | term_tr' (name,trm)			=trm;
   5.210 +fun term_tr' (name,Free (s,t) $ trm)    =if name=s
   5.211 +                                                then Syntax.free (pvar2pvarID trm)
   5.212 +                                                else Free (s,t) $ term_tr' (name,trm)
   5.213 +  | term_tr' (name,Abs (s,t,trm))       =Abs (s,t,term_tr' (name,trm))
   5.214 +  | term_tr' (name,trm1 $ trm2)         =term_tr' (name,trm1) $ term_tr' (name,trm2)
   5.215 +  | term_tr' (name,trm)                 =trm;
   5.216  
   5.217 -fun bexp_tr' (Abs(_,_,b))	=term_tr' (variant_abs ("s",dummyT,b));
   5.218 +fun bexp_tr' (Abs(_,_,b))       =term_tr' (variant_abs ("s",dummyT,b));
   5.219  
   5.220 -fun exp_tr' (Abs(_,_,e))	=term_tr' (variant_abs ("s",dummyT,e));
   5.221 +fun exp_tr' (Abs(_,_,e))        =term_tr' (variant_abs ("s",dummyT,e));
   5.222  
   5.223 -fun com_tr' (Const ("Skip",_))			=Syntax.const "@Skip"
   5.224 -  | com_tr' (Const ("Assign",_) $ v $ e)		=Syntax.const "@Assign" $ Syntax.free (pvar2pvarID v) $ exp_tr' e
   5.225 -  | com_tr' (Const ("Seq",_) $ c $ c')		=Syntax.const "@Seq" $ com_tr' c $ com_tr' c'
   5.226 -  | com_tr' (Const ("Cond",_) $ b $ c $ c')		=Syntax.const "@If" $ bexp_tr' b $ com_tr' c $ com_tr' c'
   5.227 -  | com_tr' (Const ("While",_) $ b $ inv $ c)	=Syntax.const "@While" $ bexp_tr' b $ bexp_tr' inv $ com_tr' c;
   5.228 +fun com_tr' (Const ("Skip",_))                  =Syntax.const "@Skip"
   5.229 +  | com_tr' (Const ("Assign",_) $ v $ e)                =Syntax.const "@Assign" $ Syntax.free (pvar2pvarID v) $ exp_tr' e
   5.230 +  | com_tr' (Const ("Seq",_) $ c $ c')          =Syntax.const "@Seq" $ com_tr' c $ com_tr' c'
   5.231 +  | com_tr' (Const ("Cond",_) $ b $ c $ c')             =Syntax.const "@If" $ bexp_tr' b $ com_tr' c $ com_tr' c'
   5.232 +  | com_tr' (Const ("While",_) $ b $ inv $ c)   =Syntax.const "@While" $ bexp_tr' b $ bexp_tr' inv $ com_tr' c;
   5.233  
   5.234 -fun spec_tr' [p,c,q]		=Syntax.const "@Spec" $ bexp_tr' p $ com_tr' c $ bexp_tr' q;
   5.235 +fun spec_tr' [p,c,q]            =Syntax.const "@Spec" $ bexp_tr' p $ com_tr' c $ bexp_tr' q;
   5.236  
   5.237 -val print_translation	=[("Spec",spec_tr')];
   5.238 +val print_translation   =[("Spec",spec_tr')];
     6.1 --- a/src/HOL/IMP/Com.thy	Mon Feb 05 21:27:16 1996 +0100
     6.2 +++ b/src/HOL/IMP/Com.thy	Mon Feb 05 21:29:06 1996 +0100
     6.3 @@ -1,6 +1,6 @@
     6.4 -(*  Title: 	HOL/IMP/Com.thy
     6.5 +(*  Title:      HOL/IMP/Com.thy
     6.6      ID:         $Id$
     6.7 -    Author: 	Heiko Loetzbeyer & Robert Sandner, TUM
     6.8 +    Author:     Heiko Loetzbeyer & Robert Sandner, TUM
     6.9      Copyright   1994 TUM
    6.10  
    6.11  Arithmetic expressions, Boolean expressions, Commands
    6.12 @@ -32,7 +32,7 @@
    6.13  inductive "evala"
    6.14    intrs 
    6.15      N   "<N(n),s> -a-> n"
    6.16 -    X  	"<X(x),s> -a-> s(x)"
    6.17 +    X   "<X(x),s> -a-> s(x)"
    6.18      Op1 "<e,s> -a-> n ==> <Op1 f e,s> -a-> f(n)"
    6.19      Op2 "[| <e0,s> -a-> n0;  <e1,s>  -a-> n1 |] 
    6.20             ==> <Op2 f e0 e1,s> -a-> f n0 n1"
    6.21 @@ -46,11 +46,11 @@
    6.22         | false
    6.23         | ROp  n2n2b aexp aexp
    6.24         | noti bexp
    6.25 -       | andi bexp bexp 	(infixl 60)
    6.26 -       | ori  bexp bexp 	(infixl 60)
    6.27 +       | andi bexp bexp         (infixl 60)
    6.28 +       | ori  bexp bexp         (infixl 60)
    6.29  
    6.30  (** Evaluation of boolean expressions **)
    6.31 -consts evalb	:: "(bexp*state*bool)set"	
    6.32 +consts evalb    :: "(bexp*state*bool)set"       
    6.33         "@evalb" :: [bexp,state,bool] => bool ("<_,_>/ -b-> _"  [0,0,50] 50)
    6.34  
    6.35  translations
    6.36 @@ -61,32 +61,32 @@
    6.37      tru   "<true,s> -b-> True"
    6.38      fls   "<false,s> -b-> False"
    6.39      ROp   "[| <a0,s> -a-> n0; <a1,s> -a-> n1 |] 
    6.40 -	   ==> <ROp f a0 a1,s> -b-> f n0 n1"
    6.41 +           ==> <ROp f a0 a1,s> -b-> f n0 n1"
    6.42      noti  "<b,s> -b-> w ==> <noti(b),s> -b-> (~w)"
    6.43      andi  "[| <b0,s> -b-> w0; <b1,s> -b-> w1 |] 
    6.44            ==> <b0 andi b1,s> -b-> (w0 & w1)"
    6.45      ori   "[| <b0,s> -b-> w0; <b1,s> -b-> w1 |] 
    6.46 -	    ==> <b0 ori b1,s> -b-> (w0 | w1)"
    6.47 +            ==> <b0 ori b1,s> -b-> (w0 | w1)"
    6.48  
    6.49  (** Commands **)
    6.50  
    6.51  datatype
    6.52    com = skip
    6.53 -      | ":="   loc aexp	         (infixl  60)
    6.54 -      | semic  com com	         ("_; _"  [60, 60] 10)
    6.55 -      | whileC bexp com	         ("while _ do _"  60)
    6.56 -      | ifC    bexp com com	 ("ifc _ then _ else _"  60)
    6.57 +      | ":="   loc aexp          (infixl  60)
    6.58 +      | semic  com com           ("_; _"  [60, 60] 10)
    6.59 +      | whileC bexp com          ("while _ do _"  60)
    6.60 +      | ifC    bexp com com      ("ifc _ then _ else _"  60)
    6.61  
    6.62  (** Execution of commands **)
    6.63  consts  evalc    :: "(com*state*state)set"
    6.64          "@evalc" :: [com,state,state] => bool ("<_,_>/ -c-> _" [0,0,50] 50)
    6.65 -	"assign" :: [state,nat,loc] => state  ("_[_'/_]"       [95,0,0] 95)
    6.66 +        "assign" :: [state,nat,loc] => state  ("_[_'/_]"       [95,0,0] 95)
    6.67  
    6.68  translations
    6.69         "<ce,sig> -c-> s" == "(ce,sig,s) : evalc"
    6.70  
    6.71  rules 
    6.72 -	assign_def	"s[m/x] == (%y. if y=x then m else s y)"
    6.73 +        assign_def      "s[m/x] == (%y. if y=x then m else s y)"
    6.74  
    6.75  inductive "evalc"
    6.76    intrs
     7.1 --- a/src/HOL/IMP/Denotation.thy	Mon Feb 05 21:27:16 1996 +0100
     7.2 +++ b/src/HOL/IMP/Denotation.thy	Mon Feb 05 21:29:06 1996 +0100
     7.3 @@ -1,6 +1,6 @@
     7.4 -(*  Title: 	HOL/IMP/Denotation.thy
     7.5 +(*  Title:      HOL/IMP/Denotation.thy
     7.6      ID:         $Id$
     7.7 -    Author: 	Heiko Loetzbeyer & Robert Sandner, TUM
     7.8 +    Author:     Heiko Loetzbeyer & Robert Sandner, TUM
     7.9      Copyright   1994 TUM
    7.10  
    7.11  Denotational semantics of expressions & commands
    7.12 @@ -16,31 +16,31 @@
    7.13    Gamma :: [bexp,com_den] => (com_den => com_den)
    7.14  
    7.15  primrec A aexp
    7.16 -  A_nat	"A(N(n)) = (%s. n)"
    7.17 -  A_loc	"A(X(x)) = (%s. s(x))" 
    7.18 -  A_op1	"A(Op1 f a) = (%s. f(A a s))"
    7.19 -  A_op2	"A(Op2 f a0 a1) = (%s. f (A a0 s) (A a1 s))"
    7.20 +  A_nat "A(N(n)) = (%s. n)"
    7.21 +  A_loc "A(X(x)) = (%s. s(x))" 
    7.22 +  A_op1 "A(Op1 f a) = (%s. f(A a s))"
    7.23 +  A_op2 "A(Op2 f a0 a1) = (%s. f (A a0 s) (A a1 s))"
    7.24  
    7.25  primrec B bexp
    7.26    B_true  "B(true) = (%s. True)"
    7.27    B_false "B(false) = (%s. False)"
    7.28 -  B_op	  "B(ROp f a0 a1) = (%s. f (A a0 s) (A a1 s))" 
    7.29 -  B_not	  "B(noti(b)) = (%s. ~(B b s))"
    7.30 -  B_and	  "B(b0 andi b1) = (%s. (B b0 s) & (B b1 s))"
    7.31 -  B_or	  "B(b0 ori b1) = (%s. (B b0 s) | (B b1 s))"
    7.32 +  B_op    "B(ROp f a0 a1) = (%s. f (A a0 s) (A a1 s))" 
    7.33 +  B_not   "B(noti(b)) = (%s. ~(B b s))"
    7.34 +  B_and   "B(b0 andi b1) = (%s. (B b0 s) & (B b1 s))"
    7.35 +  B_or    "B(b0 ori b1) = (%s. (B b0 s) | (B b1 s))"
    7.36  
    7.37  defs
    7.38 -  Gamma_def	"Gamma b cd ==   
    7.39 -		   (%phi.{st. st : (phi O cd) & B b (fst st)} Un 
    7.40 -	                 {st. st : id & ~B b (fst st)})"
    7.41 +  Gamma_def     "Gamma b cd ==   
    7.42 +                   (%phi.{st. st : (phi O cd) & B b (fst st)} Un 
    7.43 +                         {st. st : id & ~B b (fst st)})"
    7.44  
    7.45  primrec C com
    7.46    C_skip    "C(skip) = id"
    7.47    C_assign  "C(x := a) = {st . snd(st) = fst(st)[A a (fst st)/x]}"
    7.48    C_comp    "C(c0 ; c1) = C(c1) O C(c0)"
    7.49 -  C_if	    "C(ifc b then c0 else c1) =   
    7.50 -		   {st. st:C(c0) & (B b (fst st))} Un 
    7.51 -	           {st. st:C(c1) & ~(B b (fst st))}"
    7.52 +  C_if      "C(ifc b then c0 else c1) =   
    7.53 +                   {st. st:C(c0) & (B b (fst st))} Un 
    7.54 +                   {st. st:C(c1) & ~(B b (fst st))}"
    7.55    C_while   "C(while b do c) = lfp (Gamma b (C c))"
    7.56  
    7.57  end
     8.1 --- a/src/HOL/IMP/Equiv.thy	Mon Feb 05 21:27:16 1996 +0100
     8.2 +++ b/src/HOL/IMP/Equiv.thy	Mon Feb 05 21:29:06 1996 +0100
     8.3 @@ -1,6 +1,6 @@
     8.4 -(*  Title: 	HOL/IMP/Equiv.thy
     8.5 +(*  Title:      HOL/IMP/Equiv.thy
     8.6      ID:         $Id$
     8.7 -    Author: 	Heiko Loetzbeyer & Robert Sandner, TUM
     8.8 +    Author:     Heiko Loetzbeyer & Robert Sandner, TUM
     8.9      Copyright   1994 TUM
    8.10  *)
    8.11  
     9.1 --- a/src/HOL/IMP/Hoare.thy	Mon Feb 05 21:27:16 1996 +0100
     9.2 +++ b/src/HOL/IMP/Hoare.thy	Mon Feb 05 21:29:06 1996 +0100
     9.3 @@ -1,6 +1,6 @@
     9.4 -(*  Title: 	HOL/IMP/Hoare.thy
     9.5 +(*  Title:      HOL/IMP/Hoare.thy
     9.6      ID:         $Id$
     9.7 -    Author: 	Tobias Nipkow
     9.8 +    Author:     Tobias Nipkow
     9.9      Copyright   1995 TUM
    9.10  
    9.11  Inductive definition of Hoare logic
    9.12 @@ -27,8 +27,8 @@
    9.13    hoare_if   "[| {{%s. P s & B b s}}c{{Q}}; {{%s. P s & ~B b s}}d{{Q}} |] ==>
    9.14                {{P}} ifc b then c else d {{Q}}"
    9.15    hoare_while "[| {{%s. P s & B b s}} c {{P}} |] ==>
    9.16 -	       {{P}} while b do c {{%s. P s & ~B b s}}"
    9.17 +               {{P}} while b do c {{%s. P s & ~B b s}}"
    9.18    hoare_conseq "[| !s. P' s --> P s; {{P}}c{{Q}}; !s. Q s --> Q' s |] ==>
    9.19 -		{{P'}}c{{Q'}}"
    9.20 +                {{P'}}c{{Q'}}"
    9.21  
    9.22  end
    10.1 --- a/src/HOL/IMP/VC.thy	Mon Feb 05 21:27:16 1996 +0100
    10.2 +++ b/src/HOL/IMP/VC.thy	Mon Feb 05 21:29:06 1996 +0100
    10.3 @@ -1,6 +1,6 @@
    10.4 -(*  Title: 	HOL/IMP/VC.thy
    10.5 +(*  Title:      HOL/IMP/VC.thy
    10.6      ID:         $Id$
    10.7 -    Author: 	Tobias Nipkow
    10.8 +    Author:     Tobias Nipkow
    10.9      Copyright   1996 TUM
   10.10  
   10.11  acom: annotated commands
    11.1 --- a/src/HOL/IOA/ABP/Abschannel.thy	Mon Feb 05 21:27:16 1996 +0100
    11.2 +++ b/src/HOL/IOA/ABP/Abschannel.thy	Mon Feb 05 21:29:06 1996 +0100
    11.3 @@ -56,8 +56,8 @@
    11.4        case fst(snd(tr))                                        
    11.5          of S(b) => ((t = s) | (t = s @ [b]))  |                
    11.6             R(b) => s ~= [] &                                   
    11.7 -	            b = hd(s) &                                 
    11.8 -	            ((t = s) | (t = tl(s)))    }"
    11.9 +                    b = hd(s) &                                 
   11.10 +                    ((t = s) | (t = tl(s)))    }"
   11.11    
   11.12  ch_ioa_def "ch_ioa == (ch_asig, {[]}, ch_trans)"
   11.13  
   11.14 @@ -66,24 +66,24 @@
   11.15   *********************************************************)
   11.16    
   11.17  rsch_actions_def "rsch_actions (akt) ==                      
   11.18 -	    case akt of   
   11.19 +            case akt of   
   11.20             Next    =>  None |          
   11.21             S_msg(m) => None |         
   11.22 -	    R_msg(m) => None |         
   11.23 +            R_msg(m) => None |         
   11.24             S_pkt(packet) => None |    
   11.25 -	    R_pkt(packet) => None |    
   11.26 -	    S_ack(b) => Some(S(b)) |   
   11.27 -	    R_ack(b) => Some(R(b))"
   11.28 +            R_pkt(packet) => None |    
   11.29 +            S_ack(b) => Some(S(b)) |   
   11.30 +            R_ack(b) => Some(R(b))"
   11.31  
   11.32  srch_actions_def "srch_actions (akt) ==                      
   11.33 -	    case akt of   
   11.34 -	    Next    =>  None |          
   11.35 +            case akt of   
   11.36 +            Next    =>  None |          
   11.37             S_msg(m) => None |         
   11.38 -	    R_msg(m) => None |         
   11.39 +            R_msg(m) => None |         
   11.40             S_pkt(p) => Some(S(p)) |   
   11.41 -	    R_pkt(p) => Some(R(p)) |   
   11.42 -	    S_ack(b) => None |         
   11.43 -	    R_ack(b) => None"
   11.44 +            R_pkt(p) => Some(R(p)) |   
   11.45 +            S_ack(b) => None |         
   11.46 +            R_ack(b) => None"
   11.47  
   11.48  
   11.49  end  
    12.1 --- a/src/HOL/IOA/ABP/Abschannel_finite.thy	Mon Feb 05 21:27:16 1996 +0100
    12.2 +++ b/src/HOL/IOA/ABP/Abschannel_finite.thy	Mon Feb 05 21:29:06 1996 +0100
    12.3 @@ -54,8 +54,8 @@
    12.4          of S(b) => ((t = s) |                                    
    12.5                     (if (b=hd(reverse(s)) & s~=[]) then  t=s else  t=s@[b])) |    
    12.6             R(b) => s ~= [] &                                   
    12.7 -	            b = hd(s) &                                 
    12.8 -	            ((t = s) | (t = tl(s)))    }"
    12.9 +                    b = hd(s) &                                 
   12.10 +                    ((t = s) | (t = tl(s)))    }"
   12.11    
   12.12  ch_fin_ioa_def "ch_fin_ioa == (ch_fin_asig, {[]}, ch_fin_trans)"
   12.13  
    13.1 --- a/src/HOL/IOA/ABP/Correctness.thy	Mon Feb 05 21:27:16 1996 +0100
    13.2 +++ b/src/HOL/IOA/ABP/Correctness.thy	Mon Feb 05 21:29:06 1996 +0100
    13.3 @@ -20,11 +20,11 @@
    13.4    reduce List.list  
    13.5    reduce_Nil  "reduce [] = []"
    13.6    reduce_Cons "reduce(x#xs) =   
    13.7 -	         (case xs of   
    13.8 -	             [] => [x]   
    13.9 -	       |   y#ys => (if (x=y)   
   13.10 -	                      then reduce xs   
   13.11 -	                      else (x#(reduce xs))))"
   13.12 +                 (case xs of   
   13.13 +                     [] => [x]   
   13.14 +               |   y#ys => (if (x=y)   
   13.15 +                              then reduce xs   
   13.16 +                              else (x#(reduce xs))))"
   13.17  
   13.18    
   13.19  defs
   13.20 @@ -36,8 +36,8 @@
   13.21    "system_fin_ioa == (env_ioa || impl_fin_ioa)"
   13.22    
   13.23  abs_def "abs  ==   
   13.24 -	(%p.(fst(p),(fst(snd(p)),(fst(snd(snd(p))),   
   13.25 -	 (reduce(fst(snd(snd(snd(p))))),reduce(snd(snd(snd(snd(p))))))))))"
   13.26 +        (%p.(fst(p),(fst(snd(p)),(fst(snd(snd(p))),   
   13.27 +         (reduce(fst(snd(snd(snd(p))))),reduce(snd(snd(snd(snd(p))))))))))"
   13.28  
   13.29  rules
   13.30  
    14.1 --- a/src/HOL/IOA/ABP/Receiver.thy	Mon Feb 05 21:27:16 1996 +0100
    14.2 +++ b/src/HOL/IOA/ABP/Receiver.thy	Mon Feb 05 21:29:06 1996 +0100
    14.3 @@ -41,13 +41,13 @@
    14.4        Next    =>  False |     
    14.5        S_msg(m) => False |                                               
    14.6        R_msg(m) => (rq(s) ~= [])  &                                     
    14.7 -		   m = hd(rq(s))  &                             
    14.8 -		   rq(t) = tl(rq(s))   &                              
    14.9 +                   m = hd(rq(s))  &                             
   14.10 +                   rq(t) = tl(rq(s))   &                              
   14.11                    rbit(t)=rbit(s)  |                                 
   14.12        S_pkt(pkt) => False |                                          
   14.13        R_pkt(pkt) => if (hdr(pkt) ~= rbit(s))&rq(s)=[] then            
   14.14 -		         rq(t) = (rq(s)@[msg(pkt)]) &rbit(t) = (~rbit(s)) else  
   14.15 -		         rq(t) =rq(s) & rbit(t)=rbit(s)  |   
   14.16 +                         rq(t) = (rq(s)@[msg(pkt)]) &rbit(t) = (~rbit(s)) else  
   14.17 +                         rq(t) =rq(s) & rbit(t)=rbit(s)  |   
   14.18        S_ack(b) => b = rbit(s)                        &               
   14.19                        rq(t) = rq(s)                    &             
   14.20                        rbit(t)=rbit(s) |                              
    15.1 --- a/src/HOL/IOA/ABP/Sender.thy	Mon Feb 05 21:27:16 1996 +0100
    15.2 +++ b/src/HOL/IOA/ABP/Sender.thy	Mon Feb 05 21:29:06 1996 +0100
    15.3 @@ -41,15 +41,15 @@
    15.4                    sbit(t)=sbit(s)  |                                 
    15.5        R_msg(m) => False |                                            
    15.6        S_pkt(pkt) => sq(s) ~= []  &                                   
    15.7 -		     hdr(pkt) = sbit(s)      &                        
    15.8 +                     hdr(pkt) = sbit(s)      &                        
    15.9                      msg(pkt) = hd(sq(s))    &                   
   15.10                      sq(t) = sq(s)           &                        
   15.11                      sbit(t) = sbit(s) |                              
   15.12        R_pkt(pkt) => False |                                          
   15.13        S_ack(b)   => False |                                          
   15.14        R_ack(b)   => if b = sbit(s) then                              
   15.15 -		     sq(t)=tl(sq(s)) & sbit(t)=(~sbit(s)) else   
   15.16 -		     sq(t)=sq(s) & sbit(t)=sbit(s)}"
   15.17 +                     sq(t)=tl(sq(s)) & sbit(t)=(~sbit(s)) else   
   15.18 +                     sq(t)=sq(s) & sbit(t)=sbit(s)}"
   15.19  
   15.20  sender_ioa_def "sender_ioa == 
   15.21   (sender_asig, {([],True)}, sender_trans)"
    16.1 --- a/src/HOL/IOA/NTP/Abschannel.thy	Mon Feb 05 21:27:16 1996 +0100
    16.2 +++ b/src/HOL/IOA/NTP/Abschannel.thy	Mon Feb 05 21:29:06 1996 +0100
    16.3 @@ -57,26 +57,26 @@
    16.4  
    16.5  
    16.6  rsch_actions_def "rsch_actions (act) ==        
    16.7 -	    case act of                
    16.8 +            case act of                
    16.9             S_msg(m) => None |         
   16.10 -	    R_msg(m) => None |         
   16.11 +            R_msg(m) => None |         
   16.12             S_pkt(packet) => None |    
   16.13 -	    R_pkt(packet) => None |    
   16.14 -	    S_ack(b) => Some(S(b)) |   
   16.15 -	    R_ack(b) => Some(R(b)) |   
   16.16 +            R_pkt(packet) => None |    
   16.17 +            S_ack(b) => Some(S(b)) |   
   16.18 +            R_ack(b) => Some(R(b)) |   
   16.19             C_m_s =>  None  |          
   16.20             C_m_r =>  None |           
   16.21             C_r_s =>  None  |          
   16.22             C_r_r(m) => None"
   16.23  
   16.24  srch_actions_def "srch_actions (act) ==         
   16.25 -	    case act of                
   16.26 +            case act of                
   16.27             S_msg(m) => None |         
   16.28 -	    R_msg(m) => None |         
   16.29 +            R_msg(m) => None |         
   16.30             S_pkt(p) => Some(S(p)) |   
   16.31 -	    R_pkt(p) => Some(R(p)) |   
   16.32 -	    S_ack(b) => None |         
   16.33 -	    R_ack(b) => None |         
   16.34 +            R_pkt(p) => Some(R(p)) |   
   16.35 +            S_ack(b) => None |         
   16.36 +            R_ack(b) => None |         
   16.37             C_m_s => None |            
   16.38             C_m_r => None |            
   16.39             C_r_s => None |            
    17.1 --- a/src/HOL/IOA/meta_theory/IOA.thy	Mon Feb 05 21:27:16 1996 +0100
    17.2 +++ b/src/HOL/IOA/meta_theory/IOA.thy	Mon Feb 05 21:29:06 1996 +0100
    17.3 @@ -22,7 +22,7 @@
    17.4    asig_of    ::"('action,'state)ioa => 'action signature"
    17.5    starts_of  ::"('action,'state)ioa => 'state set"
    17.6    trans_of   ::"('action,'state)ioa => ('action,'state)transition set"
    17.7 -  IOA	     ::"('action,'state)ioa => bool"
    17.8 +  IOA        ::"('action,'state)ioa => bool"
    17.9  
   17.10    (* Executions, schedules, and traces *)
   17.11  
    18.1 --- a/src/HOL/Integ/Equiv.thy	Mon Feb 05 21:27:16 1996 +0100
    18.2 +++ b/src/HOL/Integ/Equiv.thy	Mon Feb 05 21:29:06 1996 +0100
    18.3 @@ -1,7 +1,7 @@
    18.4 -(*  Title: 	Equiv.thy
    18.5 +(*  Title:      Equiv.thy
    18.6      ID:         $Id$
    18.7 -    Authors: 	Riccardo Mattolini, Dip. Sistemi e Informatica
    18.8 -        	Lawrence C Paulson, Cambridge University Computer Laboratory
    18.9 +    Authors:    Riccardo Mattolini, Dip. Sistemi e Informatica
   18.10 +                Lawrence C Paulson, Cambridge University Computer Laboratory
   18.11      Copyright   1994 Universita' di Firenze
   18.12      Copyright   1993  University of Cambridge
   18.13  
   18.14 @@ -10,11 +10,11 @@
   18.15  
   18.16  Equiv = Relation +
   18.17  consts
   18.18 -    refl,equiv 	::      "['a set,('a*'a) set]=>bool"
   18.19 +    refl,equiv  ::      "['a set,('a*'a) set]=>bool"
   18.20      sym         ::      "('a*'a) set=>bool"
   18.21      "'/"        ::      "['a set,('a*'a) set]=>'a set set"  (infixl 90) 
   18.22                          (*set of equiv classes*)
   18.23 -    congruent	::	"[('a*'a) set,'a=>'b]=>bool"
   18.24 +    congruent   ::      "[('a*'a) set,'a=>'b]=>bool"
   18.25      congruent2  ::      "[('a*'a) set,['a,'a]=>'b]=>bool"
   18.26  
   18.27  defs
    19.1 --- a/src/HOL/Integ/Integ.thy	Mon Feb 05 21:27:16 1996 +0100
    19.2 +++ b/src/HOL/Integ/Integ.thy	Mon Feb 05 21:29:06 1996 +0100
    19.3 @@ -1,7 +1,7 @@
    19.4 -(*  Title: 	Integ.thy
    19.5 +(*  Title:      Integ.thy
    19.6      ID:         $Id$
    19.7 -    Authors: 	Riccardo Mattolini, Dip. Sistemi e Informatica
    19.8 -        	Lawrence C Paulson, Cambridge University Computer Laboratory
    19.9 +    Authors:    Riccardo Mattolini, Dip. Sistemi e Informatica
   19.10 +                Lawrence C Paulson, Cambridge University Computer Laboratory
   19.11      Copyright   1994 Universita' di Firenze
   19.12      Copyright   1993  University of Cambridge
   19.13  
   19.14 @@ -16,16 +16,16 @@
   19.15    intrel_def
   19.16     "intrel == {p. ? x1 y1 x2 y2. p=((x1::nat,y1),(x2,y2)) & x1+y2 = x2+y1}"
   19.17  
   19.18 -subtype (Integ)
   19.19 -  int = "{x::(nat*nat).True}/intrel"		(Equiv.quotient_def)
   19.20 +typedef (Integ)
   19.21 +  int = "{x::(nat*nat).True}/intrel"            (Equiv.quotient_def)
   19.22  
   19.23  instance
   19.24    int :: {ord, plus, times, minus}
   19.25  
   19.26  consts
   19.27    zNat        :: nat set
   19.28 -  znat	      :: nat => int	   ("$# _" [80] 80)
   19.29 -  zminus      :: int => int	   ("$~ _" [80] 80)
   19.30 +  znat        :: nat => int        ("$# _" [80] 80)
   19.31 +  zminus      :: int => int        ("$~ _" [80] 80)
   19.32    znegative   :: int => bool
   19.33    zmagnitude  :: int => int
   19.34    zdiv,zmod   :: [int,int]=>int  (infixl 70)
   19.35 @@ -37,7 +37,7 @@
   19.36    znat_def    "$# m == Abs_Integ(intrel ^^ {(m,0)})"
   19.37  
   19.38    zminus_def
   19.39 -	"$~ Z == Abs_Integ(UN p:Rep_Integ(Z). split (%x y. intrel^^{(y,x)}) p)"
   19.40 +        "$~ Z == Abs_Integ(UN p:Rep_Integ(Z). split (%x y. intrel^^{(y,x)}) p)"
   19.41  
   19.42    znegative_def
   19.43        "znegative(Z) == EX x y. x<y & (x,y::nat):Rep_Integ(Z)"
    20.1 --- a/src/HOL/Lambda/Commutation.thy	Mon Feb 05 21:27:16 1996 +0100
    20.2 +++ b/src/HOL/Lambda/Commutation.thy	Mon Feb 05 21:29:06 1996 +0100
    20.3 @@ -1,6 +1,6 @@
    20.4 -(*  Title: 	HOL/Lambda/Commutation.thy
    20.5 +(*  Title:      HOL/Lambda/Commutation.thy
    20.6      ID:         $Id$
    20.7 -    Author: 	Tobias Nipkow
    20.8 +    Author:     Tobias Nipkow
    20.9      Copyright   1995  TU Muenchen
   20.10  
   20.11  Abstract commutation and confluence notions.
    21.1 --- a/src/HOL/Lex/Auto.thy	Mon Feb 05 21:27:16 1996 +0100
    21.2 +++ b/src/HOL/Lex/Auto.thy	Mon Feb 05 21:29:06 1996 +0100
    21.3 @@ -1,6 +1,6 @@
    21.4 -(*  Title: 	HOL/Lex/Auto.thy
    21.5 +(*  Title:      HOL/Lex/Auto.thy
    21.6      ID:         $Id$
    21.7 -    Author: 	Tobias Nipkow
    21.8 +    Author:     Tobias Nipkow
    21.9      Copyright   1995 TUM
   21.10  
   21.11  Automata expressed as triples of
    22.1 --- a/src/HOL/Lex/AutoChopper.thy	Mon Feb 05 21:27:16 1996 +0100
    22.2 +++ b/src/HOL/Lex/AutoChopper.thy	Mon Feb 05 21:29:06 1996 +0100
    22.3 @@ -1,6 +1,6 @@
    22.4 -(*  Title: 	HOL/Lex/AutoChopper.thy
    22.5 +(*  Title:      HOL/Lex/AutoChopper.thy
    22.6      ID:         $Id$
    22.7 -    Author: 	Tobias Nipkow
    22.8 +    Author:     Tobias Nipkow
    22.9      Copyright   1995 TUM
   22.10  
   22.11  auto_chopper turns an automaton into a chopper. Tricky, because primrec.
   22.12 @@ -20,19 +20,19 @@
   22.13    is_auto_chopper :: (('a,'b)auto => 'a chopper) => bool
   22.14    auto_chopper :: ('a,'b)auto => 'a chopper
   22.15    acc :: "['a list, 'b, 'a list, 'a list, 'a list list*'a list, ('a,'b)auto]
   22.16 -	  => 'a list list * 'a list"
   22.17 +          => 'a list list * 'a list"
   22.18  
   22.19  defs
   22.20    is_auto_chopper_def "is_auto_chopper(chopperf) ==
   22.21 -		       !A. is_longest_prefix_chopper(accepts A)(chopperf A)"
   22.22 +                       !A. is_longest_prefix_chopper(accepts A)(chopperf A)"
   22.23  
   22.24    auto_chopper_def "auto_chopper A xs == acc xs (start A) [] [] ([],xs) A"
   22.25  
   22.26  primrec acc List.list
   22.27    acc_Nil  "acc [] st ys zs chopsr A =
   22.28 -	      (if ys=[] then chopsr else (ys#fst(chopsr),snd(chopsr)))" 
   22.29 +              (if ys=[] then chopsr else (ys#fst(chopsr),snd(chopsr)))" 
   22.30    acc_Cons "acc(x#xs) st ys zs chopsr A =
   22.31 -	    (let s0 = start(A); nxt = next(A); fin = fin(A)
   22.32 +            (let s0 = start(A); nxt = next(A); fin = fin(A)
   22.33               in if fin(nxt st x)
   22.34                  then acc xs (nxt st x) (zs@[x]) (zs@[x])
   22.35                           (acc xs s0 [] [] ([],xs) A) A
    23.1 --- a/src/HOL/Lex/Chopper.thy	Mon Feb 05 21:27:16 1996 +0100
    23.2 +++ b/src/HOL/Lex/Chopper.thy	Mon Feb 05 21:29:06 1996 +0100
    23.3 @@ -1,6 +1,6 @@
    23.4 -(*  Title: 	HOL/Lex/Chopper.thy
    23.5 +(*  Title:      HOL/Lex/Chopper.thy
    23.6      ID:         $Id$
    23.7 -    Author: 	Tobias Nipkow
    23.8 +    Author:     Tobias Nipkow
    23.9      Copyright   1995 TUM
   23.10  
   23.11  A 'chopper' is a function which returns
   23.12 @@ -25,10 +25,10 @@
   23.13  defs
   23.14    is_longest_prefix_chopper_def
   23.15      "is_longest_prefix_chopper L chopper == !xs.   \
   23.16 -\	 (!zs. chopper(xs) = ([],zs) --> \
   23.17 -\	       zs=xs & (!ys. ys ~= [] & ys <= xs --> ~L(ys))) &  \
   23.18 -\ 	 (!ys yss zs. chopper(xs) = (ys#yss,zs) -->                \
   23.19 -\	    ys ~= [] & L(ys) & xs=ys@flat(yss)@zs &   \
   23.20 +\        (!zs. chopper(xs) = ([],zs) --> \
   23.21 +\              zs=xs & (!ys. ys ~= [] & ys <= xs --> ~L(ys))) &  \
   23.22 +\        (!ys yss zs. chopper(xs) = (ys#yss,zs) -->                \
   23.23 +\           ys ~= [] & L(ys) & xs=ys@flat(yss)@zs &   \
   23.24  \           chopper(flat(yss)@zs) = (yss,zs) &     \
   23.25  \           (!as. as <= xs & ys <= as & ys ~= as --> ~L(as)))"
   23.26  end
    24.1 --- a/src/HOL/Lex/Prefix.thy	Mon Feb 05 21:27:16 1996 +0100
    24.2 +++ b/src/HOL/Lex/Prefix.thy	Mon Feb 05 21:29:06 1996 +0100
    24.3 @@ -1,6 +1,6 @@
    24.4 -(*  Title: 	HOL/Lex/Prefix.thy
    24.5 +(*  Title:      HOL/Lex/Prefix.thy
    24.6      ID:         $Id$
    24.7 -    Author: 	Tobias Nipkow
    24.8 +    Author:     Tobias Nipkow
    24.9      Copyright   1995 TUM
   24.10  *)
   24.11  
   24.12 @@ -9,5 +9,5 @@
   24.13  arities list :: (term)ord
   24.14  
   24.15  defs
   24.16 -	prefix_def     "xs <= zs  ==  ? ys. zs = xs@ys"
   24.17 +        prefix_def     "xs <= zs  ==  ? ys. zs = xs@ys"
   24.18  end
    25.1 --- a/src/HOL/MiniML/I.thy	Mon Feb 05 21:27:16 1996 +0100
    25.2 +++ b/src/HOL/MiniML/I.thy	Mon Feb 05 21:29:06 1996 +0100
    25.3 @@ -8,16 +8,16 @@
    25.4  I = W +
    25.5  
    25.6  consts
    25.7 -	I :: [expr, typ list, nat, subst] => result_W
    25.8 +        I :: [expr, typ list, nat, subst] => result_W
    25.9  
   25.10  primrec I expr
   25.11 -        I_Var	"I (Var i) a n s = (if i < length a then Ok(s, nth i a, n)
   25.12 +        I_Var   "I (Var i) a n s = (if i < length a then Ok(s, nth i a, n)
   25.13                                      else Fail)"
   25.14 -        I_Abs	"I (Abs e) a n s = ( (s,t,m) := I e ((TVar n)#a) (Suc n) s;
   25.15 +        I_Abs   "I (Abs e) a n s = ( (s,t,m) := I e ((TVar n)#a) (Suc n) s;
   25.16                                       Ok(s, TVar n -> t, m) )"
   25.17 -        I_App	"I (App e1 e2) a n s =
   25.18 - 		   ( (s1,t1,m1) := I e1 a n s;
   25.19 -		     (s2,t2,m2) := I e2 a m1 s1;
   25.20 -		     u := mgu ($s2 t1) ($s2 t2 -> TVar m2);
   25.21 -		     Ok($u o s2, TVar m2, Suc m2) )"
   25.22 +        I_App   "I (App e1 e2) a n s =
   25.23 +                   ( (s1,t1,m1) := I e1 a n s;
   25.24 +                     (s2,t2,m2) := I e2 a m1 s1;
   25.25 +                     u := mgu ($s2 t1) ($s2 t2 -> TVar m2);
   25.26 +                     Ok($u o s2, TVar m2, Suc m2) )"
   25.27  end
    26.1 --- a/src/HOL/MiniML/MiniML.thy	Mon Feb 05 21:27:16 1996 +0100
    26.2 +++ b/src/HOL/MiniML/MiniML.thy	Mon Feb 05 21:29:06 1996 +0100
    26.3 @@ -10,11 +10,11 @@
    26.4  
    26.5  (* expressions *)
    26.6  datatype
    26.7 -	expr = Var nat | Abs expr | App expr expr
    26.8 +        expr = Var nat | Abs expr | App expr expr
    26.9  
   26.10  (* type inference rules *)
   26.11  consts
   26.12 -	has_type :: "(typ list * expr * typ)set"
   26.13 +        has_type :: "(typ list * expr * typ)set"
   26.14  syntax
   26.15          "@has_type" :: [typ list, expr, typ] => bool
   26.16                         ("((_) |-/ (_) :: (_))" 60)
   26.17 @@ -23,10 +23,10 @@
   26.18  
   26.19  inductive "has_type"
   26.20  intrs
   26.21 -	VarI "[| n < length a |] ==> a |- Var n :: nth n a"
   26.22 -	AbsI "[| t1#a |- e :: t2 |] ==> a |- Abs e :: t1 -> t2"
   26.23 -	AppI "[| a |- e1 :: t2 -> t1; a |- e2 :: t2 |] 
   26.24 -     	      ==> a |- App e1 e2 :: t1"
   26.25 +        VarI "[| n < length a |] ==> a |- Var n :: nth n a"
   26.26 +        AbsI "[| t1#a |- e :: t2 |] ==> a |- Abs e :: t1 -> t2"
   26.27 +        AppI "[| a |- e1 :: t2 -> t1; a |- e2 :: t2 |] 
   26.28 +              ==> a |- App e1 e2 :: t1"
   26.29  
   26.30  end
   26.31  
    27.1 --- a/src/HOL/MiniML/Type.thy	Mon Feb 05 21:27:16 1996 +0100
    27.2 +++ b/src/HOL/MiniML/Type.thy	Mon Feb 05 21:29:06 1996 +0100
    27.3 @@ -10,81 +10,81 @@
    27.4  
    27.5  (* new class for structures containing type variables *)
    27.6  classes
    27.7 -	type_struct < term 
    27.8 +        type_struct < term 
    27.9  
   27.10  (* type expressions *)
   27.11  datatype
   27.12 -	typ = TVar nat | "->" typ typ (infixr 70)
   27.13 +        typ = TVar nat | "->" typ typ (infixr 70)
   27.14  
   27.15  (* type variable substitution *)
   27.16  types
   27.17 -	subst = nat => typ
   27.18 +        subst = nat => typ
   27.19  
   27.20  arities
   27.21 -	typ::type_struct
   27.22 -	list::(type_struct)type_struct
   27.23 -	fun::(term,type_struct)type_struct
   27.24 +        typ::type_struct
   27.25 +        list::(type_struct)type_struct
   27.26 +        fun::(term,type_struct)type_struct
   27.27  
   27.28  (* substitutions *)
   27.29  
   27.30  (* identity *)
   27.31  consts
   27.32 -	id_subst :: subst
   27.33 +        id_subst :: subst
   27.34  defs
   27.35 -	id_subst_def "id_subst == (%n.TVar n)"
   27.36 +        id_subst_def "id_subst == (%n.TVar n)"
   27.37  
   27.38  (* extension of substitution to type structures *)
   27.39  consts
   27.40 -	app_subst :: [subst, 'a::type_struct] => 'a::type_struct ("$")
   27.41 +        app_subst :: [subst, 'a::type_struct] => 'a::type_struct ("$")
   27.42  
   27.43  rules
   27.44 -	app_subst_TVar  "$ s (TVar n) = s n" 
   27.45 -	app_subst_Fun	"$ s (t1 -> t2) = ($ s t1) -> ($ s t2)" 
   27.46 +        app_subst_TVar  "$ s (TVar n) = s n" 
   27.47 +        app_subst_Fun   "$ s (t1 -> t2) = ($ s t1) -> ($ s t2)" 
   27.48  defs
   27.49 -        app_subst_list	"$ s == map ($ s)"
   27.50 +        app_subst_list  "$ s == map ($ s)"
   27.51    
   27.52  (* free_tv s: the type variables occuring freely in the type structure s *)
   27.53  consts
   27.54 -	free_tv :: ['a::type_struct] => nat set
   27.55 +        free_tv :: ['a::type_struct] => nat set
   27.56  
   27.57  rules
   27.58 -	free_tv_TVar	"free_tv (TVar m) = {m}"
   27.59 -	free_tv_Fun	"free_tv (t1 -> t2) = (free_tv t1) Un (free_tv t2)"
   27.60 -	free_tv_Nil	"free_tv [] = {}"
   27.61 -	free_tv_Cons	"free_tv (x#l) = (free_tv x) Un (free_tv l)"
   27.62 +        free_tv_TVar    "free_tv (TVar m) = {m}"
   27.63 +        free_tv_Fun     "free_tv (t1 -> t2) = (free_tv t1) Un (free_tv t2)"
   27.64 +        free_tv_Nil     "free_tv [] = {}"
   27.65 +        free_tv_Cons    "free_tv (x#l) = (free_tv x) Un (free_tv l)"
   27.66  
   27.67  (* domain of a substitution *)
   27.68  consts
   27.69 -	dom :: subst => nat set
   27.70 +        dom :: subst => nat set
   27.71  defs
   27.72 -	dom_def 	"dom s == {n. s n ~= TVar n}" 
   27.73 +        dom_def         "dom s == {n. s n ~= TVar n}" 
   27.74  
   27.75  (* codomain of a substitutions: the introduced variables *)
   27.76  consts
   27.77       cod :: subst => nat set
   27.78  defs
   27.79 -	cod_def		"cod s == (UN m:dom s. free_tv (s m))"
   27.80 +        cod_def         "cod s == (UN m:dom s. free_tv (s m))"
   27.81  
   27.82  defs
   27.83 -	free_tv_subst	"free_tv s == (dom s) Un (cod s)"
   27.84 +        free_tv_subst   "free_tv s == (dom s) Un (cod s)"
   27.85  
   27.86  (* new_tv s n computes whether n is a new type variable w.r.t. a type 
   27.87     structure s, i.e. whether n is greater than any type variable 
   27.88     occuring in the type structure *)
   27.89  consts
   27.90 -	new_tv :: [nat,'a::type_struct] => bool
   27.91 +        new_tv :: [nat,'a::type_struct] => bool
   27.92  defs
   27.93          new_tv_def      "new_tv n ts == ! m. m:free_tv ts --> m<n"
   27.94  
   27.95  (* unification algorithm mgu *)
   27.96  consts
   27.97 -	mgu :: [typ,typ] => subst maybe
   27.98 +        mgu :: [typ,typ] => subst maybe
   27.99  rules
  27.100 -	mgu_eq 	 "mgu t1 t2 = Ok u ==> $u t1 = $u t2"
  27.101 -	mgu_mg 	 "[| (mgu t1 t2) = Ok u; $s t1 = $s t2 |] ==>
  27.102 -		  ? r. s = $r o u"
  27.103 -	mgu_Ok	 "$s t1 = $s t2 ==> ? u. mgu t1 t2 = Ok u"
  27.104 -	mgu_free "mgu t1 t2 = Ok u ==> free_tv u <= free_tv t1 Un free_tv t2"
  27.105 +        mgu_eq   "mgu t1 t2 = Ok u ==> $u t1 = $u t2"
  27.106 +        mgu_mg   "[| (mgu t1 t2) = Ok u; $s t1 = $s t2 |] ==>
  27.107 +                  ? r. s = $r o u"
  27.108 +        mgu_Ok   "$s t1 = $s t2 ==> ? u. mgu t1 t2 = Ok u"
  27.109 +        mgu_free "mgu t1 t2 = Ok u ==> free_tv u <= free_tv t1 Un free_tv t2"
  27.110  
  27.111  end
  27.112  
    28.1 --- a/src/HOL/MiniML/W.thy	Mon Feb 05 21:27:16 1996 +0100
    28.2 +++ b/src/HOL/MiniML/W.thy	Mon Feb 05 21:29:06 1996 +0100
    28.3 @@ -13,16 +13,16 @@
    28.4  
    28.5  (* type inference algorithm W *)
    28.6  consts
    28.7 -	W :: [expr, typ list, nat] => result_W
    28.8 +        W :: [expr, typ list, nat] => result_W
    28.9  
   28.10  primrec W expr
   28.11 -  W_Var	"W (Var i) a n = (if i < length a then Ok(id_subst, nth i a, n)
   28.12 -		          else Fail)"
   28.13 -  W_Abs	"W (Abs e) a n = ( (s,t,m) := W e ((TVar n)#a) (Suc n);
   28.14 -		           Ok(s, (s n) -> t, m) )"
   28.15 -  W_App	"W (App e1 e2) a n =
   28.16 - 		 ( (s1,t1,m1) := W e1 a n;
   28.17 -		   (s2,t2,m2) := W e2 ($s1 a) m1;
   28.18 -		   u := mgu ($s2 t1) (t2 -> (TVar m2));
   28.19 -		   Ok( $u o $s2 o s1, $u (TVar m2), Suc m2) )"
   28.20 +  W_Var "W (Var i) a n = (if i < length a then Ok(id_subst, nth i a, n)
   28.21 +                          else Fail)"
   28.22 +  W_Abs "W (Abs e) a n = ( (s,t,m) := W e ((TVar n)#a) (Suc n);
   28.23 +                           Ok(s, (s n) -> t, m) )"
   28.24 +  W_App "W (App e1 e2) a n =
   28.25 +                 ( (s1,t1,m1) := W e1 a n;
   28.26 +                   (s2,t2,m2) := W e2 ($s1 a) m1;
   28.27 +                   u := mgu ($s2 t1) (t2 -> (TVar m2));
   28.28 +                   Ok( $u o $s2 o s1, $u (TVar m2), Suc m2) )"
   28.29  end
    29.1 --- a/src/HOL/Subst/AList.thy	Mon Feb 05 21:27:16 1996 +0100
    29.2 +++ b/src/HOL/Subst/AList.thy	Mon Feb 05 21:29:06 1996 +0100
    29.3 @@ -1,5 +1,5 @@
    29.4 -(*  Title: 	Substitutions/alist.thy
    29.5 -    Author: 	Martin Coen, Cambridge University Computer Laboratory
    29.6 +(*  Title:      Substitutions/alist.thy
    29.7 +    Author:     Martin Coen, Cambridge University Computer Laboratory
    29.8      Copyright   1993  University of Cambridge
    29.9  
   29.10  Association lists.
    30.1 --- a/src/HOL/Subst/Setplus.thy	Mon Feb 05 21:27:16 1996 +0100
    30.2 +++ b/src/HOL/Subst/Setplus.thy	Mon Feb 05 21:29:06 1996 +0100
    30.3 @@ -1,5 +1,5 @@
    30.4 -(*  Title: 	Substitutions/setplus.thy
    30.5 -    Author: 	Martin Coen, Cambridge University Computer Laboratory
    30.6 +(*  Title:      Substitutions/setplus.thy
    30.7 +    Author:     Martin Coen, Cambridge University Computer Laboratory
    30.8      Copyright   1993  University of Cambridge
    30.9  
   30.10  Minor additions to HOL's set theory
    31.1 --- a/src/HOL/Subst/Subst.thy	Mon Feb 05 21:27:16 1996 +0100
    31.2 +++ b/src/HOL/Subst/Subst.thy	Mon Feb 05 21:29:06 1996 +0100
    31.3 @@ -1,5 +1,5 @@
    31.4 -(*  Title: 	Substitutions/subst.thy
    31.5 -    Author: 	Martin Coen, Cambridge University Computer Laboratory
    31.6 +(*  Title:      Substitutions/subst.thy
    31.7 +    Author:     Martin Coen, Cambridge University Computer Laboratory
    31.8      Copyright   1993  University of Cambridge
    31.9  
   31.10  Substitutions on uterms
   31.11 @@ -22,8 +22,8 @@
   31.12    subst_eq_def  "r =s= s == ALL t.t <| r = t <| s"
   31.13  
   31.14    subst_def    
   31.15 -  "t <| al == uterm_rec t (%x.assoc x (Var x) al)	
   31.16 -                         (%x.Const(x))			
   31.17 +  "t <| al == uterm_rec t (%x.assoc x (Var x) al)       
   31.18 +                         (%x.Const(x))                  
   31.19                           (%u v q r.Comb q r)"
   31.20  
   31.21    comp_def    "al <> bl == alist_rec al bl (%x y xs g.(x,y <| bl)#g)"
    32.1 --- a/src/HOL/Subst/UTLemmas.thy	Mon Feb 05 21:27:16 1996 +0100
    32.2 +++ b/src/HOL/Subst/UTLemmas.thy	Mon Feb 05 21:29:06 1996 +0100
    32.3 @@ -1,5 +1,5 @@
    32.4 -(*  Title: 	Substitutions/utermlemmas.thy
    32.5 -    Author: 	Martin Coen, Cambridge University Computer Laboratory
    32.6 +(*  Title:      Substitutions/utermlemmas.thy
    32.7 +    Author:     Martin Coen, Cambridge University Computer Laboratory
    32.8      Copyright   1993  University of Cambridge
    32.9  
   32.10  Additional definitions for uterms that are not part of the basic inductive definition.
    33.1 --- a/src/HOL/Subst/UTerm.ML	Mon Feb 05 21:27:16 1996 +0100
    33.2 +++ b/src/HOL/Subst/UTerm.ML	Mon Feb 05 21:29:06 1996 +0100
    33.3 @@ -206,8 +206,18 @@
    33.4  
    33.5  (*** UTerm_rec -- by wf recursion on pred_sexp ***)
    33.6  
    33.7 -val UTerm_rec_unfold =
    33.8 -    [UTerm_rec_def, wf_pred_sexp RS wf_trancl] MRS def_wfrec;
    33.9 +goal UTerm.thy
   33.10 +   "(%M. UTerm_rec M b c d) = wfrec (trancl pred_sexp) \
   33.11 +   \ (%g. Case (%x.b(x)) (Case (%y. c(y)) (Split (%x y. d x y (g x) (g y)))))";
   33.12 +by (simp_tac (HOL_ss addsimps [UTerm_rec_def]) 1);
   33.13 +bind_thm("UTerm_rec_unfold", (wf_pred_sexp RS wf_trancl) RS 
   33.14 +                            ((result() RS eq_reflection) RS def_wfrec));
   33.15 +
   33.16 +(*---------------------------------------------------------------------------
   33.17 + * Old:
   33.18 + * val UTerm_rec_unfold =
   33.19 + *   [UTerm_rec_def, wf_pred_sexp RS wf_trancl] MRS def_wfrec;
   33.20 + *---------------------------------------------------------------------------*)
   33.21  
   33.22  (** conversion rules **)
   33.23  
    34.1 --- a/src/HOL/Subst/UTerm.thy	Mon Feb 05 21:27:16 1996 +0100
    34.2 +++ b/src/HOL/Subst/UTerm.thy	Mon Feb 05 21:29:06 1996 +0100
    34.3 @@ -1,8 +1,8 @@
    34.4 -(*  Title: 	Substitutions/UTerm.thy
    34.5 -    Author: 	Martin Coen, Cambridge University Computer Laboratory
    34.6 +(*  Title:      Substitutions/UTerm.thy
    34.7 +    Author:     Martin Coen, Cambridge University Computer Laboratory
    34.8      Copyright   1993  University of Cambridge
    34.9  
   34.10 -Simple term structure for unifiation.
   34.11 +Simple term structure for unification.
   34.12  Binary trees with leaves that are constants or variables.
   34.13  *)
   34.14  
   34.15 @@ -30,32 +30,32 @@
   34.16  
   34.17  defs
   34.18       (*defining the concrete constructors*)
   34.19 -  VAR_def  	"VAR(v) == In0(v)"
   34.20 -  CONST_def  	"CONST(v) == In1(In0(v))"
   34.21 -  COMB_def 	"COMB t u == In1(In1(t $ u))"
   34.22 +  VAR_def       "VAR(v) == In0(v)"
   34.23 +  CONST_def     "CONST(v) == In1(In0(v))"
   34.24 +  COMB_def      "COMB t u == In1(In1(t $ u))"
   34.25  
   34.26  inductive "uterm(A)"
   34.27    intrs
   34.28 -    VAR_I	   "v:A ==> VAR(v) : uterm(A)"
   34.29 +    VAR_I          "v:A ==> VAR(v) : uterm(A)"
   34.30      CONST_I  "c:A ==> CONST(c) : uterm(A)"
   34.31      COMB_I   "[| M:uterm(A);  N:uterm(A) |] ==> COMB M N : uterm(A)"
   34.32  
   34.33  rules
   34.34      (*faking a type definition...*)
   34.35 -  Rep_uterm 		"Rep_uterm(xs): uterm(range(Leaf))"
   34.36 -  Rep_uterm_inverse 	"Abs_uterm(Rep_uterm(xs)) = xs"
   34.37 -  Abs_uterm_inverse 	"M: uterm(range(Leaf)) ==> Rep_uterm(Abs_uterm(M)) = M"
   34.38 +  Rep_uterm             "Rep_uterm(xs): uterm(range(Leaf))"
   34.39 +  Rep_uterm_inverse     "Abs_uterm(Rep_uterm(xs)) = xs"
   34.40 +  Abs_uterm_inverse     "M: uterm(range(Leaf)) ==> Rep_uterm(Abs_uterm(M)) = M"
   34.41  
   34.42  defs
   34.43       (*defining the abstract constructors*)
   34.44 -  Var_def  	"Var(v) == Abs_uterm(VAR(Leaf(v)))"
   34.45 -  Const_def  	"Const(c) == Abs_uterm(CONST(Leaf(c)))"
   34.46 -  Comb_def 	"Comb t u == Abs_uterm (COMB (Rep_uterm t) (Rep_uterm u))"
   34.47 +  Var_def       "Var(v) == Abs_uterm(VAR(Leaf(v)))"
   34.48 +  Const_def     "Const(c) == Abs_uterm(CONST(Leaf(c)))"
   34.49 +  Comb_def      "Comb t u == Abs_uterm (COMB (Rep_uterm t) (Rep_uterm u))"
   34.50  
   34.51       (*uterm recursion*)
   34.52 -  UTerm_rec_def	
   34.53 -   "UTerm_rec M b c d == wfrec (trancl pred_sexp) M 
   34.54 -          (Case (%x g.b(x)) (Case (%y g. c(y)) (Split (%x y g. d x y (g x) (g y)))))"
   34.55 +  UTerm_rec_def 
   34.56 +   "UTerm_rec M b c d == wfrec (trancl pred_sexp) 
   34.57 +    (%g. Case (%x.b(x)) (Case (%y. c(y)) (Split (%x y. d x y (g x) (g y))))) M"
   34.58  
   34.59    uterm_rec_def
   34.60     "uterm_rec t b c d == 
    35.1 --- a/src/HOL/Subst/Unifier.thy	Mon Feb 05 21:27:16 1996 +0100
    35.2 +++ b/src/HOL/Subst/Unifier.thy	Mon Feb 05 21:29:06 1996 +0100
    35.3 @@ -1,5 +1,5 @@
    35.4 -(*  Title: 	Subst/unifier.thy
    35.5 -    Author: 	Martin Coen, Cambridge University Computer Laboratory
    35.6 +(*  Title:      Subst/unifier.thy
    35.7 +    Author:     Martin Coen, Cambridge University Computer Laboratory
    35.8      Copyright   1993  University of Cambridge
    35.9  
   35.10  Definition of most general idempotent unifier
   35.11 @@ -22,7 +22,7 @@
   35.12    Unifier_def      "Unifier s t u == t <| s = u <| s"
   35.13    MoreGeneral_def  "r >> s == ? q.s =s= r <> q"
   35.14    MGUnifier_def    "MGUnifier s t u == Unifier s t u & 
   35.15 -		    (! r.Unifier r t u --> s >> r)"
   35.16 +                    (! r.Unifier r t u --> s >> r)"
   35.17    MGIUnifier_def   "MGIUnifier s t u == MGUnifier s t u & Idem(s)"
   35.18  
   35.19    UWFD_def
    36.1 --- a/src/HOL/ex/Acc.thy	Mon Feb 05 21:27:16 1996 +0100
    36.2 +++ b/src/HOL/ex/Acc.thy	Mon Feb 05 21:29:06 1996 +0100
    36.3 @@ -1,6 +1,6 @@
    36.4 -(*  Title: 	HOL/ex/Acc.thy
    36.5 +(*  Title:      HOL/ex/Acc.thy
    36.6      ID:         $Id$
    36.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    36.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    36.9      Copyright   1994  University of Cambridge
   36.10  
   36.11  Inductive definition of acc(r)
   36.12 @@ -12,8 +12,8 @@
   36.13  Acc = WF + 
   36.14  
   36.15  consts
   36.16 -  pred :: "['b, ('a * 'b)set] => 'a set"	(*Set of predecessors*)
   36.17 -  acc  :: "('a * 'a)set => 'a set"		(*Accessible part*)
   36.18 +  pred :: "['b, ('a * 'b)set] => 'a set"        (*Set of predecessors*)
   36.19 +  acc  :: "('a * 'a)set => 'a set"              (*Accessible part*)
   36.20  
   36.21  defs
   36.22    pred_def  "pred x r == {y. (y,x):r}"
    37.1 --- a/src/HOL/ex/BT.thy	Mon Feb 05 21:27:16 1996 +0100
    37.2 +++ b/src/HOL/ex/BT.thy	Mon Feb 05 21:29:06 1996 +0100
    37.3 @@ -1,6 +1,6 @@
    37.4 -(*  Title: 	HOL/ex/BT.thy
    37.5 +(*  Title:      HOL/ex/BT.thy
    37.6      ID:         $Id$
    37.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    37.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    37.9      Copyright   1995  University of Cambridge
   37.10  
   37.11  Binary trees (based on the ZF version)
   37.12 @@ -11,9 +11,9 @@
   37.13  datatype 'a bt = Lf  |  Br 'a ('a bt) ('a bt)
   37.14    
   37.15  consts
   37.16 -    n_nodes	:: 'a bt => nat
   37.17 -    n_leaves   	:: 'a bt => nat
   37.18 -    reflect 	:: 'a bt => 'a bt
   37.19 +    n_nodes     :: 'a bt => nat
   37.20 +    n_leaves    :: 'a bt => nat
   37.21 +    reflect     :: 'a bt => 'a bt
   37.22      bt_map      :: ('a=>'b) => ('a bt => 'b bt)
   37.23      preorder    :: 'a bt => 'a list
   37.24      inorder     :: 'a bt => 'a list
    38.1 --- a/src/HOL/ex/InSort.thy	Mon Feb 05 21:27:16 1996 +0100
    38.2 +++ b/src/HOL/ex/InSort.thy	Mon Feb 05 21:29:06 1996 +0100
    38.3 @@ -1,6 +1,6 @@
    38.4 -(*  Title: 	HOL/ex/insort.thy
    38.5 +(*  Title:      HOL/ex/insort.thy
    38.6      ID:         $Id$
    38.7 -    Author: 	Tobias Nipkow
    38.8 +    Author:     Tobias Nipkow
    38.9      Copyright   1994 TU Muenchen
   38.10  
   38.11  Insertion sort
    39.1 --- a/src/HOL/ex/LList.thy	Mon Feb 05 21:27:16 1996 +0100
    39.2 +++ b/src/HOL/ex/LList.thy	Mon Feb 05 21:29:06 1996 +0100
    39.3 @@ -1,6 +1,6 @@
    39.4 -(*  Title: 	HOL/LList.thy
    39.5 +(*  Title:      HOL/LList.thy
    39.6      ID:         $Id$
    39.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    39.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    39.9      Copyright   1994  University of Cambridge
   39.10  
   39.11  Definition of type 'a llist by a greatest fixed point
   39.12 @@ -18,8 +18,8 @@
   39.13  
   39.14  Previous definition of llistD_Fun was explicit:
   39.15    llistD_Fun_def
   39.16 -   "llistD_Fun(r) == 	
   39.17 -       {(LNil,LNil)}  Un  	
   39.18 +   "llistD_Fun(r) ==    
   39.19 +       {(LNil,LNil)}  Un        
   39.20         (UN x. (split(%l1 l2.(LCons(x,l1),LCons(x,l2))))``r)"
   39.21  *)
   39.22  
   39.23 @@ -52,8 +52,8 @@
   39.24    LList_corec     :: "['a, 'a => unit + ('b item * 'a)] => 'b item"
   39.25    llist_corec     :: "['a, 'a => unit + ('b * 'a)] => 'b llist"
   39.26  
   39.27 -  Lmap	     :: ('a item => 'b item) => ('a item => 'b item)
   39.28 -  lmap	     :: ('a=>'b) => ('a llist => 'b llist)
   39.29 +  Lmap       :: ('a item => 'b item) => ('a item => 'b item)
   39.30 +  lmap       :: ('a=>'b) => ('a llist => 'b llist)
   39.31  
   39.32    iterates   :: ['a => 'a, 'a] => 'a llist
   39.33  
   39.34 @@ -71,21 +71,21 @@
   39.35    intrs
   39.36      NIL_I  "(NIL, NIL) : LListD(r)"
   39.37      CONS_I "[| (a,b): r;  (M,N) : LListD(r)   
   39.38 -	    |] ==> (CONS a M, CONS b N) : LListD(r)"
   39.39 +            |] ==> (CONS a M, CONS b N) : LListD(r)"
   39.40  
   39.41  defs
   39.42    (*Now used exclusively for abbreviating the coinduction rule*)
   39.43    list_Fun_def   "list_Fun A X ==   
   39.44 -		  {z. z = NIL | (? M a. z = CONS a M & a : A & M : X)}"
   39.45 +                  {z. z = NIL | (? M a. z = CONS a M & a : A & M : X)}"
   39.46  
   39.47    LListD_Fun_def "LListD_Fun r X ==   
   39.48 -		  {z. z = (NIL, NIL) |   
   39.49 -		      (? M N a b. z = (CONS a M, CONS b N) &   
   39.50 -		                  (a, b) : r & (M, N) : X)}"
   39.51 +                  {z. z = (NIL, NIL) |   
   39.52 +                      (? M N a b. z = (CONS a M, CONS b N) &   
   39.53 +                                  (a, b) : r & (M, N) : X)}"
   39.54  
   39.55    (*defining the abstract constructors*)
   39.56 -  LNil_def  	"LNil == Abs_llist(NIL)"
   39.57 -  LCons_def 	"LCons x xs == Abs_llist(CONS (Leaf x) (Rep_llist xs))"
   39.58 +  LNil_def      "LNil == Abs_llist(NIL)"
   39.59 +  LCons_def     "LCons x xs == Abs_llist(CONS (Leaf x) (Rep_llist xs))"
   39.60  
   39.61    llist_case_def
   39.62     "llist_case c d l == 
   39.63 @@ -93,8 +93,8 @@
   39.64  
   39.65    LList_corec_fun_def
   39.66      "LList_corec_fun k f == 
   39.67 -     nat_rec k (%x. {}) 			
   39.68 -	      (%j r x. sum_case (%u.NIL) (split(%z w. CONS z (r w))) (f x))"
   39.69 +     nat_rec k (%x. {})                         
   39.70 +              (%j r x. sum_case (%u.NIL) (split(%z w. CONS z (r w))) (f x))"
   39.71  
   39.72    LList_corec_def
   39.73      "LList_corec a f == UN k. LList_corec_fun k f a"
   39.74 @@ -105,12 +105,12 @@
   39.75                                      (split(%v w. Inr((Leaf(v), w)))) (f z)))"
   39.76  
   39.77    llistD_Fun_def
   39.78 -   "llistD_Fun(r) == 	
   39.79 -	prod_fun Abs_llist Abs_llist ``  	
   39.80 -                LListD_Fun (diag(range Leaf))	
   39.81 -		            (prod_fun Rep_llist Rep_llist `` r)"
   39.82 +   "llistD_Fun(r) ==    
   39.83 +        prod_fun Abs_llist Abs_llist ``         
   39.84 +                LListD_Fun (diag(range Leaf))   
   39.85 +                            (prod_fun Rep_llist Rep_llist `` r)"
   39.86  
   39.87 -  Lconst_def	"Lconst(M) == lfp(%N. CONS M N)"     
   39.88 +  Lconst_def    "Lconst(M) == lfp(%N. CONS M N)"     
   39.89  
   39.90    Lmap_def
   39.91     "Lmap f M == LList_corec M (List_case (Inl ()) (%x M'. Inr((f(x), M'))))"
   39.92 @@ -118,7 +118,7 @@
   39.93    lmap_def
   39.94     "lmap f l == llist_corec l (llist_case (Inl ()) (%y z. Inr((f(y), z))))"
   39.95  
   39.96 -  iterates_def	"iterates f a == llist_corec a (%x. Inr((x, f(x))))"     
   39.97 +  iterates_def  "iterates f a == llist_corec a (%x. Inr((x, f(x))))"     
   39.98  
   39.99  (*Append generates its result by applying f, where
  39.100      f((NIL,NIL)) = Inl(())
  39.101 @@ -127,18 +127,18 @@
  39.102  *)
  39.103  
  39.104    Lappend_def
  39.105 -   "Lappend M N == LList_corec (M,N)	   				     
  39.106 +   "Lappend M N == LList_corec (M,N)                                         
  39.107       (split(List_case (List_case (Inl ()) (%N1 N2. Inr((N1, (NIL,N2))))) 
  39.108                        (%M1 M2 N. Inr((M1, (M2,N))))))"
  39.109  
  39.110    lappend_def
  39.111 -   "lappend l n == llist_corec (l,n)	   				     
  39.112 +   "lappend l n == llist_corec (l,n)                                         
  39.113     (split(llist_case (llist_case (Inl ()) (%n1 n2. Inr((n1, (LNil,n2))))) 
  39.114                       (%l1 l2 n. Inr((l1, (l2,n))))))"
  39.115  
  39.116  rules
  39.117      (*faking a type definition...*)
  39.118 -  Rep_llist 	    "Rep_llist(xs): llist(range(Leaf))"
  39.119 +  Rep_llist         "Rep_llist(xs): llist(range(Leaf))"
  39.120    Rep_llist_inverse "Abs_llist(Rep_llist(xs)) = xs"
  39.121    Abs_llist_inverse "M: llist(range(Leaf)) ==> Rep_llist(Abs_llist(M)) = M"
  39.122  
    40.1 --- a/src/HOL/ex/LexProd.thy	Mon Feb 05 21:27:16 1996 +0100
    40.2 +++ b/src/HOL/ex/LexProd.thy	Mon Feb 05 21:29:06 1996 +0100
    40.3 @@ -1,6 +1,6 @@
    40.4 -(*  Title: 	HOL/ex/lex-prod.thy
    40.5 +(*  Title:      HOL/ex/lex-prod.thy
    40.6      ID:         $Id$
    40.7 -    Author: 	Tobias Nipkow, TU Munich
    40.8 +    Author:     Tobias Nipkow, TU Munich
    40.9      Copyright   1993  TU Munich
   40.10  
   40.11  The lexicographic product of two relations.
   40.12 @@ -10,6 +10,6 @@
   40.13  consts "**" :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set" (infixl 70)
   40.14  rules
   40.15  lex_prod_def "ra**rb == {p. ? a a' b b'. 
   40.16 -	p = ((a,b),(a',b')) & ((a,a') : ra | a=a' & (b,b') : rb)}"
   40.17 +        p = ((a,b),(a',b')) & ((a,a') : ra | a=a' & (b,b') : rb)}"
   40.18  end
   40.19  
    41.1 --- a/src/HOL/ex/MT.thy	Mon Feb 05 21:27:16 1996 +0100
    41.2 +++ b/src/HOL/ex/MT.thy	Mon Feb 05 21:29:06 1996 +0100
    41.3 @@ -1,6 +1,6 @@
    41.4 -(*  Title: 	HOL/ex/mt.thy
    41.5 +(*  Title:      HOL/ex/mt.thy
    41.6      ID:         $Id$
    41.7 -    Author: 	Jacob Frost, Cambridge University Computer Laboratory
    41.8 +    Author:     Jacob Frost, Cambridge University Computer Laboratory
    41.9      Copyright   1993  University of Cambridge
   41.10  
   41.11  Based upon the article
    42.1 --- a/src/HOL/ex/NatSum.thy	Mon Feb 05 21:27:16 1996 +0100
    42.2 +++ b/src/HOL/ex/NatSum.thy	Mon Feb 05 21:29:06 1996 +0100
    42.3 @@ -1,6 +1,6 @@
    42.4 -(*  Title: 	HOL/ex/natsum.thy
    42.5 +(*  Title:      HOL/ex/natsum.thy
    42.6      ID:         $Id$
    42.7 -    Author: 	Tobias Nipkow
    42.8 +    Author:     Tobias Nipkow
    42.9      Copyright   1994 TU Muenchen
   42.10  
   42.11  A summation operator. sum(f,n+1) is the sum of all f(i), i=0...n.
    43.1 --- a/src/HOL/ex/Perm.thy	Mon Feb 05 21:27:16 1996 +0100
    43.2 +++ b/src/HOL/ex/Perm.thy	Mon Feb 05 21:29:06 1996 +0100
    43.3 @@ -1,6 +1,6 @@
    43.4 -(*  Title: 	HOL/ex/Perm.thy
    43.5 +(*  Title:      HOL/ex/Perm.thy
    43.6      ID:         $Id$
    43.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    43.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    43.9      Copyright   1995  University of Cambridge
   43.10  
   43.11  Permutations: example of an inductive definition
    44.1 --- a/src/HOL/ex/PropLog.thy	Mon Feb 05 21:27:16 1996 +0100
    44.2 +++ b/src/HOL/ex/PropLog.thy	Mon Feb 05 21:29:06 1996 +0100
    44.3 @@ -1,6 +1,6 @@
    44.4 -(*  Title: 	HOL/ex/PropLog.thy
    44.5 +(*  Title:      HOL/ex/PropLog.thy
    44.6      ID:         $Id$
    44.7 -    Author: 	Tobias Nipkow
    44.8 +    Author:     Tobias Nipkow
    44.9      Copyright   1994  TU Muenchen
   44.10  
   44.11  Inductive definition of propositional logic.
   44.12 @@ -11,11 +11,11 @@
   44.13      'a pl = false | var 'a ("#_" [1000]) | "->" ('a pl) ('a pl) (infixr 90)
   44.14  consts
   44.15    thms :: 'a pl set => 'a pl set
   44.16 -  "|-" 	:: ['a pl set, 'a pl] => bool	(infixl 50)
   44.17 -  "|="	:: ['a pl set, 'a pl] => bool	(infixl 50)
   44.18 -  eval2	:: ['a pl, 'a set] => bool
   44.19 -  eval	:: ['a set, 'a pl] => bool	("_[_]" [100,0] 100)
   44.20 -  hyps	:: ['a pl, 'a set] => 'a pl set
   44.21 +  "|-"  :: ['a pl set, 'a pl] => bool   (infixl 50)
   44.22 +  "|="  :: ['a pl set, 'a pl] => bool   (infixl 50)
   44.23 +  eval2 :: ['a pl, 'a set] => bool
   44.24 +  eval  :: ['a set, 'a pl] => bool      ("_[_]" [100,0] 100)
   44.25 +  hyps  :: ['a pl, 'a set] => 'a pl set
   44.26  
   44.27  translations
   44.28    "H |- p" == "p : thms(H)"
    45.1 --- a/src/HOL/ex/Puzzle.thy	Mon Feb 05 21:27:16 1996 +0100
    45.2 +++ b/src/HOL/ex/Puzzle.thy	Mon Feb 05 21:29:06 1996 +0100
    45.3 @@ -1,6 +1,6 @@
    45.4 -(*  Title: 	HOL/ex/puzzle.thy
    45.5 +(*  Title:      HOL/ex/puzzle.thy
    45.6      ID:         $Id$
    45.7 -    Author: 	Tobias Nipkow
    45.8 +    Author:     Tobias Nipkow
    45.9      Copyright   1993 TU Muenchen
   45.10  
   45.11  An question from "Bundeswettbewerb Mathematik"
    46.1 --- a/src/HOL/ex/Qsort.thy	Mon Feb 05 21:27:16 1996 +0100
    46.2 +++ b/src/HOL/ex/Qsort.thy	Mon Feb 05 21:29:06 1996 +0100
    46.3 @@ -1,6 +1,6 @@
    46.4 -(*  Title: 	HOL/ex/qsort.thy
    46.5 +(*  Title:      HOL/ex/qsort.thy
    46.6      ID:         $Id$
    46.7 -    Author: 	Tobias Nipkow
    46.8 +    Author:     Tobias Nipkow
    46.9      Copyright   1994 TU Muenchen
   46.10  
   46.11  Quicksort
    47.1 --- a/src/HOL/ex/Rec.thy	Mon Feb 05 21:27:16 1996 +0100
    47.2 +++ b/src/HOL/ex/Rec.thy	Mon Feb 05 21:29:06 1996 +0100
    47.3 @@ -1,8 +1,8 @@
    47.4  Rec = Fixedpt +
    47.5  consts
    47.6 -fix	:: ('a=>'a) => 'a
    47.7 -Dom	:: (('a=>'b) => ('a=>'b)) => 'a set
    47.8 -Domf	:: (('a=>'b) => ('a=>'b)) => 'a set => 'a set
    47.9 +fix     :: ('a=>'a) => 'a
   47.10 +Dom     :: (('a=>'b) => ('a=>'b)) => 'a set
   47.11 +Domf    :: (('a=>'b) => ('a=>'b)) => 'a set => 'a set
   47.12  rules
   47.13  Domf_def "Domf(F,D) == {y . !f g. (!x:D. f(x)=g(x)) --> F(f,y)=F(g,y)}"
   47.14  Dom_def  "Dom(F) == lfp(Domf(F))"
    48.1 --- a/src/HOL/ex/SList.ML	Mon Feb 05 21:27:16 1996 +0100
    48.2 +++ b/src/HOL/ex/SList.ML	Mon Feb 05 21:29:06 1996 +0100
    48.3 @@ -148,8 +148,18 @@
    48.4  (* The trancl(pred_sexp) is essential because pred_sexp_CONS_I1,2 would not
    48.5     hold if pred_sexp^+ were changed to pred_sexp. *)
    48.6  
    48.7 -val List_rec_unfold = [List_rec_def, wf_pred_sexp RS wf_trancl] MRS def_wfrec
    48.8 -                      |> standard;
    48.9 +goal SList.thy
   48.10 +   "(%M. List_rec M c d) = wfrec (trancl pred_sexp) \
   48.11 +                           \     (%g. List_case c (%x y. d x y (g y)))";
   48.12 +by (simp_tac (HOL_ss addsimps [List_rec_def]) 1);
   48.13 +val List_rec_unfold = standard 
   48.14 +  ((wf_pred_sexp RS wf_trancl) RS ((result() RS eq_reflection) RS def_wfrec));
   48.15 +
   48.16 +(*---------------------------------------------------------------------------
   48.17 + * Old:
   48.18 + * val List_rec_unfold = [List_rec_def,wf_pred_sexp RS wf_trancl] MRS def_wfrec
   48.19 + *                     |> standard;
   48.20 + *---------------------------------------------------------------------------*)
   48.21  
   48.22  (** pred_sexp lemmas **)
   48.23  
    49.1 --- a/src/HOL/ex/SList.thy	Mon Feb 05 21:27:16 1996 +0100
    49.2 +++ b/src/HOL/ex/SList.thy	Mon Feb 05 21:29:06 1996 +0100
    49.3 @@ -27,7 +27,7 @@
    49.4    NIL       :: 'a item
    49.5    CONS      :: ['a item, 'a item] => 'a item
    49.6    Nil       :: 'a list
    49.7 -  "#"       :: ['a, 'a list] => 'a list                   	(infixr 65)
    49.8 +  "#"       :: ['a, 'a list] => 'a list                         (infixr 65)
    49.9    List_case :: ['b, ['a item, 'a item]=>'b, 'a item] => 'b
   49.10    List_rec  :: ['a item, 'b, ['a item, 'a item, 'b]=>'b] => 'b
   49.11    list_case :: ['b, ['a, 'a list]=>'b, 'a list] => 'b
   49.12 @@ -37,10 +37,10 @@
   49.13    null      :: 'a list => bool
   49.14    hd        :: 'a list => 'a
   49.15    tl,ttl    :: 'a list => 'a list
   49.16 -  mem		:: ['a, 'a list] => bool			(infixl 55)
   49.17 +  mem           :: ['a, 'a list] => bool                        (infixl 55)
   49.18    list_all  :: ('a => bool) => ('a list => bool)
   49.19    map       :: ('a=>'b) => ('a list => 'b list)
   49.20 -  "@"	    :: ['a list, 'a list] => 'a list			(infixr 65)
   49.21 +  "@"       :: ['a list, 'a list] => 'a list                    (infixr 65)
   49.22    filter    :: ['a => bool, 'a list] => 'a list
   49.23  
   49.24    (* list Enumeration *)
   49.25 @@ -49,8 +49,8 @@
   49.26    "@list"   :: args => 'a list                    ("[(_)]")
   49.27  
   49.28    (* Special syntax for list_all and filter *)
   49.29 -  "@Alls"	:: [idt, 'a list, bool] => bool	("(2Alls _:_./ _)" 10)
   49.30 -  "@filter"	:: [idt, 'a list, bool] => 'a list	("(1[_:_ ./ _])")
   49.31 +  "@Alls"       :: [idt, 'a list, bool] => bool ("(2Alls _:_./ _)" 10)
   49.32 +  "@filter"     :: [idt, 'a list, bool] => 'a list      ("(1[_:_ ./ _])")
   49.33  
   49.34  translations
   49.35    "[x, xs]"     == "x#[xs]"
   49.36 @@ -59,8 +59,8 @@
   49.37  
   49.38    "case xs of Nil => a | y#ys => b" == "list_case a (%y ys.b) xs"
   49.39  
   49.40 -  "[x:xs . P]"	== "filter (%x.P) xs"
   49.41 -  "Alls x:xs.P"	== "list_all (%x.P) xs"
   49.42 +  "[x:xs . P]"  == "filter (%x.P) xs"
   49.43 +  "Alls x:xs.P" == "list_all (%x.P) xs"
   49.44  
   49.45  defs
   49.46    (* Defining the Concrete Constructors *)
   49.47 @@ -89,8 +89,8 @@
   49.48    (* list Recursion -- the trancl is Essential; see list.ML *)
   49.49  
   49.50    List_rec_def
   49.51 -   "List_rec M c d == wfrec (trancl pred_sexp) M 
   49.52 -                           (List_case (%g.c) (%x y g. d x y (g y)))"
   49.53 +   "List_rec M c d == wfrec (trancl pred_sexp)
   49.54 +                            (%g. List_case c (%x y. d x y (g y))) M"
   49.55  
   49.56    list_rec_def
   49.57     "list_rec l c d == 
   49.58 @@ -105,14 +105,14 @@
   49.59    hd_def        "hd(xs)              == list_rec xs (@x.True) (%x xs r.x)"
   49.60    tl_def        "tl(xs)              == list_rec xs (@xs.True) (%x xs r.xs)"
   49.61    (* a total version of tl: *)
   49.62 -  ttl_def 	"ttl(xs)             == list_rec xs [] (%x xs r.xs)"
   49.63 +  ttl_def       "ttl(xs)             == list_rec xs [] (%x xs r.xs)"
   49.64  
   49.65 -  mem_def 	"x mem xs            == 
   49.66 -		   list_rec xs False (%y ys r. if y=x then True else r)"
   49.67 +  mem_def       "x mem xs            == 
   49.68 +                   list_rec xs False (%y ys r. if y=x then True else r)"
   49.69    list_all_def  "list_all P xs       == list_rec xs True (%x l r. P(x) & r)"
   49.70    map_def       "map f xs            == list_rec xs [] (%x l r. f(x)#r)"
   49.71 -  append_def 	"xs@ys               == list_rec xs ys (%x l r. x#r)"
   49.72 -  filter_def 	"filter P xs         == 
   49.73 +  append_def    "xs@ys               == list_rec xs ys (%x l r. x#r)"
   49.74 +  filter_def    "filter P xs         == 
   49.75                    list_rec xs [] (%x xs r. if P(x) then x#r else r)"
   49.76  
   49.77    list_case_def  "list_case a f xs == list_rec xs a (%x xs r.f x xs)"
    50.1 --- a/src/HOL/ex/Simult.ML	Mon Feb 05 21:27:16 1996 +0100
    50.2 +++ b/src/HOL/ex/Simult.ML	Mon Feb 05 21:29:06 1996 +0100
    50.3 @@ -227,8 +227,19 @@
    50.4  
    50.5  (*** TF_rec -- by wf recursion on pred_sexp ***)
    50.6  
    50.7 -val TF_rec_unfold =
    50.8 -    wf_pred_sexp RS wf_trancl RS (TF_rec_def RS def_wfrec);
    50.9 +goal Simult.thy
   50.10 +   "(%M. TF_rec M b c d) = wfrec (trancl pred_sexp) \
   50.11 +                         \       (%g. Case (Split(%x y. b x y (g y))) \
   50.12 +                         \           (List_case c (%x y. d x y (g x) (g y))))";
   50.13 +by (simp_tac (HOL_ss addsimps [TF_rec_def]) 1);
   50.14 +val TF_rec_unfold = (wf_pred_sexp RS wf_trancl) RS 
   50.15 +                    ((result() RS eq_reflection) RS def_wfrec);
   50.16 +
   50.17 +(*---------------------------------------------------------------------------
   50.18 + * Old: 
   50.19 + * val TF_rec_unfold =
   50.20 + *   wf_pred_sexp RS wf_trancl RS (TF_rec_def RS def_wfrec);
   50.21 + *---------------------------------------------------------------------------*)
   50.22  
   50.23  (** conversion rules for TF_rec **)
   50.24  
    51.1 --- a/src/HOL/ex/Simult.thy	Mon Feb 05 21:27:16 1996 +0100
    51.2 +++ b/src/HOL/ex/Simult.thy	Mon Feb 05 21:29:06 1996 +0100
    51.3 @@ -1,6 +1,6 @@
    51.4 -(*  Title: 	HOL/ex/Simult
    51.5 +(*  Title:      HOL/ex/Simult
    51.6      ID:         $Id$
    51.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    51.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    51.9      Copyright   1993  University of Cambridge
   51.10  
   51.11  A simultaneous recursive type definition: trees & forests
   51.12 @@ -40,35 +40,35 @@
   51.13  
   51.14  defs
   51.15       (*the concrete constants*)
   51.16 -  TCONS_def 	"TCONS M N == In0(M $ N)"
   51.17 -  FNIL_def	"FNIL      == In1(NIL)"
   51.18 -  FCONS_def	"FCONS M N == In1(CONS M N)"
   51.19 +  TCONS_def     "TCONS M N == In0(M $ N)"
   51.20 +  FNIL_def      "FNIL      == In1(NIL)"
   51.21 +  FCONS_def     "FCONS M N == In1(CONS M N)"
   51.22       (*the abstract constants*)
   51.23 -  Tcons_def 	"Tcons a ts == Abs_Tree(TCONS (Leaf a) (Rep_Forest ts))"
   51.24 -  Fnil_def  	"Fnil       == Abs_Forest(FNIL)"
   51.25 -  Fcons_def 	"Fcons t ts == Abs_Forest(FCONS (Rep_Tree t) (Rep_Forest ts))"
   51.26 +  Tcons_def     "Tcons a ts == Abs_Tree(TCONS (Leaf a) (Rep_Forest ts))"
   51.27 +  Fnil_def      "Fnil       == Abs_Forest(FNIL)"
   51.28 +  Fcons_def     "Fcons t ts == Abs_Forest(FCONS (Rep_Tree t) (Rep_Forest ts))"
   51.29  
   51.30 -  TF_def	"TF(A) == lfp(%Z. A <*> Part Z In1 
   51.31 +  TF_def        "TF(A) == lfp(%Z. A <*> Part Z In1 
   51.32                             <+> ({Numb(0)} <+> Part Z In0 <*> Part Z In1))"
   51.33  
   51.34  rules
   51.35    (*faking a type definition for tree...*)
   51.36 -  Rep_Tree 	   "Rep_Tree(n): Part (TF(range Leaf)) In0"
   51.37 +  Rep_Tree         "Rep_Tree(n): Part (TF(range Leaf)) In0"
   51.38    Rep_Tree_inverse "Abs_Tree(Rep_Tree(t)) = t"
   51.39    Abs_Tree_inverse "z: Part (TF(range Leaf)) In0 ==> Rep_Tree(Abs_Tree(z)) = z"
   51.40      (*faking a type definition for forest...*)
   51.41 -  Rep_Forest 	     "Rep_Forest(n): Part (TF(range Leaf)) In1"
   51.42 +  Rep_Forest         "Rep_Forest(n): Part (TF(range Leaf)) In1"
   51.43    Rep_Forest_inverse "Abs_Forest(Rep_Forest(ts)) = ts"
   51.44    Abs_Forest_inverse 
   51.45 -	"z: Part (TF(range Leaf)) In1 ==> Rep_Forest(Abs_Forest(z)) = z"
   51.46 +        "z: Part (TF(range Leaf)) In1 ==> Rep_Forest(Abs_Forest(z)) = z"
   51.47  
   51.48  
   51.49  defs
   51.50       (*recursion*)
   51.51 -  TF_rec_def	
   51.52 -   "TF_rec M b c d == wfrec (trancl pred_sexp) M   
   51.53 -               (Case (Split(%x y g. b x y (g y))) 
   51.54 -	              (List_case (%g.c) (%x y g. d x y (g x) (g y))))"
   51.55 +  TF_rec_def    
   51.56 +   "TF_rec M b c d == wfrec (trancl pred_sexp)
   51.57 +               (%g. Case (Split(%x y. b x y (g y))) 
   51.58 +                      (List_case c (%x y. d x y (g x) (g y)))) M"
   51.59  
   51.60    tree_rec_def
   51.61     "tree_rec t b c d == 
    52.1 --- a/src/HOL/ex/Sorting.thy	Mon Feb 05 21:27:16 1996 +0100
    52.2 +++ b/src/HOL/ex/Sorting.thy	Mon Feb 05 21:29:06 1996 +0100
    52.3 @@ -1,6 +1,6 @@
    52.4 -(*  Title: 	HOL/ex/sorting.thy
    52.5 +(*  Title:      HOL/ex/sorting.thy
    52.6      ID:         $Id$
    52.7 -    Author: 	Tobias Nipkow
    52.8 +    Author:     Tobias Nipkow
    52.9      Copyright   1994 TU Muenchen
   52.10  
   52.11  Specification of sorting
    53.1 --- a/src/HOL/ex/Term.ML	Mon Feb 05 21:27:16 1996 +0100
    53.2 +++ b/src/HOL/ex/Term.ML	Mon Feb 05 21:29:06 1996 +0100
    53.3 @@ -110,8 +110,18 @@
    53.4  
    53.5  (*** Term_rec -- by wf recursion on pred_sexp ***)
    53.6  
    53.7 -val Term_rec_unfold =
    53.8 -    wf_pred_sexp RS wf_trancl RS (Term_rec_def RS def_wfrec);
    53.9 +goal Term.thy
   53.10 +   "(%M. Term_rec M d) = wfrec (trancl pred_sexp) \
   53.11 +                             \ (%g. Split(%x y. d x y (Abs_map g y)))";
   53.12 +by (simp_tac (HOL_ss addsimps [Term_rec_def]) 1);
   53.13 +bind_thm("Term_rec_unfold", (wf_pred_sexp RS wf_trancl) RS 
   53.14 +                            ((result() RS eq_reflection) RS def_wfrec));
   53.15 +
   53.16 +(*---------------------------------------------------------------------------
   53.17 + * Old:
   53.18 + * val Term_rec_unfold =
   53.19 + *     wf_pred_sexp RS wf_trancl RS (Term_rec_def RS def_wfrec);
   53.20 + *---------------------------------------------------------------------------*)
   53.21  
   53.22  (** conversion rules **)
   53.23  
    54.1 --- a/src/HOL/ex/Term.thy	Mon Feb 05 21:27:16 1996 +0100
    54.2 +++ b/src/HOL/ex/Term.thy	Mon Feb 05 21:29:06 1996 +0100
    54.3 @@ -1,6 +1,6 @@
    54.4 -(*  Title: 	HOL/ex/Term
    54.5 +(*  Title:      HOL/ex/Term
    54.6      ID:         $Id$
    54.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    54.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    54.9      Copyright   1992  University of Cambridge
   54.10  
   54.11  Terms over a given alphabet -- function applications; illustrates list functor
   54.12 @@ -16,14 +16,14 @@
   54.13  arities term :: (term)term
   54.14  
   54.15  consts
   54.16 -  term		:: 'a item set => 'a item set
   54.17 -  Rep_term	:: 'a term => 'a item
   54.18 -  Abs_term	:: 'a item => 'a term
   54.19 -  Rep_Tlist	:: 'a term list => 'a item
   54.20 -  Abs_Tlist	:: 'a item => 'a term list
   54.21 -  App		:: ['a, ('a term)list] => 'a term
   54.22 -  Term_rec	:: ['a item, ['a item , 'a item, 'b list]=>'b] => 'b
   54.23 -  term_rec	:: ['a term, ['a ,'a term list, 'b list]=>'b] => 'b
   54.24 +  term          :: 'a item set => 'a item set
   54.25 +  Rep_term      :: 'a term => 'a item
   54.26 +  Abs_term      :: 'a item => 'a term
   54.27 +  Rep_Tlist     :: 'a term list => 'a item
   54.28 +  Abs_Tlist     :: 'a item => 'a term list
   54.29 +  App           :: ['a, ('a term)list] => 'a term
   54.30 +  Term_rec      :: ['a item, ['a item , 'a item, 'b list]=>'b] => 'b
   54.31 +  term_rec      :: ['a term, ['a ,'a term list, 'b list]=>'b] => 'b
   54.32  
   54.33  inductive "term(A)"
   54.34    intrs
   54.35 @@ -32,16 +32,16 @@
   54.36  
   54.37  defs
   54.38    (*defining abstraction/representation functions for term list...*)
   54.39 -  Rep_Tlist_def	"Rep_Tlist == Rep_map(Rep_term)"
   54.40 -  Abs_Tlist_def	"Abs_Tlist == Abs_map(Abs_term)"
   54.41 +  Rep_Tlist_def "Rep_Tlist == Rep_map(Rep_term)"
   54.42 +  Abs_Tlist_def "Abs_Tlist == Abs_map(Abs_term)"
   54.43  
   54.44    (*defining the abstract constants*)
   54.45 -  App_def 	"App a ts == Abs_term(Leaf(a) $ Rep_Tlist(ts))"
   54.46 +  App_def       "App a ts == Abs_term(Leaf(a) $ Rep_Tlist(ts))"
   54.47  
   54.48    (*list recursion*)
   54.49 -  Term_rec_def	
   54.50 -   "Term_rec M d == wfrec (trancl pred_sexp) M 
   54.51 -           (Split(%x y g. d x y (Abs_map g y)))"
   54.52 +  Term_rec_def  
   54.53 +   "Term_rec M d == wfrec (trancl pred_sexp)
   54.54 +           (%g. Split(%x y. d x y (Abs_map g y))) M"
   54.55  
   54.56    term_rec_def
   54.57     "term_rec t d == 
   54.58 @@ -49,7 +49,7 @@
   54.59  
   54.60  rules
   54.61      (*faking a type definition for term...*)
   54.62 -  Rep_term 		"Rep_term(n): term(range(Leaf))"
   54.63 -  Rep_term_inverse 	"Abs_term(Rep_term(t)) = t"
   54.64 -  Abs_term_inverse 	"M: term(range(Leaf)) ==> Rep_term(Abs_term(M)) = M"
   54.65 +  Rep_term              "Rep_term(n): term(range(Leaf))"
   54.66 +  Rep_term_inverse      "Abs_term(Rep_term(t)) = t"
   54.67 +  Abs_term_inverse      "M: term(range(Leaf)) ==> Rep_term(Abs_term(M)) = M"
   54.68  end