# HG changeset patch
# User berghofe
# Date 901280667 -7200
# Node ID 704dd3a6d47d80de718aac1bd22dd01349ee92f5
# Parent  8ceaa19f771712c07d8f073e1877b71e9d08104c
Adapted to new datatype package.

diff -r 8ceaa19f7717 -r 704dd3a6d47d src/HOLCF/Discrete0.thy
--- a/src/HOLCF/Discrete0.thy	Fri Jul 24 13:39:47 1998 +0200
+++ b/src/HOLCF/Discrete0.thy	Fri Jul 24 13:44:27 1998 +0200
@@ -6,9 +6,9 @@
 Discrete CPOs
 *)
 
-Discrete0 = Cont +
+Discrete0 = Cont + Datatype +
 
-datatype 'a discr = Discr 'a
+datatype 'a discr = Discr "'a :: term"
 
 instance discr :: (term)sq_ord
 
diff -r 8ceaa19f7717 -r 704dd3a6d47d src/HOLCF/Discrete1.ML
--- a/src/HOLCF/Discrete1.ML	Fri Jul 24 13:39:47 1998 +0200
+++ b/src/HOLCF/Discrete1.ML	Fri Jul 24 13:44:27 1998 +0200
@@ -13,7 +13,7 @@
 
 Goalw [chain]
  "!!S::nat=>('a::term)discr. chain S ==> S i = S 0";
-by (nat_ind_tac "i" 1);
+by (induct_tac "i" 1);
 by (rtac refl 1);
 by (etac subst 1);
 by (rtac sym 1);
diff -r 8ceaa19f7717 -r 704dd3a6d47d src/HOLCF/Fix.ML
--- a/src/HOLCF/Fix.ML	Fri Jul 24 13:39:47 1998 +0200
+++ b/src/HOLCF/Fix.ML	Fri Jul 24 13:44:27 1998 +0200
@@ -12,24 +12,10 @@
 (* derive inductive properties of iterate from primitive recursion          *)
 (* ------------------------------------------------------------------------ *)
 
