Examples are adopted to the changes from HOLCF.
Classlib is reduced.
Classlib still uses arities, Classlib will change completely to new
classes of ADTs

--- a/src/HOLCF/ex/Classlib.ML	Mon Feb 17 11:01:10 1997 +0100
+++ b/src/HOLCF/ex/Classlib.ML	Mon Feb 17 11:04:00 1997 +0100
@@ -1,196 +1,2 @@
 open Classlib;
 
-qed_goal "strict_qless" Classlib.thy "(UU .< x) = UU & (x .< UU) = UU"
- (fn prems =>
-	[
-	(simp_tac (HOLCF_ss addsimps [strict_qpo,qless_def,strict_per]) 1)
-	]);
-
-qed_goal "total_qless" Classlib.thy "[|x ~= UU; y ~= UU|] ==> (x .< y) ~= UU"
- (fn prems =>
-	[
-	(cut_facts_tac prems 1),
-	(asm_simp_tac (HOLCF_ss addsimps [qless_def]) 1),
-	(res_inst_tac [("p","x .= y")] trE 1),
-	(asm_simp_tac (HOLCF_ss addsimps [strict_qpo,total_qpo,strict_per,total_per]) 1),
-	(res_inst_tac [("P","x .= y = UU")] notE 1),
-	(etac total_per 1),
-	(atac 1),
-	(atac 1),
-	(asm_simp_tac (HOLCF_ss addsimps [strict_qpo,total_qpo,strict_per,total_per]) 1),
-	(asm_simp_tac (HOLCF_ss addsimps [strict_qpo,total_qpo,strict_per,total_per]) 1)
-	]);
-
-qed_goal "irrefl_qless" Classlib.thy "[|x ~= UU|] ==> (x .< x)=FF"
- (fn prems =>
-	[
-	(cut_facts_tac prems 1),
-	(asm_simp_tac (HOLCF_ss addsimps [total_per,qless_def,refl_per]) 1)
-	]);
-
-qed_goal "asym_qless" Classlib.thy "~((x .< y)=TT & (y .< x)=TT)"
- (fn prems =>
-	[
-	(case_tac "x ~= UU & y ~= UU" 1),
-	(etac conjE 1),
-	(asm_simp_tac (HOLCF_ss addsimps [qless_def]) 1),
-	(res_inst_tac [("p","x .= y")] trE 1),
-	(asm_simp_tac HOLCF_ss 1),
-	(asm_simp_tac HOLCF_ss 1),
-	(asm_simp_tac HOLCF_ss 1),
-	(rtac (sym_per RS subst) 1),
-	(asm_simp_tac HOLCF_ss  1),
-	(rtac (de_Morgan_conj RS iffD1) 1),
-	(res_inst_tac [("Pa","(x .= y)=TT")] classical2 1),
-	(asm_simp_tac (HOLCF_ss addsimps []) 1),
-	(etac conjE 1),
-	(rtac antisym_qpo 1),
-	(atac 1),
-	(atac 1),
-	(subgoal_tac "x=UU Á y=UU" 1),
-	(etac disjE 1),
-	(asm_simp_tac (HOLCF_ss addsimps [strict_qless]) 1),
-	(asm_simp_tac (HOLCF_ss addsimps [strict_qless]) 1),
-	(fast_tac HOL_cs 1)
-	]);
-
-
-qed_goal "qless_iff" Classlib.thy "((x .< y)=TT) = ((x.=y)=FF & (x .<= y)=TT)"
- (fn prems =>
-	[
-	(rtac iffI 1),
-	(asm_full_simp_tac (HOLCF_ss addsimps [qless_def]) 1),
-	(res_inst_tac [("p","x .= y")] trE 1),
-	(res_inst_tac [("P","TT=UU")] notE 1),
-	(simp_tac (HOLCF_ss addsimps []) 1),
-	(rtac trans 1),
-	(etac sym 1),
-	(asm_simp_tac (HOLCF_ss addsimps []) 1),
-	(res_inst_tac [("P","TT=FF")] notE 1),
-	(simp_tac (HOLCF_ss addsimps []) 1),
-	(rtac trans 1),
-	(etac sym 1),
-	(asm_full_simp_tac (HOLCF_ss addsimps []) 1),
-	(rtac conjI 1),
-	(atac 1),
-	(rtac trans 1),
-	(atac 2),
-	(asm_full_simp_tac (HOLCF_ss addsimps []) 1),
-	(asm_full_simp_tac (HOLCF_ss addsimps [qless_def]) 1)
-	]);
-
-qed_goal "trans_qless" Classlib.thy "[|(x .< y)=TT; (y .< z)=TT |] ==> (x .< z)=TT"
- (fn prems =>
-	[
-	(cut_facts_tac prems 1),
-	(rtac (qless_iff RS iffD2) 1),
-	(rtac conjI 1),
-	(dtac (qless_iff RS iffD1) 1),
-	(dtac (qless_iff RS iffD1) 1),
-	(REPEAT (etac conjE 1)),
-	(case_tac "x~=UU & z~=UU" 1),
-	(REPEAT (etac conjE 1)),
-	(res_inst_tac [("p","x .= z")] trE 1),
-	(res_inst_tac [("P","x .= z = UU")] notE 1),
-	(rtac total_per 1),
-	(atac 1),
-	(atac 1),
-	(atac 1),
-	(res_inst_tac [("P","TT = FF")] notE 1),
-	(simp_tac (HOLCF_ss addsimps []) 1),
-	(subgoal_tac "(y.=z)=TT" 1),
-	(rtac trans 1),
-	(etac sym 1),
-	(atac 1),
-	(rtac antisym_qpo 1),
-	(atac 1),
-	(rtac trans_qpo 1),
-	(atac 2),
-	(etac (antisym_qpo_rev RS conjunct2) 1),
-	(atac 1),
-	(dtac (de_Morgan_conj RS iffD1) 1),
-	(etac disjE 1),
-	(dtac notnotD 1),
-	(res_inst_tac [("P","FF=UU")] notE 1),
-	(simp_tac (HOLCF_ss addsimps []) 1),
-	(rtac trans 1),
-	(etac sym 1),
-	(asm_simp_tac (HOLCF_ss addsimps [strict_per]) 1),
-	(dtac notnotD 1),
-	(res_inst_tac [("P","FF=UU")] notE 1),
-	(simp_tac (HOLCF_ss addsimps []) 1),
-	(rtac trans 1),
-	(etac sym 1),
-	(asm_simp_tac (HOLCF_ss addsimps [strict_per]) 1),
-	(dtac (qless_iff RS iffD1) 1),
-	(dtac (qless_iff RS iffD1) 1),
-	(REPEAT (etac conjE 1)),
-	(rtac trans_qpo 1),
-	(atac 1),
-	(atac 1)
-	]);
-
-(*
-
-proof for transitivity depends on property antisym_qpo_rev
-the proof is a bit lengthy
-
-val prems = goal Classlib.thy "[|(x .< y)=TT; (y .< z)=TT |] ==> (x .< z)=TT";
-by (cut_facts_tac prems 1);
-by (rtac (qless_iff RS iffD2) 1);
-by (rtac conjI 1);
-
-by (dtac (qless_iff RS iffD1) 1);
-by (dtac (qless_iff RS iffD1) 1);
-by (REPEAT (etac conjE 1));
-by (case_tac "x~=UU & z~=UU" 1);
-by (REPEAT (etac conjE 1));
-by (res_inst_tac [("p","x .= z")] trE 1);
-by (res_inst_tac [("P","x .= z = UU")] notE 1);
-
-by (rtac total_per 1);
-by (atac 1);
-by (atac 1);
-by (atac 1);
-
-by (res_inst_tac [("P","TT = FF")] notE 1);
-by (simp_tac (HOLCF_ss addsimps []) 1);
-by (subgoal_tac "(y.=z)=TT" 1);
-by (rtac trans 1);
-by (etac sym 1);
-back();
-back();
-back();
-by (atac 1);
-by (rtac antisym_qpo 1);
-by (atac 1);
-by (rtac trans_qpo 1);
-by (atac 2);
-by (etac (antisym_qpo_rev RS conjunct2) 1);
-by (atac 1);
-
-by (dtac (de_Morgan_conj RS iffD1) 1);
-by (etac disjE 1);
-by (dtac notnotD 1);
-by (res_inst_tac [("P","FF=UU")] notE 1);
-by (simp_tac (HOLCF_ss addsimps []) 1);
-by (rtac trans 1);
-by (etac sym 1);
-by (asm_simp_tac (HOLCF_ss addsimps [strict_per]) 1);
-
-by (dtac notnotD 1);
-by (res_inst_tac [("P","FF=UU")] notE 1);
-by (simp_tac (HOLCF_ss addsimps []) 1);
-by (rtac trans 1);
-by (etac sym 1);
-back();
-by (asm_simp_tac (HOLCF_ss addsimps [strict_per]) 1);
-
-by (dtac (qless_iff RS iffD1) 1);
-by (dtac (qless_iff RS iffD1) 1);
-by (REPEAT (etac conjE 1));
-by (rtac trans_qpo 1);
-by (atac 1);
-by (atac 1);
-val trans_qless = result();
-*)

