# HG changeset patch
# User oheimb
# Date 851011307 -3600
# Node ID 045d00d777fbc896da5aadf7f9c2ce8e24b85751
# Parent  ce85a2aafc7a56ed431388b15566ab81ad1a38a6
converted dist_less_one and dist_eq_one to single theorems instead of thm lists
re-added lost Addsimps (dist_less_one::dist_eq_one::one_when);

diff -r ce85a2aafc7a -r 045d00d777fb src/HOLCF/One.ML
--- a/src/HOLCF/One.ML	Thu Dec 19 11:58:39 1996 +0100
+++ b/src/HOLCF/One.ML	Thu Dec 19 17:01:47 1996 +0100
@@ -3,7 +3,7 @@
     Author:     Franz Regensburger
     Copyright   1993 Technische Universitaet Muenchen
 
-Lemmas for one.thy 
+Lemmas for One.thy 
 *)
 
 open One;
@@ -41,28 +41,18 @@
 (* distinctness for type one : stored in a list                             *)
 (* ------------------------------------------------------------------------ *)
 
-val dist_less_one = [
-prove_goalw One.thy [one_def] "~one << UU"
- (fn prems =>
-        [
+qed_goalw "dist_less_one" One.thy [one_def] "~one << UU" (fn prems => [
         (rtac classical2 1),
         (rtac less_up4b 1),
         (rtac (rep_one_iso RS subst) 1),
         (rtac (rep_one_iso RS subst) 1),
         (rtac monofun_cfun_arg 1),
         (etac ((abs_one_iso RS allI) RS ((rep_one_iso RS allI) RS iso_strict ) 
-                RS conjunct2 RS ssubst) 1)
-        ])
-];
+                RS conjunct2 RS ssubst) 1)]);
 
-val  dist_eq_one = [prove_goal One.thy "one~=UU"
- (fn prems =>
-        [
+qed_goal "dist_eq_one" One.thy "one~=UU" (fn prems => [
         (rtac not_less2not_eq 1),
-        (resolve_tac dist_less_one 1)
-        ])];
-
-val dist_eq_one = dist_eq_one @ (map (fn thm => (thm RS not_sym)) dist_eq_one);
+        (rtac dist_less_one 1)]);
 
 (* ------------------------------------------------------------------------ *)
 (* one is flat                                                              *)
@@ -76,7 +66,7 @@
         (res_inst_tac [("p","x")] oneE 1),
         (Asm_simp_tac 1),
         (res_inst_tac [("p","y")] oneE 1),
-        (asm_simp_tac (!simpset addsimps dist_less_one) 1),
+        (asm_simp_tac (!simpset addsimps [dist_less_one]) 1),
         (Asm_simp_tac 1)
         ]);
 
@@ -96,3 +86,4 @@
 
 val one_when = map prover ["one_when`x`UU = UU","one_when`x`one = x"];
 
+Addsimps (dist_less_one::dist_eq_one::one_when);
diff -r ce85a2aafc7a -r 045d00d777fb src/HOLCF/Tr1.ML
--- a/src/HOLCF/Tr1.ML	Thu Dec 19 11:58:39 1996 +0100
+++ b/src/HOLCF/Tr1.ML	Thu Dec 19 17:01:47 1996 +0100
@@ -19,7 +19,7 @@
         (rtac classical2 1),
         (rtac defined_sinl 1),
         (rtac not_less2not_eq 1),
-        (resolve_tac dist_less_one 1),
+        (rtac dist_less_one 1),
         (rtac (rep_tr_iso RS subst) 1),
         (rtac (rep_tr_iso RS subst) 1),
         (rtac cfun_arg_cong 1),
@@ -32,7 +32,7 @@
         (rtac classical2 1),
         (rtac defined_sinr 1),
         (rtac not_less2not_eq 1),
-        (resolve_tac dist_less_one 1),
+        (rtac dist_less_one 1),
         (rtac (rep_tr_iso RS subst) 1),
         (rtac (rep_tr_iso RS subst) 1),
         (rtac cfun_arg_cong 1),
@@ -45,7 +45,7 @@
         (rtac classical2 1),
         (rtac (less_ssum4c RS iffD1) 2),
         (rtac not_less2not_eq 1),
-        (resolve_tac dist_less_one 1),
+        (rtac dist_less_one 1),
         (rtac (rep_tr_iso RS subst) 1),
         (rtac (rep_tr_iso RS subst) 1),
         (etac monofun_cfun_arg 1)
@@ -56,7 +56,7 @@
         (rtac classical2 1),
         (rtac (less_ssum4d RS iffD1) 2),
         (rtac not_less2not_eq 1),
-        (resolve_tac dist_less_one 1),
+        (rtac dist_less_one 1),
         (rtac (rep_tr_iso RS subst) 1),
         (rtac (rep_tr_iso RS subst) 1),
         (etac monofun_cfun_arg 1)
@@ -145,14 +145,11 @@
 (* properties of tr_when                                                    *) 
 (* ------------------------------------------------------------------------ *)
 
-fun prover s =  prove_goalw Tr1.thy [tr_when_def,TT_def,FF_def] s
- (fn prems =>
-        [
+fun prover s = prove_goalw Tr1.thy [tr_when_def,TT_def,FF_def] s (fn prems => [
         (Simp_tac 1),
-        (simp_tac (!simpset addsimps [(rep_tr_iso ),
+        (simp_tac (!simpset addsimps [rep_tr_iso,
                 (abs_tr_iso RS allI) RS ((rep_tr_iso RS allI) 
-                RS iso_strict) RS conjunct1]@dist_eq_one)1)
-        ]);
+                RS iso_strict) RS conjunct1]) 1)]);
 
 val tr_when = map prover [
                         "tr_when`x`y`UU = UU",