-qed_goal "iterate_0" thy "iterate 0 F x = x"
- (fn prems =>
-        [
-        (resolve_tac (nat_recs iterate_def) 1)
-        ]);
-
-qed_goal "iterate_Suc" thy "iterate (Suc n) F x  = F`(iterate n F x)"
- (fn prems =>
-        [
-        (resolve_tac (nat_recs iterate_def) 1)
-        ]);
-
-Addsimps [iterate_0, iterate_Suc];
-
 qed_goal "iterate_Suc2" thy "iterate (Suc n) F x = iterate n F (F`x)"
  (fn prems =>
         [
-        (nat_ind_tac "n" 1),
+        (induct_tac "n" 1),
         (Simp_tac 1),
         (stac iterate_Suc 1),
         (stac iterate_Suc 1),
@@ -49,7 +35,7 @@
         (cut_facts_tac prems 1),
         (strip_tac 1),
         (Simp_tac 1),
-        (nat_ind_tac "i" 1),
+        (induct_tac "i" 1),
         (Asm_simp_tac 1),
         (Asm_simp_tac 1),
         (etac monofun_cfun_arg 1)
@@ -103,7 +89,7 @@
         (rtac chain_iterate 1),
         (rtac ub_rangeI 1),
         (strip_tac 1),
-        (nat_ind_tac "i" 1),
+        (induct_tac "i" 1),
         (Asm_simp_tac 1),
         (Asm_simp_tac 1),
         (res_inst_tac [("t","x")] subst 1),
@@ -120,7 +106,7 @@
  (fn prems =>
         [
         (strip_tac 1),
-        (nat_ind_tac "i" 1),
+        (induct_tac "i" 1),
         (Asm_simp_tac 1),
         (Asm_simp_tac 1),
         (rtac (less_fun RS iffD2) 1),
@@ -141,7 +127,7 @@
  (fn prems =>
         [
         (strip_tac 1),
-        (nat_ind_tac "i" 1),
+        (induct_tac "i" 1),
         (Asm_simp_tac 1),
         (rtac (lub_const RS thelubI RS sym) 1),
         (Asm_simp_tac 1),
@@ -185,7 +171,7 @@
         [
         (rtac monofunI 1),
         (strip_tac 1),
-        (nat_ind_tac "n" 1),
+        (induct_tac "n" 1),
         (Asm_simp_tac 1),
         (Asm_simp_tac 1),
         (etac monofun_cfun_arg 1)
@@ -196,7 +182,7 @@
         [
         (rtac contlubI 1),
         (strip_tac 1),
-        (nat_ind_tac "n" 1),
+        (induct_tac "n" 1),
         (Simp_tac 1),
         (Simp_tac 1),
         (res_inst_tac [("t","iterate n F (lub(range(%u. Y u)))"),
@@ -493,7 +479,7 @@
         (etac admD 1),
         (rtac chain_iterate 1),
         (rtac allI 1),
-        (nat_ind_tac "i" 1),
+        (induct_tac "i" 1),
         (stac iterate_0 1),
         (atac 1),
         (stac iterate_Suc 1),
diff -r 8ceaa19f7717 -r 704dd3a6d47d src/HOLCF/Fix.thy
--- a/src/HOLCF/Fix.thy	Fri Jul 24 13:39:47 1998 +0200
+++ b/src/HOLCF/Fix.thy	Fri Jul 24 13:44:27 1998 +0200
@@ -18,9 +18,12 @@
 adm		:: "('a::cpo=>bool)=>bool"
 admw		:: "('a=>bool)=>bool"
 
+primrec
+  iterate_0   "iterate 0 F x = x"
+  iterate_Suc "iterate (Suc n) F x  = F`(iterate n F x)"
+
 defs
 
-iterate_def   "iterate n F c == nat_rec c (%n x. F`x) n"
 Ifix_def      "Ifix F == lub(range(%i. iterate i F UU))"
 fix_def       "fix == (LAM f. Ifix f)"
 
diff -r 8ceaa19f7717 -r 704dd3a6d47d src/HOLCF/IMP/Denotational.ML
--- a/src/HOLCF/IMP/Denotational.ML	Fri Jul 24 13:39:47 1998 +0200
+++ b/src/HOLCF/IMP/Denotational.ML	Fri Jul 24 13:44:27 1998 +0200
@@ -18,7 +18,7 @@
 
 Goalw [dlift_def]
  "(dlift f`l = Def y) = (? x. l = Def x & f`(Discr x) = Def y)";
-by (simp_tac (simpset() addsplits [split_lift_case]) 1);
+by (simp_tac (simpset() addsplits [Lift1.lift.split]) 1);
 qed "dlift_is_Def";
 Addsimps [dlift_is_Def];
 
@@ -29,7 +29,7 @@
 qed_spec_mp "eval_implies_D";
 
 Goal "!s t. D c`(Discr s) = (Def t) --> <c,s> -c-> t";
-by (com.induct_tac "c" 1);
+by (induct_tac "c" 1);
     by (fast_tac ((HOL_cs addSIs evalc.intrs) addss simpset()) 1);
    by (fast_tac ((HOL_cs addSIs evalc.intrs) addss simpset()) 1);
   by (fast_tac ((HOL_cs addSIs evalc.intrs) addss simpset()) 1);
diff -r 8ceaa19f7717 -r 704dd3a6d47d src/HOLCF/IMP/Denotational.thy
--- a/src/HOLCF/IMP/Denotational.thy	Fri Jul 24 13:39:47 1998 +0200
+++ b/src/HOLCF/IMP/Denotational.thy	Fri Jul 24 13:44:27 1998 +0200
@@ -14,7 +14,7 @@
 
 consts D :: "com => state discr -> state lift"
 
-primrec D com
+primrec
   "D(SKIP) = (LAM s. Def(undiscr s))"
   "D(X := a) = (LAM s. Def((undiscr s)[X := a(undiscr s)]))"
   "D(c0 ; c1) = (dlift(D c1) oo (D c0))"
diff -r 8ceaa19f7717 -r 704dd3a6d47d src/HOLCF/IOA/ABP/Abschannel_finite.thy
--- a/src/HOLCF/IOA/ABP/Abschannel_finite.thy	Fri Jul 24 13:39:47 1998 +0200
+++ b/src/HOLCF/IOA/ABP/Abschannel_finite.thy	Fri Jul 24 13:44:27 1998 +0200
@@ -28,7 +28,6 @@
 reverse        :: 'a list => 'a list
 
 primrec
-  reverse List.list  
   reverse_Nil  "reverse([]) = []"
   reverse_Cons "reverse(x#xs) =  reverse(xs)@[x]"
 
diff -r 8ceaa19f7717 -r 704dd3a6d47d src/HOLCF/IOA/ABP/Action.thy
--- a/src/HOLCF/IOA/ABP/Action.thy	Fri Jul 24 13:39:47 1998 +0200
+++ b/src/HOLCF/IOA/ABP/Action.thy	Fri Jul 24 13:44:27 1998 +0200
@@ -6,7 +6,7 @@
 The set of all actions of the system
 *)
 
-Action = Packet +
+Action = Packet + Datatype +
 datatype 'm action = Next | S_msg ('m) | R_msg ('m)
                    | S_pkt ('m packet) | R_pkt ('m packet) 
                    | S_ack (bool) | R_ack (bool)         
diff -r 8ceaa19f7717 -r 704dd3a6d47d src/HOLCF/IOA/ABP/Correctness.ML
--- a/src/HOLCF/IOA/ABP/Correctness.ML	Fri Jul 24 13:39:47 1998 +0200
+++ b/src/HOLCF/IOA/ABP/Correctness.ML	Fri Jul 24 13:44:27 1998 +0200
@@ -46,10 +46,10 @@
  by (rtac iffI 1);
  by (subgoal_tac "(l~=[]) --> (reduce(l)~=[])" 1);
  by (Fast_tac 1); 
- by (List.list.induct_tac "l" 1);
+ by (induct_tac "l" 1);
  by (Simp_tac 1);
  by (Simp_tac 1);
- by (rtac (split_list_case RS iffD2) 1);
+ by (rtac (list.split RS iffD2) 1);
  by (Asm_full_simp_tac 1);
  by (REPEAT (rtac allI 1)); 
  by (rtac impI 1); 
@@ -60,7 +60,7 @@
 val l_iff_red_nil = result();
 
 Goal "s~=[] --> hd(s)=hd(reduce(s))";
-by (List.list.induct_tac "s" 1);
+by (induct_tac "s" 1);
 by (Simp_tac 1);
 by (case_tac "list =[]" 1);
 by (Asm_full_simp_tac 1);
@@ -68,7 +68,7 @@
 by (rotate 1 1);
 by (asm_full_simp_tac list_ss 1);
 by (Simp_tac 1);
-by (rtac (split_list_case RS iffD2) 1);
+by (rtac (list.split RS iffD2) 1);
 by (asm_full_simp_tac list_ss 1);
 by (REPEAT (rtac allI 1)); 
  by (rtac impI 1); 
@@ -80,7 +80,7 @@
 
 (* to be used in the following Lemma *)
 Goal "l~=[] --> reverse(reduce(l))~=[]";
-by (List.list.induct_tac "l" 1);
+by (induct_tac "l" 1);
 by (Simp_tac 1);
 by (case_tac "list =[]" 1);
 by (asm_full_simp_tac (simpset() addsimps [reverse_Cons]) 1);
@@ -100,7 +100,7 @@
 Goal "!!l.[| l~=[] |] ==>   \
 \   hd(reverse(reduce(a#l))) = hd(reverse(reduce(l)))";
  by (Simp_tac 1);
- by (rtac (split_list_case RS iffD2) 1);
+ by (rtac (list.split RS iffD2) 1);
  by (asm_full_simp_tac list_ss 1);
  by (REPEAT (rtac allI 1)); 
  by (rtac impI 1); 
@@ -119,7 +119,7 @@
 by (stac split_if 1);
 by (rtac conjI 1);
 (* --> *)
-by (List.list.induct_tac "l" 1);
+by (induct_tac "l" 1);
 by (Simp_tac 1);
 by (case_tac "list=[]" 1);
  by (asm_full_simp_tac (simpset() addsimps [reverse_Nil,reverse_Cons]) 1);
@@ -132,7 +132,7 @@
 by (asm_full_simp_tac (impl_ss addsimps [last_ind_on_first,l_iff_red_nil]) 1);
 (* <-- *)
 by (simp_tac (simpset() addsimps [and_de_morgan_and_absorbe,l_iff_red_nil]) 1);
-by (List.list.induct_tac "l" 1);
+by (induct_tac "l" 1);
 by (Simp_tac 1);
 by (case_tac "list=[]" 1);
 by (cut_inst_tac [("l","list")] cons_not_nil 2);
@@ -174,7 +174,7 @@
 (* ---------------- main-part ------------------- *)
 by (REPEAT (rtac allI 1));
 by (rtac imp_conj_lemma 1);
-by (abs_action.induct_tac "a" 1);
+by (induct_tac "a" 1);
 (* ----------------- 2 cases ---------------------*)
 by (ALLGOALS (simp_tac (simpset() addsimps [externals_def])));
 (* fst case --------------------------------------*)
@@ -219,7 +219,7 @@
 (* main-part *)
 by (REPEAT (rtac allI 1));
 by (rtac imp_conj_lemma 1);
-by (Action.action.induct_tac "a" 1);
+by (induct_tac "a" 1);
 (* 7 cases *)
 by (ALLGOALS (simp_tac (simpset() addsimps [externals_def] addsplits [split_if])));
 qed"sender_unchanged";
@@ -235,7 +235,7 @@
 (* main-part *)
 by (REPEAT (rtac allI 1));
 by (rtac imp_conj_lemma 1);
-by (Action.action.induct_tac "a" 1);
+by (induct_tac "a" 1);
 (* 7 cases *)
 by (ALLGOALS(simp_tac (simpset() addsimps [externals_def] addsplits [split_if])));
 qed"receiver_unchanged";
@@ -250,7 +250,7 @@
 (* main-part *)
 by (REPEAT (rtac allI 1));
 by (rtac imp_conj_lemma 1);
-by (Action.action.induct_tac "a" 1);
+by (induct_tac "a" 1);
 (* 7 cases *)
 by (ALLGOALS(simp_tac (simpset() addsimps [externals_def] addsplits [split_if])));
 qed"env_unchanged";
@@ -259,7 +259,7 @@
 Goal "compatible srch_ioa rsch_ioa"; 
 by (simp_tac (simpset() addsimps [compatible_def,Int_def,empty_def]) 1);
 by (rtac set_ext 1);
-by (Action.action.induct_tac "x" 1);
+by (induct_tac "x" 1);
 by (ALLGOALS(Simp_tac));
 val compat_single_ch = result();
 
@@ -267,7 +267,7 @@
 Goal "compatible srch_fin_ioa rsch_fin_ioa"; 
 by (simp_tac (simpset() addsimps [compatible_def,Int_def,empty_def]) 1);
 by (rtac set_ext 1);
-by (Action.action.induct_tac "x" 1);
+by (induct_tac "x" 1);
 by (ALLGOALS(Simp_tac));
 val compat_single_fin_ch = result();
 
@@ -284,7 +284,7 @@
                            Int_def]) 1);
 by (Simp_tac 1);
 by (rtac set_ext 1);
-by (Action.action.induct_tac "x" 1);
+by (induct_tac "x" 1);
 by (ALLGOALS Simp_tac);
 val compat_rec = result();
 
@@ -293,7 +293,7 @@
 by (simp_tac (ss addsimps [empty_def,compatible_def,asig_of_par,asig_comp_def,actions_def,Int_def]) 1);
 by (Simp_tac 1);
 by (rtac set_ext 1);
-by (Action.action.induct_tac "x" 1);
+by (induct_tac "x" 1);
 by (ALLGOALS Simp_tac);
 val compat_rec_fin =result();
 
@@ -302,7 +302,7 @@
 by (simp_tac (ss addsimps [empty_def,compatible_def,asig_of_par,asig_comp_def,actions_def,Int_def]) 1);
 by (Simp_tac 1);
 by (rtac set_ext 1);
-by (Action.action.induct_tac "x" 1);
+by (induct_tac "x" 1);
 by (ALLGOALS(Simp_tac));
 val compat_sen=result();
 
@@ -311,7 +311,7 @@
 by (simp_tac (ss addsimps [empty_def,  compatible_def,asig_of_par,asig_comp_def,actions_def,Int_def]) 1);
 by (Simp_tac 1);
 by (rtac set_ext 1);
-by (Action.action.induct_tac "x" 1);
+by (induct_tac "x" 1);
 by (ALLGOALS(Simp_tac));
 val compat_sen_fin =result();
 
@@ -320,7 +320,7 @@
 by (simp_tac (ss addsimps [empty_def,compatible_def,asig_of_par,asig_comp_def,actions_def,Int_def]) 1);
 by (Simp_tac 1);
 by (rtac set_ext 1);
-by (Action.action.induct_tac "x" 1);
+by (induct_tac "x" 1);
 by (ALLGOALS(Simp_tac));
 val compat_env=result();
 
@@ -329,7 +329,7 @@
 by (simp_tac (ss addsimps [empty_def,compatible_def,asig_of_par,asig_comp_def,actions_def,Int_def]) 1);
 by (Simp_tac 1);
 by (rtac set_ext 1);
-by (Action.action.induct_tac "x" 1);
+by (induct_tac "x" 1);
 by (ALLGOALS Simp_tac);
 val compat_env_fin=result();
 
diff -r 8ceaa19f7717 -r 704dd3a6d47d src/HOLCF/IOA/ABP/Correctness.thy
--- a/src/HOLCF/IOA/ABP/Correctness.thy	Fri Jul 24 13:39:47 1998 +0200
+++ b/src/HOLCF/IOA/ABP/Correctness.thy	Fri Jul 24 13:44:27 1998 +0200
@@ -17,7 +17,6 @@
 system_fin_ioa   :: "('m action, bool * 'm impl_state)ioa"
   
 primrec
-  reduce List.list  
   reduce_Nil  "reduce [] = []"
   reduce_Cons "reduce(x#xs) =   
                  (case xs of   
diff -r 8ceaa19f7717 -r 704dd3a6d47d src/HOLCF/IOA/ABP/Lemmas.ML
--- a/src/HOLCF/IOA/ABP/Lemmas.ML	Fri Jul 24 13:39:47 1998 +0200
+++ b/src/HOLCF/IOA/ABP/Lemmas.ML	Fri Jul 24 13:44:27 1998 +0200
@@ -45,13 +45,13 @@
 val list_ss = simpset_of List.thy;
 
 goal List.thy "hd(l@m) = (if l~=[] then hd(l) else hd(m))";
-by (List.list.induct_tac "l" 1);
+by (induct_tac "l" 1);
 by (simp_tac list_ss 1);
 by (simp_tac list_ss 1);
 val hd_append =result();
 
 goal List.thy "l ~= [] --> (? x xs. l = (x#xs))";
- by (List.list.induct_tac "l" 1);
+ by (induct_tac "l" 1);
  by (simp_tac list_ss 1);
  by (Fast_tac 1);
 qed"cons_not_nil";
diff -r 8ceaa19f7717 -r 704dd3a6d47d src/HOLCF/IOA/NTP/Action.thy
--- a/src/HOLCF/IOA/NTP/Action.thy	Fri Jul 24 13:39:47 1998 +0200
+++ b/src/HOLCF/IOA/NTP/Action.thy	Fri Jul 24 13:44:27 1998 +0200
@@ -6,7 +6,7 @@
 The set of all actions of the system
 *)
 
-Action = Packet +
+Action = Packet + Datatype +
 datatype 'm action = S_msg ('m) | R_msg ('m)
                    | S_pkt ('m packet) | R_pkt ('m packet)
                    | S_ack (bool) | R_ack (bool)
diff -r 8ceaa19f7717 -r 704dd3a6d47d src/HOLCF/IOA/NTP/Correctness.ML
--- a/src/HOLCF/IOA/NTP/Correctness.ML	Fri Jul 24 13:39:47 1998 +0200
+++ b/src/HOLCF/IOA/NTP/Correctness.ML	Fri Jul 24 13:44:27 1998 +0200
@@ -44,7 +44,7 @@
                             restrict_asig_def, Spec.sig_def]
                             @asig_projections)) 1);
 
-  by (Action.action.induct_tac "a" 1);
+  by (induct_tac "a" 1);
   by (ALLGOALS(simp_tac (simpset() addsimps [actions_def]@asig_projections)));
  (* 2 *)
   by (simp_tac (simpset() addsimps impl_ioas) 1);
@@ -76,7 +76,7 @@
 by (REPEAT(rtac allI 1));
 by (rtac imp_conj_lemma 1);   (* from lemmas.ML *)
 
-by (Action.action.induct_tac "a"  1);
+by (induct_tac "a"  1);
 by (asm_simp_tac (ss' addsplits [split_if]) 1);
 by (forward_tac [inv4] 1);
 by (fast_tac (claset() addss (simpset() addsimps [neq_Nil_conv])) 1);
diff -r 8ceaa19f7717 -r 704dd3a6d47d src/HOLCF/IOA/NTP/Impl.ML
--- a/src/HOLCF/IOA/NTP/Impl.ML	Fri Jul 24 13:39:47 1998 +0200
+++ b/src/HOLCF/IOA/NTP/Impl.ML	Fri Jul 24 13:44:27 1998 +0200
@@ -41,7 +41,7 @@
 \            | a:actions(receiver_asig) \
 \            | a:actions(srch_asig)     \
 \            | a:actions(rsch_asig)";
-  by (Action.action.induct_tac "a" 1);
+  by (induct_tac "a" 1);
   by (ALLGOALS (Simp_tac));
 Addsimps [result()];
 
@@ -160,7 +160,7 @@
       1);
 
   by (asm_simp_tac (simpset() addsimps impl_ioas delsplits [split_if]) 1);
-  by (Action.action.induct_tac "a" 1);
+  by (induct_tac "a" 1);
 
   (* 10 cases. First 4 are simple, since state doesn't change *)
 
@@ -221,7 +221,7 @@
                                        @ sender_projections @ impl_ioas))) 1);
 
   by (asm_simp_tac (simpset() addsimps impl_ioas delsplits [split_if]) 1);