--- a/src/HOLCF/ex/Classlib.thy	Mon Feb 17 11:01:10 1997 +0100
+++ b/src/HOLCF/ex/Classlib.thy	Mon Feb 17 11:04:00 1997 +0100
@@ -5,13 +5,14 @@
 
 Introduce various type classes
 
-The 8bit package is needed for this theory
-
-The type void of HOLCF/Void.thy is a witness for all the introduced classes.
+The type void of HOLCF/One.thy is a witness for all the introduced classes.
 Inspect theory Witness.thy for all the proofs. 
 
-the trivial instance for ++ -- ** // is LAM x y.(UU::void) 
-the trivial instance for .= and .<=  is LAM x y.(UU::tr)
+!!! Witness and Claslib have to be adapted to axclasses !!!
+------------------------------------------------------------
+
+the trivial instance for ++ -- ** // is circ
+the trivial instance for .= and .<=  is bullet
 
 the class hierarchy is as follows
 
@@ -42,7 +43,7 @@
  
 classes cplus < pcpo	
 
-arities void :: cplus
+arities lift :: (term)cplus
 
 ops curried 
 	"++"	:: "'a::cplus -> 'a -> 'a"		(cinfixl 65)
@@ -56,7 +57,7 @@
  
 classes cminus < pcpo	
 
