src/HOLCF/Sprod2.ML
changeset 1461 6bcb44e4d6e5
parent 1168 74be52691d62
child 1779 1155c06fa956
     1.1 --- a/src/HOLCF/Sprod2.ML	Mon Jan 29 14:16:13 1996 +0100
     1.2 +++ b/src/HOLCF/Sprod2.ML	Tue Jan 30 13:42:57 1996 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4 -(*  Title: 	HOLCF/sprod2.ML
     1.5 +(*  Title:      HOLCF/sprod2.ML
     1.6      ID:         $Id$
     1.7 -    Author: 	Franz Regensburger
     1.8 +    Author:     Franz Regensburger
     1.9      Copyright   1993 Technische Universitaet Muenchen
    1.10  
    1.11  Lemmas for sprod2.thy
    1.12 @@ -14,47 +14,47 @@
    1.13  (* ------------------------------------------------------------------------ *)
    1.14  
    1.15  qed_goal "less_sprod3a" Sprod2.thy 
    1.16 -	"p1=Ispair UU UU ==> p1 << p2"
    1.17 +        "p1=Ispair UU UU ==> p1 << p2"
    1.18  (fn prems =>
    1.19 -	[
    1.20 -	(cut_facts_tac prems 1),
    1.21 -	(rtac (inst_sprod_po RS ssubst) 1),
    1.22 -	(etac less_sprod1a 1)
    1.23 -	]);
    1.24 +        [
    1.25 +        (cut_facts_tac prems 1),
    1.26 +        (rtac (inst_sprod_po RS ssubst) 1),
    1.27 +        (etac less_sprod1a 1)
    1.28 +        ]);
    1.29  
    1.30  
    1.31  qed_goal "less_sprod3b" Sprod2.thy
    1.32   "p1~=Ispair UU UU ==>\
    1.33 -\	(p1<<p2) = (Isfst(p1)<<Isfst(p2) & Issnd(p1)<<Issnd(p2))" 
    1.34 +\       (p1<<p2) = (Isfst(p1)<<Isfst(p2) & Issnd(p1)<<Issnd(p2))" 
    1.35  (fn prems =>
    1.36 -	[
    1.37 -	(cut_facts_tac prems 1),
    1.38 -	(rtac (inst_sprod_po RS ssubst) 1),
    1.39 -	(etac less_sprod1b 1)
    1.40 -	]);
    1.41 +        [
    1.42 +        (cut_facts_tac prems 1),
    1.43 +        (rtac (inst_sprod_po RS ssubst) 1),
    1.44 +        (etac less_sprod1b 1)
    1.45 +        ]);
    1.46  
    1.47  qed_goal "less_sprod4b" Sprod2.thy 
    1.48 -	"p << Ispair UU UU ==> p = Ispair UU UU"
    1.49 +        "p << Ispair UU UU ==> p = Ispair UU UU"
    1.50  (fn prems =>
    1.51 -	[
    1.52 -	(cut_facts_tac prems 1),
    1.53 -	(rtac less_sprod2b 1),
    1.54 -	(etac (inst_sprod_po RS subst) 1)
    1.55 -	]);
    1.56 +        [
    1.57 +        (cut_facts_tac prems 1),
    1.58 +        (rtac less_sprod2b 1),
    1.59 +        (etac (inst_sprod_po RS subst) 1)
    1.60 +        ]);
    1.61  
    1.62  val less_sprod4a = (less_sprod4b RS defined_Ispair_rev);
    1.63  (* Ispair ?a ?b << Ispair UU UU ==> ?a = UU | ?b = UU *)
    1.64  
    1.65  qed_goal "less_sprod4c" Sprod2.thy
    1.66   "[|Ispair xa ya << Ispair x y; xa~=UU; ya~=UU; x~=UU; y~=UU|] ==>\
    1.67 -\		xa<<x & ya << y"
    1.68 +\               xa<<x & ya << y"
    1.69  (fn prems =>
    1.70 -	[
    1.71 -	(cut_facts_tac prems 1),
    1.72 -	(rtac less_sprod2c 1),
    1.73 -	(etac (inst_sprod_po RS subst) 1),
    1.74 -	(REPEAT (atac 1))
    1.75 -	]);
    1.76 +        [
    1.77 +        (cut_facts_tac prems 1),
    1.78 +        (rtac less_sprod2c 1),
    1.79 +        (etac (inst_sprod_po RS subst) 1),
    1.80 +        (REPEAT (atac 1))
    1.81 +        ]);
    1.82  
    1.83  (* ------------------------------------------------------------------------ *)
    1.84  (* type sprod is pointed                                                    *)
    1.85 @@ -62,10 +62,10 @@
    1.86  
    1.87  qed_goal "minimal_sprod" Sprod2.thy  "Ispair UU UU << p"
    1.88  (fn prems =>
    1.89 -	[
    1.90 -	(rtac less_sprod3a 1),
    1.91 -	(rtac refl 1)
    1.92 -	]);
    1.93 +        [
    1.94 +        (rtac less_sprod3a 1),
    1.95 +        (rtac refl 1)
    1.96 +        ]);
    1.97  
    1.98  (* ------------------------------------------------------------------------ *)
    1.99  (* Ispair is monotone in both arguments                                     *)
   1.100 @@ -73,93 +73,93 @@
   1.101  
   1.102  qed_goalw "monofun_Ispair1" Sprod2.thy [monofun] "monofun(Ispair)"
   1.103  (fn prems =>
   1.104 -	[
   1.105 -	(strip_tac 1),
   1.106 -	(rtac (less_fun RS iffD2) 1),
   1.107 -	(strip_tac 1),
   1.108 -	(res_inst_tac [("Q",
   1.109 -	" Ispair y xa = Ispair UU UU")] (excluded_middle RS disjE) 1),
   1.110 -	(res_inst_tac [("Q",
   1.111 -	" Ispair x xa = Ispair UU UU")] (excluded_middle RS disjE) 1),
   1.112 -	(rtac (less_sprod3b RS iffD2) 1),
   1.113 -	(atac 1),
   1.114 -	(rtac conjI 1),
   1.115 -	(rtac (Isfst RS ssubst) 1),
   1.116 -	(etac (strict_Ispair_rev RS conjunct1) 1),
   1.117 -	(etac (strict_Ispair_rev RS conjunct2) 1),
   1.118 -	(rtac (Isfst RS ssubst) 1),
   1.119 -	(etac (strict_Ispair_rev RS conjunct1) 1),
   1.120 -	(etac (strict_Ispair_rev RS conjunct2) 1),
   1.121 -	(atac 1),
   1.122 -	(rtac (Issnd RS ssubst) 1),
   1.123 -	(etac (strict_Ispair_rev RS conjunct1) 1),
   1.124 -	(etac (strict_Ispair_rev RS conjunct2) 1),
   1.125 -	(rtac (Issnd RS ssubst) 1),
   1.126 -	(etac (strict_Ispair_rev RS conjunct1) 1),
   1.127 -	(etac (strict_Ispair_rev RS conjunct2) 1),
   1.128 -	(rtac refl_less 1),
   1.129 -	(etac less_sprod3a 1),
   1.130 -	(res_inst_tac [("Q",
   1.131 -	" Ispair x xa  = Ispair UU UU")] (excluded_middle RS disjE) 1),
   1.132 -	(etac less_sprod3a 2),
   1.133 -	(res_inst_tac [("P","Ispair y xa = Ispair UU UU")] notE 1),
   1.134 -	(atac 2),
   1.135 -	(rtac defined_Ispair 1),
   1.136 -	(etac notUU_I 1),
   1.137 -	(etac (strict_Ispair_rev RS  conjunct1) 1),
   1.138 -	(etac (strict_Ispair_rev RS  conjunct2) 1)
   1.139 -	]);
   1.140 +        [
   1.141 +        (strip_tac 1),
   1.142 +        (rtac (less_fun RS iffD2) 1),
   1.143 +        (strip_tac 1),
   1.144 +        (res_inst_tac [("Q",
   1.145 +        " Ispair y xa = Ispair UU UU")] (excluded_middle RS disjE) 1),
   1.146 +        (res_inst_tac [("Q",
   1.147 +        " Ispair x xa = Ispair UU UU")] (excluded_middle RS disjE) 1),
   1.148 +        (rtac (less_sprod3b RS iffD2) 1),
   1.149 +        (atac 1),
   1.150 +        (rtac conjI 1),
   1.151 +        (rtac (Isfst RS ssubst) 1),
   1.152 +        (etac (strict_Ispair_rev RS conjunct1) 1),
   1.153 +        (etac (strict_Ispair_rev RS conjunct2) 1),
   1.154 +        (rtac (Isfst RS ssubst) 1),
   1.155 +        (etac (strict_Ispair_rev RS conjunct1) 1),
   1.156 +        (etac (strict_Ispair_rev RS conjunct2) 1),
   1.157 +        (atac 1),
   1.158 +        (rtac (Issnd RS ssubst) 1),
   1.159 +        (etac (strict_Ispair_rev RS conjunct1) 1),
   1.160 +        (etac (strict_Ispair_rev RS conjunct2) 1),
   1.161 +        (rtac (Issnd RS ssubst) 1),
   1.162 +        (etac (strict_Ispair_rev RS conjunct1) 1),
   1.163 +        (etac (strict_Ispair_rev RS conjunct2) 1),
   1.164 +        (rtac refl_less 1),
   1.165 +        (etac less_sprod3a 1),
   1.166 +        (res_inst_tac [("Q",
   1.167 +        " Ispair x xa  = Ispair UU UU")] (excluded_middle RS disjE) 1),
   1.168 +        (etac less_sprod3a 2),
   1.169 +        (res_inst_tac [("P","Ispair y xa = Ispair UU UU")] notE 1),
   1.170 +        (atac 2),
   1.171 +        (rtac defined_Ispair 1),
   1.172 +        (etac notUU_I 1),
   1.173 +        (etac (strict_Ispair_rev RS  conjunct1) 1),
   1.174 +        (etac (strict_Ispair_rev RS  conjunct2) 1)
   1.175 +        ]);
   1.176  
   1.177  
   1.178  qed_goalw "monofun_Ispair2" Sprod2.thy [monofun] "monofun(Ispair(x))"
   1.179  (fn prems =>
   1.180 -	[
   1.181 -	(strip_tac 1),
   1.182 -	(res_inst_tac [("Q",
   1.183 -	" Ispair x y = Ispair UU UU")] (excluded_middle RS disjE) 1),
   1.184 -	(res_inst_tac [("Q",
   1.185 -	" Ispair x xa = Ispair UU UU")] (excluded_middle RS disjE) 1),
   1.186 -	(rtac (less_sprod3b RS iffD2) 1),
   1.187 -	(atac 1),
   1.188 -	(rtac conjI 1),
   1.189 -	(rtac (Isfst RS ssubst) 1),
   1.190 -	(etac (strict_Ispair_rev RS conjunct1) 1),
   1.191 -	(etac (strict_Ispair_rev RS conjunct2) 1),
   1.192 -	(rtac (Isfst RS ssubst) 1),
   1.193 -	(etac (strict_Ispair_rev RS conjunct1) 1),
   1.194 -	(etac (strict_Ispair_rev RS conjunct2) 1),
   1.195 -	(rtac refl_less 1),
   1.196 -	(rtac (Issnd RS ssubst) 1),
   1.197 -	(etac (strict_Ispair_rev RS conjunct1) 1),
   1.198 -	(etac (strict_Ispair_rev RS conjunct2) 1),
   1.199 -	(rtac (Issnd RS ssubst) 1),
   1.200 -	(etac (strict_Ispair_rev RS conjunct1) 1),
   1.201 -	(etac (strict_Ispair_rev RS conjunct2) 1),
   1.202 -	(atac 1),
   1.203 -	(etac less_sprod3a 1),
   1.204 -	(res_inst_tac [("Q",
   1.205 -	" Ispair x xa = Ispair UU UU")] (excluded_middle RS disjE) 1),
   1.206 -	(etac less_sprod3a 2),
   1.207 -	(res_inst_tac [("P","Ispair x y = Ispair UU UU")] notE 1),
   1.208 -	(atac 2),
   1.209 -	(rtac defined_Ispair 1),
   1.210 -	(etac (strict_Ispair_rev RS  conjunct1) 1),
   1.211 -	(etac notUU_I 1),
   1.212 -	(etac (strict_Ispair_rev RS  conjunct2) 1)
   1.213 -	]);
   1.214 +        [
   1.215 +        (strip_tac 1),
   1.216 +        (res_inst_tac [("Q",
   1.217 +        " Ispair x y = Ispair UU UU")] (excluded_middle RS disjE) 1),
   1.218 +        (res_inst_tac [("Q",
   1.219 +        " Ispair x xa = Ispair UU UU")] (excluded_middle RS disjE) 1),
   1.220 +        (rtac (less_sprod3b RS iffD2) 1),
   1.221 +        (atac 1),
   1.222 +        (rtac conjI 1),
   1.223 +        (rtac (Isfst RS ssubst) 1),
   1.224 +        (etac (strict_Ispair_rev RS conjunct1) 1),
   1.225 +        (etac (strict_Ispair_rev RS conjunct2) 1),
   1.226 +        (rtac (Isfst RS ssubst) 1),
   1.227 +        (etac (strict_Ispair_rev RS conjunct1) 1),
   1.228 +        (etac (strict_Ispair_rev RS conjunct2) 1),
   1.229 +        (rtac refl_less 1),
   1.230 +        (rtac (Issnd RS ssubst) 1),
   1.231 +        (etac (strict_Ispair_rev RS conjunct1) 1),
   1.232 +        (etac (strict_Ispair_rev RS conjunct2) 1),
   1.233 +        (rtac (Issnd RS ssubst) 1),
   1.234 +        (etac (strict_Ispair_rev RS conjunct1) 1),
   1.235 +        (etac (strict_Ispair_rev RS conjunct2) 1),
   1.236 +        (atac 1),
   1.237 +        (etac less_sprod3a 1),
   1.238 +        (res_inst_tac [("Q",
   1.239 +        " Ispair x xa = Ispair UU UU")] (excluded_middle RS disjE) 1),
   1.240 +        (etac less_sprod3a 2),
   1.241 +        (res_inst_tac [("P","Ispair x y = Ispair UU UU")] notE 1),
   1.242 +        (atac 2),
   1.243 +        (rtac defined_Ispair 1),
   1.244 +        (etac (strict_Ispair_rev RS  conjunct1) 1),
   1.245 +        (etac notUU_I 1),
   1.246 +        (etac (strict_Ispair_rev RS  conjunct2) 1)
   1.247 +        ]);
   1.248  
   1.249  qed_goal " monofun_Ispair" Sprod2.thy 
   1.250   "[|x1<<x2; y1<<y2|] ==> Ispair x1 y1 << Ispair x2 y2"
   1.251  (fn prems =>
   1.252 -	[
   1.253 -	(cut_facts_tac prems 1),
   1.254 -	(rtac trans_less 1),
   1.255 -	(rtac (monofun_Ispair1 RS monofunE RS spec RS spec RS mp RS 
   1.256 -	(less_fun RS iffD1 RS spec)) 1),
   1.257 -	(rtac (monofun_Ispair2 RS monofunE RS spec RS spec RS mp) 2),
   1.258 -	(atac 1),
   1.259 -	(atac 1)
   1.260 -	]);
   1.261 +        [
   1.262 +        (cut_facts_tac prems 1),
   1.263 +        (rtac trans_less 1),
   1.264 +        (rtac (monofun_Ispair1 RS monofunE RS spec RS spec RS mp RS 
   1.265 +        (less_fun RS iffD1 RS spec)) 1),
   1.266 +        (rtac (monofun_Ispair2 RS monofunE RS spec RS spec RS mp) 2),
   1.267 +        (atac 1),
   1.268 +        (atac 1)
   1.269 +        ]);
   1.270  
   1.271  
   1.272  (* ------------------------------------------------------------------------ *)
   1.273 @@ -168,57 +168,57 @@
   1.274  
   1.275  qed_goalw " monofun_Isfst" Sprod2.thy [monofun] "monofun(Isfst)"
   1.276  (fn prems =>
   1.277 -	[
   1.278 -	(strip_tac 1),
   1.279 -	(res_inst_tac [("p","x")] IsprodE 1),
   1.280 -	(hyp_subst_tac 1),
   1.281 -	(rtac trans_less 1),
   1.282 -	(rtac minimal 2),
   1.283 -	(rtac (strict_Isfst1 RS ssubst) 1),
   1.284 -	(rtac refl_less 1),
   1.285 -	(hyp_subst_tac 1),
   1.286 -	(res_inst_tac [("p","y")] IsprodE 1),
   1.287 -	(hyp_subst_tac 1),
   1.288 -	(res_inst_tac [("t","Isfst(Ispair xa ya)")] subst 1),
   1.289 -	(rtac refl_less 2),
   1.290 -	(etac (less_sprod4b RS sym RS arg_cong) 1),
   1.291 -	(hyp_subst_tac 1),
   1.292 -	(rtac (Isfst RS ssubst) 1),
   1.293 -	(atac 1),
   1.294 -	(atac 1),
   1.295 -	(rtac (Isfst RS ssubst) 1),
   1.296 -	(atac 1),
   1.297 -	(atac 1),
   1.298 -	(etac (less_sprod4c RS  conjunct1) 1),
   1.299 -	(REPEAT (atac 1))
   1.300 -	]);
   1.301 +        [
   1.302 +        (strip_tac 1),
   1.303 +        (res_inst_tac [("p","x")] IsprodE 1),
   1.304 +        (hyp_subst_tac 1),
   1.305 +        (rtac trans_less 1),
   1.306 +        (rtac minimal 2),
   1.307 +        (rtac (strict_Isfst1 RS ssubst) 1),
   1.308 +        (rtac refl_less 1),
   1.309 +        (hyp_subst_tac 1),
   1.310 +        (res_inst_tac [("p","y")] IsprodE 1),
   1.311 +        (hyp_subst_tac 1),
   1.312 +        (res_inst_tac [("t","Isfst(Ispair xa ya)")] subst 1),
   1.313 +        (rtac refl_less 2),
   1.314 +        (etac (less_sprod4b RS sym RS arg_cong) 1),
   1.315 +        (hyp_subst_tac 1),
   1.316 +        (rtac (Isfst RS ssubst) 1),
   1.317 +        (atac 1),
   1.318 +        (atac 1),
   1.319 +        (rtac (Isfst RS ssubst) 1),
   1.320 +        (atac 1),
   1.321 +        (atac 1),
   1.322 +        (etac (less_sprod4c RS  conjunct1) 1),
   1.323 +        (REPEAT (atac 1))
   1.324 +        ]);
   1.325  
   1.326  qed_goalw "monofun_Issnd" Sprod2.thy [monofun] "monofun(Issnd)"
   1.327  (fn prems =>
   1.328 -	[
   1.329 -	(strip_tac 1),
   1.330 -	(res_inst_tac [("p","x")] IsprodE 1),
   1.331 -	(hyp_subst_tac 1),
   1.332 -	(rtac trans_less 1),
   1.333 -	(rtac minimal 2),
   1.334 -	(rtac (strict_Issnd1 RS ssubst) 1),
   1.335 -	(rtac refl_less 1),
   1.336 -	(hyp_subst_tac 1),
   1.337 -	(res_inst_tac [("p","y")] IsprodE 1),
   1.338 -	(hyp_subst_tac 1),
   1.339 -	(res_inst_tac [("t","Issnd(Ispair xa ya)")] subst 1),
   1.340 -	(rtac refl_less 2),
   1.341 -	(etac (less_sprod4b RS sym RS arg_cong) 1),
   1.342 -	(hyp_subst_tac 1),
   1.343 -	(rtac (Issnd RS ssubst) 1),
   1.344 -	(atac 1),
   1.345 -	(atac 1),
   1.346 -	(rtac (Issnd RS ssubst) 1),
   1.347 -	(atac 1),
   1.348 -	(atac 1),
   1.349 -	(etac (less_sprod4c RS  conjunct2) 1),
   1.350 -	(REPEAT (atac 1))
   1.351 -	]);
   1.352 +        [
   1.353 +        (strip_tac 1),
   1.354 +        (res_inst_tac [("p","x")] IsprodE 1),
   1.355 +        (hyp_subst_tac 1),
   1.356 +        (rtac trans_less 1),
   1.357 +        (rtac minimal 2),
   1.358 +        (rtac (strict_Issnd1 RS ssubst) 1),
   1.359 +        (rtac refl_less 1),
   1.360 +        (hyp_subst_tac 1),
   1.361 +        (res_inst_tac [("p","y")] IsprodE 1),
   1.362 +        (hyp_subst_tac 1),
   1.363 +        (res_inst_tac [("t","Issnd(Ispair xa ya)")] subst 1),
   1.364 +        (rtac refl_less 2),
   1.365 +        (etac (less_sprod4b RS sym RS arg_cong) 1),
   1.366 +        (hyp_subst_tac 1),
   1.367 +        (rtac (Issnd RS ssubst) 1),
   1.368 +        (atac 1),
   1.369 +        (atac 1),
   1.370 +        (rtac (Issnd RS ssubst) 1),
   1.371 +        (atac 1),
   1.372 +        (atac 1),
   1.373 +        (etac (less_sprod4c RS  conjunct2) 1),
   1.374 +        (REPEAT (atac 1))
   1.375 +        ]);
   1.376  
   1.377  
   1.378  (* ------------------------------------------------------------------------ *)
   1.379 @@ -229,40 +229,40 @@
   1.380  "[|is_chain(S)|] ==> range(S) <<| \
   1.381  \ Ispair (lub(range(%i.Isfst(S i)))) (lub(range(%i.Issnd(S i))))"
   1.382  (fn prems =>
   1.383 -	[
   1.384 -	(cut_facts_tac prems 1),
   1.385 -	(rtac is_lubI 1),
   1.386 -	(rtac conjI 1),
   1.387 -	(rtac ub_rangeI 1),
   1.388 -	(rtac allI 1),
   1.389 -	(res_inst_tac [("t","S(i)")] (surjective_pairing_Sprod RS ssubst) 1),
   1.390 -	(rtac monofun_Ispair 1),
   1.391 -	(rtac is_ub_thelub 1),
   1.392 -	(etac (monofun_Isfst RS ch2ch_monofun) 1),
   1.393 -	(rtac is_ub_thelub 1),
   1.394 -	(etac (monofun_Issnd RS ch2ch_monofun) 1),
   1.395 -	(strip_tac 1),
   1.396 -	(res_inst_tac [("t","u")] (surjective_pairing_Sprod RS ssubst) 1),
   1.397 -	(rtac monofun_Ispair 1),
   1.398 -	(rtac is_lub_thelub 1),
   1.399 -	(etac (monofun_Isfst RS ch2ch_monofun) 1),
   1.400 -	(etac (monofun_Isfst RS ub2ub_monofun) 1),
   1.401 -	(rtac is_lub_thelub 1),
   1.402 -	(etac (monofun_Issnd RS ch2ch_monofun) 1),
   1.403 -	(etac (monofun_Issnd RS ub2ub_monofun) 1)
   1.404 -	]);
   1.405 +        [
   1.406 +        (cut_facts_tac prems 1),
   1.407 +        (rtac is_lubI 1),
   1.408 +        (rtac conjI 1),
   1.409 +        (rtac ub_rangeI 1),
   1.410 +        (rtac allI 1),
   1.411 +        (res_inst_tac [("t","S(i)")] (surjective_pairing_Sprod RS ssubst) 1),
   1.412 +        (rtac monofun_Ispair 1),
   1.413 +        (rtac is_ub_thelub 1),
   1.414 +        (etac (monofun_Isfst RS ch2ch_monofun) 1),
   1.415 +        (rtac is_ub_thelub 1),
   1.416 +        (etac (monofun_Issnd RS ch2ch_monofun) 1),
   1.417 +        (strip_tac 1),
   1.418 +        (res_inst_tac [("t","u")] (surjective_pairing_Sprod RS ssubst) 1),
   1.419 +        (rtac monofun_Ispair 1),
   1.420 +        (rtac is_lub_thelub 1),
   1.421 +        (etac (monofun_Isfst RS ch2ch_monofun) 1),
   1.422 +        (etac (monofun_Isfst RS ub2ub_monofun) 1),
   1.423 +        (rtac is_lub_thelub 1),
   1.424 +        (etac (monofun_Issnd RS ch2ch_monofun) 1),
   1.425 +        (etac (monofun_Issnd RS ub2ub_monofun) 1)
   1.426 +        ]);
   1.427  
   1.428  val thelub_sprod = (lub_sprod RS thelubI);
   1.429  
   1.430  
   1.431  qed_goal "cpo_sprod" Sprod2.thy 
   1.432 -	"is_chain(S::nat=>'a**'b)==>? x.range(S)<<| x"
   1.433 +        "is_chain(S::nat=>'a**'b)==>? x.range(S)<<| x"
   1.434  (fn prems =>
   1.435 -	[
   1.436 -	(cut_facts_tac prems 1),
   1.437 -	(rtac exI 1),
   1.438 -	(etac lub_sprod 1)
   1.439 -	]);
   1.440 +        [
   1.441 +        (cut_facts_tac prems 1),
   1.442 +        (rtac exI 1),
   1.443 +        (etac lub_sprod 1)
   1.444 +        ]);
   1.445  
   1.446  
   1.447