-  by (Action.action.induct_tac "a" 1);
+  by (induct_tac "a" 1);
 
 val tac3 = asm_full_simp_tac (ss addsimps [inv3_def] addsplits [split_if]);
 
@@ -287,7 +287,7 @@
                                        @ sender_projections @ impl_ioas))) 1);
 
   by (asm_simp_tac (simpset() addsimps impl_ioas delsplits [split_if]) 1);
-  by (Action.action.induct_tac "a" 1);
+  by (induct_tac "a" 1);
 
 val tac4 =  asm_full_simp_tac (ss addsimps [inv4_def]
                               setloop (split_tac [split_if]));
diff -r 8ceaa19f7717 -r 704dd3a6d47d src/HOLCF/IOA/NTP/Lemmas.ML
--- a/src/HOLCF/IOA/NTP/Lemmas.ML	Fri Jul 24 13:39:47 1998 +0200
+++ b/src/HOLCF/IOA/NTP/Lemmas.ML	Fri Jul 24 13:44:27 1998 +0200
@@ -36,7 +36,7 @@
 (* Arithmetic *)
 
 goal Arith.thy "!!x. 0<x ==> (x-1 = y) = (x = Suc(y))";
-by (asm_simp_tac (simpset() addsimps [diff_Suc] addsplits [split_nat_case]) 1);
+by (asm_simp_tac (simpset() addsimps [diff_Suc] addsplits [nat.split]) 1);
 by (Blast_tac 1);
 qed "pred_suc";
 