-arities void :: cminus
+arities lift :: (term)cminus
 
 ops curried 
 	"--"	:: "'a::cminus -> 'a -> 'a"		(cinfixl 65)
@@ -69,7 +70,7 @@
  
 classes ctimes < pcpo	
 
-arities void :: ctimes
+arities lift :: (term)ctimes
 
 ops curried 
 	"**"	:: "'a::ctimes -> 'a -> 'a"		(cinfixl 70)
@@ -82,7 +83,7 @@
  
 classes cdiv < pcpo	
 
-arities void :: cdiv
+arities lift :: (term)cdiv
 
 ops curried 
 	"//"	:: "'a::cdiv -> 'a -> 'a"		(cinfixl 70)
@@ -95,7 +96,7 @@
  
 classes per < pcpo	
 
-arities void :: per
+arities lift :: (term)per
 
 ops curried 
 	".="	:: "'a::per -> 'a -> tr"	(cinfixl 55)
@@ -106,7 +107,7 @@
 
 strict_per	"(UU .= x) = UU & (x .= UU) = UU"
 total_per	"[|x ~= UU; y ~= UU|] ==> (x .= y) ~= UU"
-flat_per	"flat (UU::'a::per)"
+flat_per	"flat (x::'a::per)"
 
 sym_per		"(x .= y) = (y .= x)"
 trans_per	"[| (x .= y)=TT; (y .= z)=TT |] ==> (x .= z)=TT"
@@ -118,7 +119,7 @@
  
 classes equiv < per 	
 
-arities void :: equiv
+arities lift :: (term)equiv
 
 rules 
 
@@ -131,65 +132,11 @@
  
 classes eq < equiv  	
 
-arities void :: eq
+arities lift :: (term)eq
 
 rules 
 
 weq	"[| (x::'a::eq) ~= UU; y ~= UU |] ==> 
 	 (x = y --> (x .=y) = TT) & (x ~= y --> (x .= y)=FF)"
 
