diff -r 2c38796b33b9 -r ee4dfce170a0 src/HOLCF/One.ML
--- a/src/HOLCF/One.ML	Sat Feb 15 18:24:05 1997 +0100
+++ b/src/HOLCF/One.ML	Mon Feb 17 10:57:11 1997 +0100
@@ -1,9 +1,9 @@
 (*  Title:      HOLCF/One.ML
     ID:         $Id$
-    Author:     Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
+    Author:     Oscar Slotosch
+    Copyright   1997 Technische Universitaet Muenchen
 
-Lemmas for One.thy 
+Lemmas for One.thy
 *)
 
 open One;
@@ -12,24 +12,17 @@
 (* Exhaustion and Elimination for type one                                  *)
 (* ------------------------------------------------------------------------ *)
 
-qed_goalw "Exh_one" One.thy [one_def] "z=UU | z = one"
+qed_goalw "Exh_one" thy [ONE_def] "t=UU | t = ONE"
  (fn prems =>
         [
-        (res_inst_tac [("p","rep_one`z")] upE1 1),
-        (rtac disjI1 1),
-        (rtac ((abs_one_iso RS allI) RS ((rep_one_iso RS allI) RS iso_strict )
-                RS conjunct2 RS subst) 1),
-        (rtac (abs_one_iso RS subst) 1),
-        (etac cfun_arg_cong 1),
-        (rtac disjI2 1),
-        (rtac (abs_one_iso RS subst) 1),
-        (rtac cfun_arg_cong 1),
-        (rtac (unique_void2 RS subst) 1),
-        (atac 1)
-        ]);
+	(lift.induct_tac "t" 1),
+	(fast_tac HOL_cs 1),
+	(Simp_tac 1),
+	(rtac unit_eq 1)
+	]);
 
-qed_goal "oneE" One.thy
-        "[| p=UU ==> Q; p = one ==>Q|] ==>Q"
+qed_goal "oneE" thy
+        "[| p=UU ==> Q; p = ONE ==>Q|] ==>Q"
  (fn prems =>
         [
         (rtac (Exh_one RS disjE) 1),
@@ -37,53 +30,22 @@
         (eresolve_tac prems 1)
         ]);
 
+(* ------------------------------------------------------------------------ *) 
+(* tactic for one-thms                                                      *)
+(* ------------------------------------------------------------------------ *)
+
+fun prover t = prove_goalw thy [ONE_def] t
+ (fn prems =>
+        [
+	(asm_simp_tac (!simpset addsimps [inst_lift_po]) 1)
+	]);
+
 (* ------------------------------------------------------------------------ *)
 (* distinctness for type one : stored in a list                             *)
 (* ------------------------------------------------------------------------ *)
 
-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)]);
-
-qed_goal "dist_eq_one" One.thy "one~=UU" (fn prems => [
-        (rtac not_less2not_eq 1),
-        (rtac dist_less_one 1)]);
-
-(* ------------------------------------------------------------------------ *)
-(* one is flat                                                              *)
-(* ------------------------------------------------------------------------ *)
+val dist_less_one = map prover ["~ONE << UU"];
 
-qed_goalw "flat_one" One.thy [flat_def] "flat one"
- (fn prems =>
-        [
-        (rtac allI 1),
-        (rtac allI 1),
-        (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 1)
-        ]);
-
+val dist_eq_one = map prover ["ONE~=UU","UU~=ONE"];
 
-(* ------------------------------------------------------------------------ *)
-(* properties of one_when                                                   *)
-(* here I tried a generic prove procedure                                   *)
-(* ------------------------------------------------------------------------ *)
-
-fun prover s =  prove_goalw One.thy [one_when_def,one_def] s
- (fn prems =>
-        [
-        (simp_tac (!simpset addsimps [(rep_one_iso ),
-        (abs_one_iso RS allI) RS ((rep_one_iso RS allI) 
-        RS iso_strict) RS conjunct1] )1)
-        ]);
-
-val one_when = map prover ["one_when`x`UU = UU","one_when`x`one = x"];
-
-Addsimps (dist_less_one::dist_eq_one::one_when);
+Addsimps (dist_less_one@dist_eq_one);