diff -r 8ceaa19f7717 -r 704dd3a6d47d src/HOLCF/IOA/meta_theory/Sequence.ML
--- a/src/HOLCF/IOA/meta_theory/Sequence.ML	Fri Jul 24 13:39:47 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/Sequence.ML	Fri Jul 24 13:44:27 1998 +0200
@@ -878,9 +878,9 @@
 \   --> seq_take n`(x @@ (t>>y1)) =  seq_take n`(x @@ (t>>y2)))";
 by (Seq_induct_tac "x" [] 1);
 by (strip_tac 1);
-by (res_inst_tac [("n","n")] natE 1);
+by (exhaust_tac "n" 1);
 by Auto_tac;
-by (res_inst_tac [("n","n")] natE 1);
+by (exhaust_tac "n" 1);
 by Auto_tac;
 qed"take_reduction1";
 
@@ -900,9 +900,9 @@
 \   --> seq_take n`(x @@ (t>>y1)) <<  seq_take n`(x @@ (t>>y2)))";
 by (Seq_induct_tac "x" [] 1);
 by (strip_tac 1);
-by (res_inst_tac [("n","n")] natE 1);
+by (exhaust_tac "n" 1);
 by Auto_tac;
-by (res_inst_tac [("n","n")] natE 1);
+by (exhaust_tac "n" 1);
 by Auto_tac;
 qed"take_reduction_less1";
 