-(* -------------------------------------------------------------------- *)
-
-(* -------------------------------------------------------------------- *)
-(* class qpo with characteristic constant .<=                           *)
-(*  .<= is a partial order wrt an equivalence                           *)
- 
-classes qpo < equiv	
-
-arities void :: qpo
-
-ops curried 
-	".<="	:: "'a::qpo -> 'a -> tr"	(cinfixl 55)
-syntax (symbols)
-	"op .<=":: "'a::qpo => 'a => tr"	(infixl "\\<preceq>" 55)
-rules 
-
-strict_qpo	"(UU .<= x) = UU & (x .<= UU) = UU"
-total_qpo	"[|x ~= UU; y ~= UU|] ==> (x .<= y) ~= UU"
-
-refl_qpo	"[|x ~= UU|] ==> (x .<= x)=TT"
-antisym_qpo	"[| (x .<= y)=TT; (y .<= x)=TT |] ==> (x .=  y)=TT"
-trans_qpo	"[| (x .<= y)=TT; (y .<= z)=TT |] ==> (x .<= z)=TT"
-
-antisym_qpo_rev	"(x .= y)=TT ==> (x .<= y)=TT & (y .<= x)=TT" 
-
-(* -------------------------------------------------------------------- *)
-
-(* -------------------------------------------------------------------- *)
-(* irreflexive part .< defined via .<=                                  *)
- 
-ops curried 
-	".<"	:: "'a::qpo -> 'a -> tr"	(cinfixl 55)
-syntax (symbols)
-	"op .<"	:: "'a::qpo => 'a => tr"	(infixl "\\<prec>" 55)
-
-defs
-
-qless_def	"(op .<) Ú LAM x y.If x .= y then FF else x .<= y fi"
-
-(* -------------------------------------------------------------------- *)
-
-(* -------------------------------------------------------------------- *)
-(* class qlinear is a refinement of of class qpo                        *)
- 
-classes qlinear < qpo  	
-
-arities void :: qlinear
-
-rules 
-
-qlinear	"[|(x::'a::qlinear) ~= UU; y ~= UU|] ==> (x .<= y)=TT Á (y .<= x)=TT "
-
-(* -------------------------------------------------------------------- *)
-
 end

--- a/src/HOLCF/ex/Hoare.ML	Mon Feb 17 11:01:10 1997 +0100
+++ b/src/HOLCF/ex/Hoare.ML	Mon Feb 17 11:04:00 1997 +0100
@@ -95,7 +95,7 @@
  (fn prems =>
         [
         (cut_facts_tac prems 1),
-        (etac (flat_tr RS flat_codom RS disjE) 1),
+        (etac (flat_flat RS flat_codom RS disjE) 1),
         (atac 1),
         (etac spec 1)
         ]);
@@ -323,7 +323,7 @@
  (fn prems =>
         [
         (cut_facts_tac prems 1),
-        (rtac (flat_tr RS flat_codom) 1),
+        (rtac (flat_flat RS flat_codom) 1),
         (res_inst_tac [("t","x1")] (iterate_0 RS subst) 1),
         (etac spec 1)
         ]);

--- a/src/HOLCF/ex/Loop.ML	Mon Feb 17 11:01:10 1997 +0100
+++ b/src/HOLCF/ex/Loop.ML	Mon Feb 17 11:04:00 1997 +0100
@@ -57,7 +57,7 @@
         (asm_simp_tac HOLCF_ss 1),
         (stac while_unfold 1),
         (res_inst_tac [("s","UU"),("t","b`UU")]ssubst 1),
-        (etac (flat_tr RS flat_codom RS disjE) 1),
+        (etac (flat_flat RS flat_codom RS disjE) 1),
         (atac 1),
         (etac spec 1),
         (simp_tac HOLCF_ss 1),
@@ -92,7 +92,7 @@
         (rtac step_def2 1),
         (asm_simp_tac HOLCF_ss 1),
         (etac exE 1),
-        (etac (flat_tr RS flat_codom RS disjE) 1),
+        (etac (flat_flat RS flat_codom RS disjE) 1),
         (asm_simp_tac HOLCF_ss 1),
         (asm_simp_tac HOLCF_ss 1)
         ]);

--- a/src/HOLCF/ex/Loop.thy	Mon Feb 17 11:01:10 1997 +0100
+++ b/src/HOLCF/ex/Loop.thy	Mon Feb 17 11:04:00 1997 +0100
@@ -6,10 +6,9 @@
 Theory for a loop primitive like while
 *)
 
-Loop = Tr2 +
+Loop = Tr +
 
 consts
-
         step  :: "('a -> tr)->('a -> 'a)->'a->'a"
         while :: "('a -> tr)->('a -> 'a)->'a->'a"
 

--- a/src/HOLCF/ex/Witness.ML	Mon Feb 17 11:01:10 1997 +0100
+++ b/src/HOLCF/ex/Witness.ML	Mon Feb 17 11:04:00 1997 +0100
@@ -4,7 +4,7 @@
 (* classes cplus, cminus, ctimes, cdiv introduce 
    characteristic constants  o+ o- o* o/
 
-	"bullet":: "void -> void -> void"
+	"circ":: "one -> one -> one"
 
    is the witness for o+ o- o* o/	
 
@@ -18,9 +18,9 @@
 
    The witness for these is 
 
-	"cric"	:: "void -> void -> tr"			(cinfixl 55)
+	"bullet":: "one -> one -> tr"			(cinfixl 55)
 
-   the classes equiv, eq, qlinear impose additional axioms
+   the classes equiv, eq, impose additional axioms
 *)
 
 (* -------------------------------------------------------------------- *)
