Adapted to new datatype package.
authorberghofe
Fri Jul 24 13:44:27 1998 +0200 (1998-07-24)
changeset 5192704dd3a6d47d
parent 5191 8ceaa19f7717
child 5193 5f6f7195dacf
Adapted to new datatype package.
src/HOLCF/Discrete0.thy
src/HOLCF/Discrete1.ML
src/HOLCF/Fix.ML
src/HOLCF/Fix.thy
src/HOLCF/IMP/Denotational.ML
src/HOLCF/IMP/Denotational.thy
src/HOLCF/IOA/ABP/Abschannel_finite.thy
src/HOLCF/IOA/ABP/Action.thy
src/HOLCF/IOA/ABP/Correctness.ML
src/HOLCF/IOA/ABP/Correctness.thy
src/HOLCF/IOA/ABP/Lemmas.ML
src/HOLCF/IOA/NTP/Action.thy
src/HOLCF/IOA/NTP/Correctness.ML
src/HOLCF/IOA/NTP/Impl.ML
src/HOLCF/IOA/NTP/Lemmas.ML
src/HOLCF/IOA/meta_theory/Sequence.ML
src/HOLCF/IOA/meta_theory/TrivEx.ML
src/HOLCF/IOA/meta_theory/TrivEx2.ML
src/HOLCF/Lift1.thy
src/HOLCF/Porder.ML
src/HOLCF/ex/Hoare.ML
     1.1 --- a/src/HOLCF/Discrete0.thy	Fri Jul 24 13:39:47 1998 +0200
     1.2 +++ b/src/HOLCF/Discrete0.thy	Fri Jul 24 13:44:27 1998 +0200
     1.3 @@ -6,9 +6,9 @@
     1.4  Discrete CPOs
     1.5  *)
     1.6  
     1.7 -Discrete0 = Cont +
     1.8 +Discrete0 = Cont + Datatype +
     1.9  
    1.10 -datatype 'a discr = Discr 'a
    1.11 +datatype 'a discr = Discr "'a :: term"
    1.12  
    1.13  instance discr :: (term)sq_ord
    1.14  
     2.1 --- a/src/HOLCF/Discrete1.ML	Fri Jul 24 13:39:47 1998 +0200
     2.2 +++ b/src/HOLCF/Discrete1.ML	Fri Jul 24 13:44:27 1998 +0200
     2.3 @@ -13,7 +13,7 @@
     2.4  
     2.5  Goalw [chain]
     2.6   "!!S::nat=>('a::term)discr. chain S ==> S i = S 0";
     2.7 -by (nat_ind_tac "i" 1);
     2.8 +by (induct_tac "i" 1);
     2.9  by (rtac refl 1);
    2.10  by (etac subst 1);
    2.11  by (rtac sym 1);
     3.1 --- a/src/HOLCF/Fix.ML	Fri Jul 24 13:39:47 1998 +0200
     3.2 +++ b/src/HOLCF/Fix.ML	Fri Jul 24 13:44:27 1998 +0200
     3.3 @@ -12,24 +12,10 @@
     3.4  (* derive inductive properties of iterate from primitive recursion          *)
     3.5  (* ------------------------------------------------------------------------ *)
     3.6  
     3.7 -qed_goal "iterate_0" thy "iterate 0 F x = x"
     3.8 - (fn prems =>
     3.9 -        [
    3.10 -        (resolve_tac (nat_recs iterate_def) 1)
    3.11 -        ]);
    3.12 -
    3.13 -qed_goal "iterate_Suc" thy "iterate (Suc n) F x  = F`(iterate n F x)"
    3.14 - (fn prems =>
    3.15 -        [
    3.16 -        (resolve_tac (nat_recs iterate_def) 1)
    3.17 -        ]);
    3.18 -
    3.19 -Addsimps [iterate_0, iterate_Suc];
    3.20 -
    3.21  qed_goal "iterate_Suc2" thy "iterate (Suc n) F x = iterate n F (F`x)"
    3.22   (fn prems =>
    3.23          [
    3.24 -        (nat_ind_tac "n" 1),
    3.25 +        (induct_tac "n" 1),
    3.26          (Simp_tac 1),
    3.27          (stac iterate_Suc 1),
    3.28          (stac iterate_Suc 1),
    3.29 @@ -49,7 +35,7 @@
    3.30          (cut_facts_tac prems 1),
    3.31          (strip_tac 1),
    3.32          (Simp_tac 1),
    3.33 -        (nat_ind_tac "i" 1),
    3.34 +        (induct_tac "i" 1),
    3.35          (Asm_simp_tac 1),
    3.36          (Asm_simp_tac 1),
    3.37          (etac monofun_cfun_arg 1)
    3.38 @@ -103,7 +89,7 @@
    3.39          (rtac chain_iterate 1),
    3.40          (rtac ub_rangeI 1),
    3.41          (strip_tac 1),
    3.42 -        (nat_ind_tac "i" 1),
    3.43 +        (induct_tac "i" 1),
    3.44          (Asm_simp_tac 1),
    3.45          (Asm_simp_tac 1),
    3.46          (res_inst_tac [("t","x")] subst 1),
    3.47 @@ -120,7 +106,7 @@
    3.48   (fn prems =>
    3.49          [
    3.50          (strip_tac 1),
    3.51 -        (nat_ind_tac "i" 1),
    3.52 +        (induct_tac "i" 1),
    3.53          (Asm_simp_tac 1),
    3.54          (Asm_simp_tac 1),
    3.55          (rtac (less_fun RS iffD2) 1),
    3.56 @@ -141,7 +127,7 @@
    3.57   (fn prems =>
    3.58          [
    3.59          (strip_tac 1),
    3.60 -        (nat_ind_tac "i" 1),
    3.61 +        (induct_tac "i" 1),
    3.62          (Asm_simp_tac 1),
    3.63          (rtac (lub_const RS thelubI RS sym) 1),
    3.64          (Asm_simp_tac 1),
    3.65 @@ -185,7 +171,7 @@
    3.66          [
    3.67          (rtac monofunI 1),
    3.68          (strip_tac 1),
    3.69 -        (nat_ind_tac "n" 1),
    3.70 +        (induct_tac "n" 1),
    3.71          (Asm_simp_tac 1),
    3.72          (Asm_simp_tac 1),
    3.73          (etac monofun_cfun_arg 1)
    3.74 @@ -196,7 +182,7 @@
    3.75          [
    3.76          (rtac contlubI 1),
    3.77          (strip_tac 1),
    3.78 -        (nat_ind_tac "n" 1),
    3.79 +        (induct_tac "n" 1),
    3.80          (Simp_tac 1),
    3.81          (Simp_tac 1),
    3.82          (res_inst_tac [("t","iterate n F (lub(range(%u. Y u)))"),
    3.83 @@ -493,7 +479,7 @@
    3.84          (etac admD 1),
    3.85          (rtac chain_iterate 1),
    3.86          (rtac allI 1),
    3.87 -        (nat_ind_tac "i" 1),
    3.88 +        (induct_tac "i" 1),
    3.89          (stac iterate_0 1),
    3.90          (atac 1),
    3.91          (stac iterate_Suc 1),
     4.1 --- a/src/HOLCF/Fix.thy	Fri Jul 24 13:39:47 1998 +0200
     4.2 +++ b/src/HOLCF/Fix.thy	Fri Jul 24 13:44:27 1998 +0200
     4.3 @@ -18,9 +18,12 @@
     4.4  adm		:: "('a::cpo=>bool)=>bool"
     4.5  admw		:: "('a=>bool)=>bool"
     4.6  
     4.7 +primrec
     4.8 +  iterate_0   "iterate 0 F x = x"
     4.9 +  iterate_Suc "iterate (Suc n) F x  = F`(iterate n F x)"
    4.10 +
    4.11  defs
    4.12  
    4.13 -iterate_def   "iterate n F c == nat_rec c (%n x. F`x) n"
    4.14  Ifix_def      "Ifix F == lub(range(%i. iterate i F UU))"
    4.15  fix_def       "fix == (LAM f. Ifix f)"
    4.16  
     5.1 --- a/src/HOLCF/IMP/Denotational.ML	Fri Jul 24 13:39:47 1998 +0200
     5.2 +++ b/src/HOLCF/IMP/Denotational.ML	Fri Jul 24 13:44:27 1998 +0200
     5.3 @@ -18,7 +18,7 @@
     5.4  
     5.5  Goalw [dlift_def]
     5.6   "(dlift f`l = Def y) = (? x. l = Def x & f`(Discr x) = Def y)";
     5.7 -by (simp_tac (simpset() addsplits [split_lift_case]) 1);
     5.8 +by (simp_tac (simpset() addsplits [Lift1.lift.split]) 1);
     5.9  qed "dlift_is_Def";
    5.10  Addsimps [dlift_is_Def];
    5.11  
    5.12 @@ -29,7 +29,7 @@
    5.13  qed_spec_mp "eval_implies_D";
    5.14  
    5.15  Goal "!s t. D c`(Discr s) = (Def t) --> <c,s> -c-> t";
    5.16 -by (com.induct_tac "c" 1);
    5.17 +by (induct_tac "c" 1);
    5.18      by (fast_tac ((HOL_cs addSIs evalc.intrs) addss simpset()) 1);
    5.19     by (fast_tac ((HOL_cs addSIs evalc.intrs) addss simpset()) 1);
    5.20    by (fast_tac ((HOL_cs addSIs evalc.intrs) addss simpset()) 1);
     6.1 --- a/src/HOLCF/IMP/Denotational.thy	Fri Jul 24 13:39:47 1998 +0200
     6.2 +++ b/src/HOLCF/IMP/Denotational.thy	Fri Jul 24 13:44:27 1998 +0200
     6.3 @@ -14,7 +14,7 @@
     6.4  
     6.5  consts D :: "com => state discr -> state lift"
     6.6  
     6.7 -primrec D com
     6.8 +primrec
     6.9    "D(SKIP) = (LAM s. Def(undiscr s))"
    6.10    "D(X := a) = (LAM s. Def((undiscr s)[X := a(undiscr s)]))"
    6.11    "D(c0 ; c1) = (dlift(D c1) oo (D c0))"
     7.1 --- a/src/HOLCF/IOA/ABP/Abschannel_finite.thy	Fri Jul 24 13:39:47 1998 +0200
     7.2 +++ b/src/HOLCF/IOA/ABP/Abschannel_finite.thy	Fri Jul 24 13:44:27 1998 +0200
     7.3 @@ -28,7 +28,6 @@
     7.4  reverse        :: 'a list => 'a list
     7.5  
     7.6  primrec
     7.7 -  reverse List.list  
     7.8    reverse_Nil  "reverse([]) = []"
     7.9    reverse_Cons "reverse(x#xs) =  reverse(xs)@[x]"
    7.10  
     8.1 --- a/src/HOLCF/IOA/ABP/Action.thy	Fri Jul 24 13:39:47 1998 +0200
     8.2 +++ b/src/HOLCF/IOA/ABP/Action.thy	Fri Jul 24 13:44:27 1998 +0200
     8.3 @@ -6,7 +6,7 @@
     8.4  The set of all actions of the system
     8.5  *)
     8.6  
     8.7 -Action = Packet +
     8.8 +Action = Packet + Datatype +
     8.9  datatype 'm action = Next | S_msg ('m) | R_msg ('m)
    8.10                     | S_pkt ('m packet) | R_pkt ('m packet) 
    8.11                     | S_ack (bool) | R_ack (bool)         
     9.1 --- a/src/HOLCF/IOA/ABP/Correctness.ML	Fri Jul 24 13:39:47 1998 +0200
     9.2 +++ b/src/HOLCF/IOA/ABP/Correctness.ML	Fri Jul 24 13:44:27 1998 +0200
     9.3 @@ -46,10 +46,10 @@
     9.4   by (rtac iffI 1);
     9.5   by (subgoal_tac "(l~=[]) --> (reduce(l)~=[])" 1);
     9.6   by (Fast_tac 1); 
     9.7 - by (List.list.induct_tac "l" 1);
     9.8 + by (induct_tac "l" 1);
     9.9   by (Simp_tac 1);
    9.10   by (Simp_tac 1);
    9.11 - by (rtac (split_list_case RS iffD2) 1);
    9.12 + by (rtac (list.split RS iffD2) 1);
    9.13   by (Asm_full_simp_tac 1);
    9.14   by (REPEAT (rtac allI 1)); 
    9.15   by (rtac impI 1); 
    9.16 @@ -60,7 +60,7 @@
    9.17  val l_iff_red_nil = result();
    9.18  
    9.19  Goal "s~=[] --> hd(s)=hd(reduce(s))";
    9.20 -by (List.list.induct_tac "s" 1);
    9.21 +by (induct_tac "s" 1);
    9.22  by (Simp_tac 1);
    9.23  by (case_tac "list =[]" 1);
    9.24  by (Asm_full_simp_tac 1);
    9.25 @@ -68,7 +68,7 @@
    9.26  by (rotate 1 1);
    9.27  by (asm_full_simp_tac list_ss 1);
    9.28  by (Simp_tac 1);
    9.29 -by (rtac (split_list_case RS iffD2) 1);
    9.30 +by (rtac (list.split RS iffD2) 1);
    9.31  by (asm_full_simp_tac list_ss 1);
    9.32  by (REPEAT (rtac allI 1)); 
    9.33   by (rtac impI 1); 
    9.34 @@ -80,7 +80,7 @@
    9.35  
    9.36  (* to be used in the following Lemma *)
    9.37  Goal "l~=[] --> reverse(reduce(l))~=[]";
    9.38 -by (List.list.induct_tac "l" 1);
    9.39 +by (induct_tac "l" 1);
    9.40  by (Simp_tac 1);
    9.41  by (case_tac "list =[]" 1);
    9.42  by (asm_full_simp_tac (simpset() addsimps [reverse_Cons]) 1);
    9.43 @@ -100,7 +100,7 @@
    9.44  Goal "!!l.[| l~=[] |] ==>   \
    9.45  \   hd(reverse(reduce(a#l))) = hd(reverse(reduce(l)))";
    9.46   by (Simp_tac 1);
    9.47 - by (rtac (split_list_case RS iffD2) 1);
    9.48 + by (rtac (list.split RS iffD2) 1);
    9.49   by (asm_full_simp_tac list_ss 1);
    9.50   by (REPEAT (rtac allI 1)); 
    9.51   by (rtac impI 1); 
    9.52 @@ -119,7 +119,7 @@
    9.53  by (stac split_if 1);
    9.54  by (rtac conjI 1);
    9.55  (* --> *)
    9.56 -by (List.list.induct_tac "l" 1);
    9.57 +by (induct_tac "l" 1);
    9.58  by (Simp_tac 1);
    9.59  by (case_tac "list=[]" 1);
    9.60   by (asm_full_simp_tac (simpset() addsimps [reverse_Nil,reverse_Cons]) 1);
    9.61 @@ -132,7 +132,7 @@
    9.62  by (asm_full_simp_tac (impl_ss addsimps [last_ind_on_first,l_iff_red_nil]) 1);
    9.63  (* <-- *)
    9.64  by (simp_tac (simpset() addsimps [and_de_morgan_and_absorbe,l_iff_red_nil]) 1);
    9.65 -by (List.list.induct_tac "l" 1);
    9.66 +by (induct_tac "l" 1);
    9.67  by (Simp_tac 1);
    9.68  by (case_tac "list=[]" 1);
    9.69  by (cut_inst_tac [("l","list")] cons_not_nil 2);
    9.70 @@ -174,7 +174,7 @@
    9.71  (* ---------------- main-part ------------------- *)
    9.72  by (REPEAT (rtac allI 1));
    9.73  by (rtac imp_conj_lemma 1);
    9.74 -by (abs_action.induct_tac "a" 1);
    9.75 +by (induct_tac "a" 1);
    9.76  (* ----------------- 2 cases ---------------------*)
    9.77  by (ALLGOALS (simp_tac (simpset() addsimps [externals_def])));
    9.78  (* fst case --------------------------------------*)
    9.79 @@ -219,7 +219,7 @@
    9.80  (* main-part *)
    9.81  by (REPEAT (rtac allI 1));
    9.82  by (rtac imp_conj_lemma 1);
    9.83 -by (Action.action.induct_tac "a" 1);
    9.84 +by (induct_tac "a" 1);
    9.85  (* 7 cases *)
    9.86  by (ALLGOALS (simp_tac (simpset() addsimps [externals_def] addsplits [split_if])));
    9.87  qed"sender_unchanged";
    9.88 @@ -235,7 +235,7 @@
    9.89  (* main-part *)
    9.90  by (REPEAT (rtac allI 1));
    9.91  by (rtac imp_conj_lemma 1);
    9.92 -by (Action.action.induct_tac "a" 1);
    9.93 +by (induct_tac "a" 1);
    9.94  (* 7 cases *)
    9.95  by (ALLGOALS(simp_tac (simpset() addsimps [externals_def] addsplits [split_if])));
    9.96  qed"receiver_unchanged";
    9.97 @@ -250,7 +250,7 @@
    9.98  (* main-part *)
    9.99  by (REPEAT (rtac allI 1));
   9.100  by (rtac imp_conj_lemma 1);
   9.101 -by (Action.action.induct_tac "a" 1);
   9.102 +by (induct_tac "a" 1);
   9.103  (* 7 cases *)
   9.104  by (ALLGOALS(simp_tac (simpset() addsimps [externals_def] addsplits [split_if])));
   9.105  qed"env_unchanged";
   9.106 @@ -259,7 +259,7 @@
   9.107  Goal "compatible srch_ioa rsch_ioa"; 
   9.108  by (simp_tac (simpset() addsimps [compatible_def,Int_def,empty_def]) 1);
   9.109  by (rtac set_ext 1);
   9.110 -by (Action.action.induct_tac "x" 1);
   9.111 +by (induct_tac "x" 1);
   9.112  by (ALLGOALS(Simp_tac));
   9.113  val compat_single_ch = result();
   9.114  
   9.115 @@ -267,7 +267,7 @@
   9.116  Goal "compatible srch_fin_ioa rsch_fin_ioa"; 
   9.117  by (simp_tac (simpset() addsimps [compatible_def,Int_def,empty_def]) 1);
   9.118  by (rtac set_ext 1);
   9.119 -by (Action.action.induct_tac "x" 1);
   9.120 +by (induct_tac "x" 1);
   9.121  by (ALLGOALS(Simp_tac));
   9.122  val compat_single_fin_ch = result();
   9.123  
   9.124 @@ -284,7 +284,7 @@
   9.125                             Int_def]) 1);
   9.126  by (Simp_tac 1);
   9.127  by (rtac set_ext 1);
   9.128 -by (Action.action.induct_tac "x" 1);
   9.129 +by (induct_tac "x" 1);
   9.130  by (ALLGOALS Simp_tac);
   9.131  val compat_rec = result();
   9.132  
   9.133 @@ -293,7 +293,7 @@
   9.134  by (simp_tac (ss addsimps [empty_def,compatible_def,asig_of_par,asig_comp_def,actions_def,Int_def]) 1);
   9.135  by (Simp_tac 1);
   9.136  by (rtac set_ext 1);
   9.137 -by (Action.action.induct_tac "x" 1);
   9.138 +by (induct_tac "x" 1);
   9.139  by (ALLGOALS Simp_tac);
   9.140  val compat_rec_fin =result();
   9.141  
   9.142 @@ -302,7 +302,7 @@
   9.143  by (simp_tac (ss addsimps [empty_def,compatible_def,asig_of_par,asig_comp_def,actions_def,Int_def]) 1);
   9.144  by (Simp_tac 1);
   9.145  by (rtac set_ext 1);
   9.146 -by (Action.action.induct_tac "x" 1);
   9.147 +by (induct_tac "x" 1);
   9.148  by (ALLGOALS(Simp_tac));
   9.149  val compat_sen=result();
   9.150  
   9.151 @@ -311,7 +311,7 @@
   9.152  by (simp_tac (ss addsimps [empty_def,  compatible_def,asig_of_par,asig_comp_def,actions_def,Int_def]) 1);
   9.153  by (Simp_tac 1);
   9.154  by (rtac set_ext 1);
   9.155 -by (Action.action.induct_tac "x" 1);
   9.156 +by (induct_tac "x" 1);
   9.157  by (ALLGOALS(Simp_tac));
   9.158  val compat_sen_fin =result();
   9.159  
   9.160 @@ -320,7 +320,7 @@
   9.161  by (simp_tac (ss addsimps [empty_def,compatible_def,asig_of_par,asig_comp_def,actions_def,Int_def]) 1);
   9.162  by (Simp_tac 1);
   9.163  by (rtac set_ext 1);
   9.164 -by (Action.action.induct_tac "x" 1);
   9.165 +by (induct_tac "x" 1);
   9.166  by (ALLGOALS(Simp_tac));
   9.167  val compat_env=result();
   9.168  
   9.169 @@ -329,7 +329,7 @@
   9.170  by (simp_tac (ss addsimps [empty_def,compatible_def,asig_of_par,asig_comp_def,actions_def,Int_def]) 1);
   9.171  by (Simp_tac 1);
   9.172  by (rtac set_ext 1);
   9.173 -by (Action.action.induct_tac "x" 1);
   9.174 +by (induct_tac "x" 1);
   9.175  by (ALLGOALS Simp_tac);
   9.176  val compat_env_fin=result();
   9.177  
    10.1 --- a/src/HOLCF/IOA/ABP/Correctness.thy	Fri Jul 24 13:39:47 1998 +0200
    10.2 +++ b/src/HOLCF/IOA/ABP/Correctness.thy	Fri Jul 24 13:44:27 1998 +0200
    10.3 @@ -17,7 +17,6 @@
    10.4  system_fin_ioa   :: "('m action, bool * 'm impl_state)ioa"
    10.5    
    10.6  primrec
    10.7 -  reduce List.list  
    10.8    reduce_Nil  "reduce [] = []"
    10.9    reduce_Cons "reduce(x#xs) =   
   10.10                   (case xs of   
    11.1 --- a/src/HOLCF/IOA/ABP/Lemmas.ML	Fri Jul 24 13:39:47 1998 +0200
    11.2 +++ b/src/HOLCF/IOA/ABP/Lemmas.ML	Fri Jul 24 13:44:27 1998 +0200
    11.3 @@ -45,13 +45,13 @@
    11.4  val list_ss = simpset_of List.thy;
    11.5  
    11.6  goal List.thy "hd(l@m) = (if l~=[] then hd(l) else hd(m))";
    11.7 -by (List.list.induct_tac "l" 1);
    11.8 +by (induct_tac "l" 1);
    11.9  by (simp_tac list_ss 1);
   11.10  by (simp_tac list_ss 1);
   11.11  val hd_append =result();
   11.12  
   11.13  goal List.thy "l ~= [] --> (? x xs. l = (x#xs))";
   11.14 - by (List.list.induct_tac "l" 1);
   11.15 + by (induct_tac "l" 1);
   11.16   by (simp_tac list_ss 1);
   11.17   by (Fast_tac 1);
   11.18  qed"cons_not_nil";
    12.1 --- a/src/HOLCF/IOA/NTP/Action.thy	Fri Jul 24 13:39:47 1998 +0200
    12.2 +++ b/src/HOLCF/IOA/NTP/Action.thy	Fri Jul 24 13:44:27 1998 +0200
    12.3 @@ -6,7 +6,7 @@
    12.4  The set of all actions of the system
    12.5  *)
    12.6  
    12.7 -Action = Packet +
    12.8 +Action = Packet + Datatype +
    12.9  datatype 'm action = S_msg ('m) | R_msg ('m)
   12.10                     | S_pkt ('m packet) | R_pkt ('m packet)
   12.11                     | S_ack (bool) | R_ack (bool)
    13.1 --- a/src/HOLCF/IOA/NTP/Correctness.ML	Fri Jul 24 13:39:47 1998 +0200
    13.2 +++ b/src/HOLCF/IOA/NTP/Correctness.ML	Fri Jul 24 13:44:27 1998 +0200
    13.3 @@ -44,7 +44,7 @@
    13.4                              restrict_asig_def, Spec.sig_def]
    13.5                              @asig_projections)) 1);
    13.6  
    13.7 -  by (Action.action.induct_tac "a" 1);
    13.8 +  by (induct_tac "a" 1);
    13.9    by (ALLGOALS(simp_tac (simpset() addsimps [actions_def]@asig_projections)));
   13.10   (* 2 *)
   13.11    by (simp_tac (simpset() addsimps impl_ioas) 1);
   13.12 @@ -76,7 +76,7 @@
   13.13  by (REPEAT(rtac allI 1));
   13.14  by (rtac imp_conj_lemma 1);   (* from lemmas.ML *)
   13.15  
   13.16 -by (Action.action.induct_tac "a"  1);
   13.17 +by (induct_tac "a"  1);
   13.18  by (asm_simp_tac (ss' addsplits [split_if]) 1);
   13.19  by (forward_tac [inv4] 1);
   13.20  by (fast_tac (claset() addss (simpset() addsimps [neq_Nil_conv])) 1);
    14.1 --- a/src/HOLCF/IOA/NTP/Impl.ML	Fri Jul 24 13:39:47 1998 +0200
    14.2 +++ b/src/HOLCF/IOA/NTP/Impl.ML	Fri Jul 24 13:44:27 1998 +0200
    14.3 @@ -41,7 +41,7 @@
    14.4  \            | a:actions(receiver_asig) \
    14.5  \            | a:actions(srch_asig)     \
    14.6  \            | a:actions(rsch_asig)";
    14.7 -  by (Action.action.induct_tac "a" 1);
    14.8 +  by (induct_tac "a" 1);
    14.9    by (ALLGOALS (Simp_tac));
   14.10  Addsimps [result()];
   14.11  
   14.12 @@ -160,7 +160,7 @@
   14.13        1);
   14.14  
   14.15    by (asm_simp_tac (simpset() addsimps impl_ioas delsplits [split_if]) 1);
   14.16 -  by (Action.action.induct_tac "a" 1);
   14.17 +  by (induct_tac "a" 1);
   14.18  
   14.19    (* 10 cases. First 4 are simple, since state doesn't change *)
   14.20  
   14.21 @@ -221,7 +221,7 @@
   14.22                                         @ sender_projections @ impl_ioas))) 1);
   14.23  
   14.24    by (asm_simp_tac (simpset() addsimps impl_ioas delsplits [split_if]) 1);
   14.25 -  by (Action.action.induct_tac "a" 1);
   14.26 +  by (induct_tac "a" 1);
   14.27  
   14.28  val tac3 = asm_full_simp_tac (ss addsimps [inv3_def] addsplits [split_if]);
   14.29  
   14.30 @@ -287,7 +287,7 @@
   14.31                                         @ sender_projections @ impl_ioas))) 1);
   14.32  
   14.33    by (asm_simp_tac (simpset() addsimps impl_ioas delsplits [split_if]) 1);
   14.34 -  by (Action.action.induct_tac "a" 1);
   14.35 +  by (induct_tac "a" 1);
   14.36  
   14.37  val tac4 =  asm_full_simp_tac (ss addsimps [inv4_def]
   14.38                                setloop (split_tac [split_if]));
    15.1 --- a/src/HOLCF/IOA/NTP/Lemmas.ML	Fri Jul 24 13:39:47 1998 +0200
    15.2 +++ b/src/HOLCF/IOA/NTP/Lemmas.ML	Fri Jul 24 13:44:27 1998 +0200
    15.3 @@ -36,7 +36,7 @@
    15.4  (* Arithmetic *)
    15.5  
    15.6  goal Arith.thy "!!x. 0<x ==> (x-1 = y) = (x = Suc(y))";
    15.7 -by (asm_simp_tac (simpset() addsimps [diff_Suc] addsplits [split_nat_case]) 1);
    15.8 +by (asm_simp_tac (simpset() addsimps [diff_Suc] addsplits [nat.split]) 1);
    15.9  by (Blast_tac 1);
   15.10  qed "pred_suc";
   15.11  
    16.1 --- a/src/HOLCF/IOA/meta_theory/Sequence.ML	Fri Jul 24 13:39:47 1998 +0200
    16.2 +++ b/src/HOLCF/IOA/meta_theory/Sequence.ML	Fri Jul 24 13:44:27 1998 +0200
    16.3 @@ -878,9 +878,9 @@
    16.4  \   --> seq_take n`(x @@ (t>>y1)) =  seq_take n`(x @@ (t>>y2)))";
    16.5  by (Seq_induct_tac "x" [] 1);
    16.6  by (strip_tac 1);
    16.7 -by (res_inst_tac [("n","n")] natE 1);
    16.8 +by (exhaust_tac "n" 1);
    16.9  by Auto_tac;
   16.10 -by (res_inst_tac [("n","n")] natE 1);
   16.11 +by (exhaust_tac "n" 1);
   16.12  by Auto_tac;
   16.13  qed"take_reduction1";
   16.14  
   16.15 @@ -900,9 +900,9 @@
   16.16  \   --> seq_take n`(x @@ (t>>y1)) <<  seq_take n`(x @@ (t>>y2)))";
   16.17  by (Seq_induct_tac "x" [] 1);
   16.18  by (strip_tac 1);
   16.19 -by (res_inst_tac [("n","n")] natE 1);
   16.20 +by (exhaust_tac "n" 1);
   16.21  by Auto_tac;
   16.22 -by (res_inst_tac [("n","n")] natE 1);
   16.23 +by (exhaust_tac "n" 1);
   16.24  by Auto_tac;
   16.25  qed"take_reduction_less1";
   16.26  
    17.1 --- a/src/HOLCF/IOA/meta_theory/TrivEx.ML	Fri Jul 24 13:39:47 1998 +0200
    17.2 +++ b/src/HOLCF/IOA/meta_theory/TrivEx.ML	Fri Jul 24 13:44:27 1998 +0200
    17.3 @@ -23,7 +23,7 @@
    17.4  by (simp_tac (simpset() addsimps [trans_of_def,
    17.5          C_ioa_def,A_ioa_def,C_trans_def,A_trans_def])1);
    17.6  by (simp_tac (simpset() addsimps [h_abs_def]) 1);
    17.7 -by (action.induct_tac "a" 1);
    17.8 +by (induct_tac "a" 1);
    17.9  by Auto_tac;
   17.10  qed"h_abs_is_abstraction";
   17.11  
    18.1 --- a/src/HOLCF/IOA/meta_theory/TrivEx2.ML	Fri Jul 24 13:39:47 1998 +0200
    18.2 +++ b/src/HOLCF/IOA/meta_theory/TrivEx2.ML	Fri Jul 24 13:44:27 1998 +0200
    18.3 @@ -23,7 +23,7 @@
    18.4  by (simp_tac (simpset() addsimps [trans_of_def,
    18.5          C_ioa_def,A_ioa_def,C_trans_def,A_trans_def])1);
    18.6  by (simp_tac (simpset() addsimps [h_abs_def]) 1);
    18.7 -by (action.induct_tac "a" 1);
    18.8 +by (induct_tac "a" 1);
    18.9  by Auto_tac;
   18.10  qed"h_abs_is_abstraction";
   18.11  
   18.12 @@ -32,7 +32,7 @@
   18.13  Goalw [xt2_def,plift,option_lift]
   18.14    "(xt2 (plift afun)) (s,a,t) = (afun a)";
   18.15  (* !!!!!!!!!!!!! Occurs check !!!! *)
   18.16 -by (option.induct_tac "a" 1);
   18.17 +by (induct_tac "a" 1);
   18.18  
   18.19  *)
   18.20  
    19.1 --- a/src/HOLCF/Lift1.thy	Fri Jul 24 13:39:47 1998 +0200
    19.2 +++ b/src/HOLCF/Lift1.thy	Fri Jul 24 13:44:27 1998 +0200
    19.3 @@ -6,7 +6,7 @@
    19.4  Lifting types of class term to flat pcpo's
    19.5  *)
    19.6  
    19.7 -Lift1 = Cprod3 + 
    19.8 +Lift1 = Cprod3 + Datatype +
    19.9  
   19.10  default term
   19.11  
    20.1 --- a/src/HOLCF/Porder.ML	Fri Jul 24 13:39:47 1998 +0200
    20.2 +++ b/src/HOLCF/Porder.ML	Fri Jul 24 13:44:27 1998 +0200
    20.3 @@ -32,7 +32,7 @@
    20.4  ( fn prems =>
    20.5          [
    20.6          (cut_facts_tac prems 1),
    20.7 -        (nat_ind_tac "y" 1),
    20.8 +        (induct_tac "y" 1),
    20.9          (rtac impI 1),
   20.10          (etac less_zeroE 1),
   20.11          (stac less_Suc_eq 1),
   20.12 @@ -224,7 +224,7 @@
   20.13          (cut_facts_tac prems 1),
   20.14          (rtac chainI 1),
   20.15          (rtac allI 1),
   20.16 -        (nat_ind_tac "i" 1),
   20.17 +        (induct_tac "i" 1),
   20.18          (Asm_simp_tac 1),
   20.19          (Asm_simp_tac 1)
   20.20          ]);
   20.21 @@ -235,7 +235,7 @@
   20.22          [
   20.23          (cut_facts_tac prems 1),
   20.24          (rtac allI 1),
   20.25 -        (nat_ind_tac "j" 1),
   20.26 +        (induct_tac "j" 1),
   20.27          (Asm_simp_tac 1),
   20.28          (Asm_simp_tac 1)
   20.29          ]);
    21.1 --- a/src/HOLCF/ex/Hoare.ML	Fri Jul 24 13:39:47 1998 +0200
    21.2 +++ b/src/HOLCF/ex/Hoare.ML	Fri Jul 24 13:44:27 1998 +0200
    21.3 @@ -183,7 +183,7 @@
    21.4   (fn prems =>
    21.5          [
    21.6          (cut_facts_tac prems 1),
    21.7 -        (res_inst_tac [("n","k")] natE 1),
    21.8 +        (exhaust_tac "k" 1),
    21.9          (hyp_subst_tac 1),
   21.10          (Simp_tac 1),
   21.11          (strip_tac 1),
   21.12 @@ -199,7 +199,7 @@
   21.13          (atac 1),
   21.14          (rtac trans 1),
   21.15          (rtac p_def3 1),
   21.16 -        (res_inst_tac [("s","TT"),("t","b1`(iterate xa g x)")] ssubst 1),
   21.17 +        (res_inst_tac [("s","TT"),("t","b1`(iterate nat g x)")] ssubst 1),
   21.18          (rtac (hoare_lemma8 RS spec RS mp) 1),
   21.19          (atac 1),
   21.20          (atac 1),
   21.21 @@ -220,7 +220,7 @@
   21.22   (fn prems =>
   21.23          [
   21.24          (cut_facts_tac prems 1),
   21.25 -        (res_inst_tac [("n","k")] natE 1),
   21.26 +        (exhaust_tac "k" 1),
   21.27          (hyp_subst_tac 1),
   21.28          (Simp_tac 1),
   21.29          (strip_tac 1),
   21.30 @@ -238,7 +238,7 @@
   21.31          (atac 1),
   21.32          (rtac trans 1),
   21.33          (rtac p_def3 1),
   21.34 -        (res_inst_tac [("s","TT"),("t","b1`(iterate xa g x)")] ssubst 1),
   21.35 +        (res_inst_tac [("s","TT"),("t","b1`(iterate nat g x)")] ssubst 1),
   21.36          (rtac (hoare_lemma8 RS spec RS mp) 1),
   21.37          (atac 1),
   21.38          (atac 1),
   21.39 @@ -381,7 +381,7 @@
   21.40   (fn prems =>
   21.41          [
   21.42          (cut_facts_tac prems 1),
   21.43 -        (res_inst_tac [("n","k")] natE 1),
   21.44 +        (exhaust_tac "k" 1),
   21.45          (hyp_subst_tac 1),
   21.46          (strip_tac 1),
   21.47          (Simp_tac 1),
   21.48 @@ -394,7 +394,7 @@
   21.49          (atac 1),
   21.50          (rtac trans 1),
   21.51          (rtac q_def3 1),
   21.52 -        (res_inst_tac [("s","TT"),("t","b1`(iterate xa g x)")] ssubst 1),
   21.53 +        (res_inst_tac [("s","TT"),("t","b1`(iterate nat g x)")] ssubst 1),
   21.54          (rtac (hoare_lemma8 RS spec RS mp) 1),
   21.55          (atac 1),
   21.56          (atac 1),
   21.57 @@ -410,7 +410,7 @@
   21.58   (fn prems =>
   21.59          [
   21.60          (cut_facts_tac prems 1),
   21.61 -        (res_inst_tac [("n","k")] natE 1),
   21.62 +        (exhaust_tac "k" 1),
   21.63          (hyp_subst_tac 1),
   21.64          (Simp_tac 1),
   21.65          (strip_tac 1),
   21.66 @@ -427,7 +427,7 @@
   21.67          (atac 1),
   21.68          (rtac trans 1),
   21.69          (rtac q_def3 1),
   21.70 -        (res_inst_tac [("s","TT"),("t","b1`(iterate xa g x)")] ssubst 1),
   21.71 +        (res_inst_tac [("s","TT"),("t","b1`(iterate nat g x)")] ssubst 1),
   21.72          (rtac (hoare_lemma8 RS spec RS mp) 1),
   21.73          (atac 1),
   21.74          (atac 1),