diff -r 8ceaa19f7717 -r 704dd3a6d47d src/HOLCF/IOA/meta_theory/TrivEx.ML
--- a/src/HOLCF/IOA/meta_theory/TrivEx.ML	Fri Jul 24 13:39:47 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/TrivEx.ML	Fri Jul 24 13:44:27 1998 +0200
@@ -23,7 +23,7 @@
 by (simp_tac (simpset() addsimps [trans_of_def,
         C_ioa_def,A_ioa_def,C_trans_def,A_trans_def])1);
 by (simp_tac (simpset() addsimps [h_abs_def]) 1);
-by (action.induct_tac "a" 1);
+by (induct_tac "a" 1);
 by Auto_tac;
 qed"h_abs_is_abstraction";
 
diff -r 8ceaa19f7717 -r 704dd3a6d47d src/HOLCF/IOA/meta_theory/TrivEx2.ML
--- a/src/HOLCF/IOA/meta_theory/TrivEx2.ML	Fri Jul 24 13:39:47 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/TrivEx2.ML	Fri Jul 24 13:44:27 1998 +0200
@@ -23,7 +23,7 @@
 by (simp_tac (simpset() addsimps [trans_of_def,
         C_ioa_def,A_ioa_def,C_trans_def,A_trans_def])1);
 by (simp_tac (simpset() addsimps [h_abs_def]) 1);