@@ -45,88 +45,85 @@
 
 characteristic axioms of class eq:
 
-weq	"[|(x::'a::eq) ~= UU; y ~= UU|] ==> (x = y --> (x .= y)=TT) & (x ~= y --> Çx .= yÈ)"
+weq	"[|(x::'a::eq)~=UU; y~=UU|] ==> (x=y --> (x.=y)=TT) & (x~=y --> Çx.=yÈ)"
 
 
    --------------------------------------------------------------------
 
-characteristic axioms of class qpo:
-
-strict_qpo	"(UU .<= x) = UU & (x .<= UU) = UU"
-total_qpo	"[|x ~= UU; y ~= UU|] ==> (x .<= y) ~= UU"
-
-refl_qpo	"[|x ~= UU|] ==> (x .<= x)=TT"
-antisym_qpo	"[|(x .<= y)=TT; (y .<= x)=TT |] ==> (x .= y)=TT"
-trans_qpo	"[|(x .<= y)=TT; (y .<= z)=TT |] ==> (x .<= z)=TT"
-antisym_qpo_rev	" (x .= y)=TT ==> (x .<= y)=TT & (y .<= x)=TT" 
-
-   --------------------------------------------------------------------
-
-characteristic axioms of class qlinear:
-
-qlinear	"[|(x::'a::qlinear) ~= UU; y ~= UU|] ==> (x .<= y)=TT | (y .<= x)=TT "
-
 *)
 
 (* strict_per, strict_qpo *)
-val prems = goal thy "(UU circ x) = UU & (x circ UU) = UU";
-by (simp_tac (HOLCF_ss addsimps [circ_def]) 1);
+goalw thy [bullet_def] "(UU bullet x) = UU & (x bullet UU) = UU";
+by (simp_tac (!simpset addsimps [flift1_def,flift2_def,o_def]) 1);
+by (lift.induct_tac "x" 1);
+auto();
 result();
 
 (* total_per, total_qpo *)
-val prems = goal thy "[|x ~= UU; y ~= UU|] ==> (x circ y) ~= UU";
+val prems = goal thy "[|x~=UU; y~=UU|] ==> (x bullet y) ~= UU";
+by (subgoal_tac "x~=UU&y~=UU-->(x bullet y) ~= UU" 1);
 by (cut_facts_tac prems 1);
-by (etac notE 1);
-by (rtac unique_void2 1);
+by (fast_tac HOL_cs 1);
+by (simp_tac (!simpset addsimps [bullet_def,flift1_def,flift2_def,o_def]) 1);
+by (lift.induct_tac "x" 1);
+by (fast_tac HOL_cs 1);
+by (lift.induct_tac "y" 1);
+auto();
 result();
 
 (* flat_per *)
 
-val prems = goal thy "flat (UU::void)";
-by (rtac flat_void 1);
+goal thy "flat (x::one)";
+by (rtac flat_flat 1);
 result();
 
 (* sym_per *)  
-val prems = goal thy "(x circ y) = (y circ x)";
-by (simp_tac (HOLCF_ss addsimps [circ_def]) 1);
+goalw thy [bullet_def] "(x bullet y) = (y bullet x)";
+by (simp_tac (!simpset addsimps [bullet_def,flift1_def,flift2_def,o_def]) 1);
+by (lift.induct_tac "x" 1);
+by (lift.induct_tac "y" 2);
+by (lift.induct_tac "y" 1);
+auto();
 result();
 
 (* trans_per, trans_qpo *)
-val prems = goal thy "[|(x bullet y)=TT; (y bullet z)=TT |] ==> (x bullet z)=TT";
+val prems = goal thy "[|(x bullet y)=TT; (y bullet z)=TT|] ==>(x bullet z)=TT";
+by (subgoal_tac "(x bullet y)=TT&(y bullet z)=TT-->(x bullet z)=TT" 1);
 by (cut_facts_tac prems 1);