-by (action.induct_tac "a" 1);
+by (induct_tac "a" 1);
 by Auto_tac;
 qed"h_abs_is_abstraction";
 
@@ -32,7 +32,7 @@
 Goalw [xt2_def,plift,option_lift]
   "(xt2 (plift afun)) (s,a,t) = (afun a)";
 (* !!!!!!!!!!!!! Occurs check !!!! *)
-by (option.induct_tac "a" 1);
+by (induct_tac "a" 1);
 
 *)
 
diff -r 8ceaa19f7717 -r 704dd3a6d47d src/HOLCF/Lift1.thy
--- a/src/HOLCF/Lift1.thy	Fri Jul 24 13:39:47 1998 +0200
+++ b/src/HOLCF/Lift1.thy	Fri Jul 24 13:44:27 1998 +0200
@@ -6,7 +6,7 @@
 Lifting types of class term to flat pcpo's
 *)
 
-Lift1 = Cprod3 + 
+Lift1 = Cprod3 + Datatype +
 
 default term
 
diff -r 8ceaa19f7717 -r 704dd3a6d47d src/HOLCF/Porder.ML
--- a/src/HOLCF/Porder.ML	Fri Jul 24 13:39:47 1998 +0200
+++ b/src/HOLCF/Porder.ML	Fri Jul 24 13:44:27 1998 +0200
@@ -32,7 +32,7 @@
 ( fn prems =>
         [
         (cut_facts_tac prems 1),
-        (nat_ind_tac "y" 1),
+        (induct_tac "y" 1),
         (rtac impI 1),
         (etac less_zeroE 1),
         (stac less_Suc_eq 1),
@@ -224,7 +224,7 @@
         (cut_facts_tac prems 1),
         (rtac chainI 1),
         (rtac allI 1),
-        (nat_ind_tac "i" 1),
+        (induct_tac "i" 1),
         (Asm_simp_tac 1),
         (Asm_simp_tac 1)
         ]);
@@ -235,7 +235,7 @@
         [
         (cut_facts_tac prems 1),
         (rtac allI 1),
-        (nat_ind_tac "j" 1),
+        (induct_tac "j" 1),
         (Asm_simp_tac 1),
         (Asm_simp_tac 1)
         ]);
diff -r 8ceaa19f7717 -r 704dd3a6d47d src/HOLCF/ex/Hoare.ML
--- a/src/HOLCF/ex/Hoare.ML	Fri Jul 24 13:39:47 1998 +0200
+++ b/src/HOLCF/ex/Hoare.ML	Fri Jul 24 13:44:27 1998 +0200
@@ -183,7 +183,7 @@
  (fn prems =>
         [
         (cut_facts_tac prems 1),
-        (res_inst_tac [("n","k")] natE 1),
+        (exhaust_tac "k" 1),
         (hyp_subst_tac 1),
         (Simp_tac 1),
         (strip_tac 1),
@@ -199,7 +199,7 @@
         (atac 1),
         (rtac trans 1),
         (rtac p_def3 1),
-        (res_inst_tac [("s","TT"),("t","b1`(iterate xa g x)")] ssubst 1),
+        (res_inst_tac [("s","TT"),("t","b1`(iterate nat g x)")] ssubst 1),
         (rtac (hoare_lemma8 RS spec RS mp) 1),
         (atac 1),
         (atac 1),
@@ -220,7 +220,7 @@
  (fn prems =>
         [
         (cut_facts_tac prems 1),
-        (res_inst_tac [("n","k")] natE 1),
+        (exhaust_tac "k" 1),
         (hyp_subst_tac 1),
         (Simp_tac 1),
         (strip_tac 1),
@@ -238,7 +238,7 @@
         (atac 1),
         (rtac trans 1),
         (rtac p_def3 1),
-        (res_inst_tac [("s","TT"),("t","b1`(iterate xa g x)")] ssubst 1),
+        (res_inst_tac [("s","TT"),("t","b1`(iterate nat g x)")] ssubst 1),
         (rtac (hoare_lemma8 RS spec RS mp) 1),
         (atac 1),
         (atac 1),
@@ -381,7 +381,7 @@
  (fn prems =>
         [
         (cut_facts_tac prems 1),
-        (res_inst_tac [("n","k")] natE 1),
+        (exhaust_tac "k" 1),
         (hyp_subst_tac 1),
         (strip_tac 1),
         (Simp_tac 1),
@@ -394,7 +394,7 @@
         (atac 1),
         (rtac trans 1),
         (rtac q_def3 1),
-        (res_inst_tac [("s","TT"),("t","b1`(iterate xa g x)")] ssubst 1),
+        (res_inst_tac [("s","TT"),("t","b1`(iterate nat g x)")] ssubst 1),
         (rtac (hoare_lemma8 RS spec RS mp) 1),
         (atac 1),
         (atac 1),
@@ -410,7 +410,7 @@
  (fn prems =>
         [
         (cut_facts_tac prems 1),
-        (res_inst_tac [("n","k")] natE 1),
+        (exhaust_tac "k" 1),
         (hyp_subst_tac 1),
         (Simp_tac 1),
         (strip_tac 1),
@@ -427,7 +427,7 @@
         (atac 1),
         (rtac trans 1),
         (rtac q_def3 1),
-        (res_inst_tac [("s","TT"),("t","b1`(iterate xa g x)")] ssubst 1),
+        (res_inst_tac [("s","TT"),("t","b1`(iterate nat g x)")] ssubst 1),
         (rtac (hoare_lemma8 RS spec RS mp) 1),
         (atac 1),
         (atac 1),