-by (asm_full_simp_tac (HOLCF_ss addsimps [bullet_def]) 1);
+by (fast_tac HOL_cs 1);
+by (simp_tac (!simpset addsimps [bullet_def,flift1_def,flift2_def,o_def]) 1);
+by (lift.induct_tac "x" 1);
+by (lift.induct_tac "y" 2);
+by (lift.induct_tac "y" 1);
+by (lift.induct_tac "z" 4);
+by (lift.induct_tac "z" 3);
+by (lift.induct_tac "z" 2);
+by (lift.induct_tac "z" 1);
+auto();
 result();
 
 (* refl_per *)
-val prems = goal thy "[|(x::void) ~= UU|] ==> (x bullet x)=TT";
+val prems = goal thy "x ~= UU ==> (x bullet x)=TT";
+by (subgoal_tac "x ~= UU --> (x bullet x)=TT" 1);
 by (cut_facts_tac prems 1);
-by (etac notE 1);
-by (rtac unique_void2 1);
-result();
+by (fast_tac HOL_cs 1);
+by (simp_tac (!simpset addsimps [bullet_def,flift1_def,flift2_def,o_def]) 1);
+by (lift.induct_tac "x" 1);
+auto();
+qed "refl_per_one";
 
 (* weq *)
 val prems = goal thy 
-	"[|(x::void) ~= UU; y ~= UU|] ==> (x = y --> (x bullet y)=TT) & (x ~= y --> (x bullet y)=FF)";
+	"[|x~=UU; y~=UU|]==>(x=y-->(x bullet y)=TT)&(x~=y-->(x bullet y)=FF)";
+by(subgoal_tac"x~=UU&y~=UU-->(x=y-->(x bullet y)=TT)&(x~=y-->(x bullet y)=FF)"1);
 by (cut_facts_tac prems 1);
-by (etac notE 1);
-by (rtac unique_void2 1);
-result();
-
-(* antisym_qpo *)
-val prems = goal thy "[|(x bullet y)=TT; (y bullet x)=TT |] ==> (x bullet y)=TT";
-by (cut_facts_tac prems 1);
-by (asm_full_simp_tac (HOLCF_ss addsimps [bullet_def]) 1);
+by (fast_tac HOL_cs 1);
+by (lift.induct_tac "x" 1);
+by (lift.induct_tac "y" 2);
+by (lift.induct_tac "y" 1);
+auto();
+br refl_per_one 1;
+auto();
+by (simp_tac (!simpset addsimps [bullet_def,flift1_def,flift2_def,o_def]) 1);
 result();
 
-(* antisym_qpo_rev *)
-val prems = goal thy "(x bullet y)=TT ==> (x bullet y)=TT & (y bullet x)=TT";
-by (cut_facts_tac prems 1);
-by (asm_full_simp_tac (HOLCF_ss addsimps [bullet_def]) 1);
-
-(* qlinear *)
-val prems = goal thy 
-	"[|(x::void) ~= UU; y ~= UU|] ==> (x bullet y)=TT | (y bullet x)=TT ";
-by (cut_facts_tac prems 1);
-by (etac notE 1);
-by (rtac unique_void2 1);
-result();

--- a/src/HOLCF/ex/Witness.thy	Mon Feb 17 11:01:10 1997 +0100
+++ b/src/HOLCF/ex/Witness.thy	Mon Feb 17 11:04:00 1997 +0100
@@ -1,29 +1,24 @@
 (*  Title:      FOCUS/Witness.thy
-    ID:         $ $
+    ID:         $Id$
     Author:     Franz Regensburger
     Copyright   1995 Technical University Munich
 
 Witnesses for introduction of type cleasse in theory Classlib
 
-The 8bit package is needed for this theory
+The type one of HOLCF/One.thy is a witness for all the introduced classes.
 
-The type void of HOLCF/Void.thy is a witness for all the introduced classes.
-
-the trivial instance for ++ -- ** // is LAM x y.(UU::void) 
-the trivial instance for .= and .<=  is LAM x y.(UU::tr)
+the trivial instance for ++ -- ** // is circ 
+the trivial instance for .= and .<=  is bullet
 
 *)
 
 Witness = HOLCF +
 
 ops curried 
-	"circ"	:: "void -> void -> void"		(cinfixl 65)
-	"bullet":: "void -> void -> tr"			(cinfixl 55)
+	"bullet":: "one -> one -> tr"			(cinfixl 55)
 
 defs 
 
-circ_def	"(op circ) Ú (LAM x y.UU)"
-
-bullet_def	"(op bullet) Ú (LAM x y.UU)"
+bullet_def	"(op bullet) Ú flift1(flift2 o (op =))"
 
 end