Adapted to new datatype package.
authorberghofe
Fri Jul 24 13:19:38 1998 +0200 (1998-07-24)
changeset 51849b8547a9496a
parent 5183 89f162de39cf
child 5185 d1067e2c3f9f
Adapted to new datatype package.
src/HOL/IOA/IOA.ML
src/HOL/IOA/Solve.ML
src/HOL/Induct/Com.thy
src/HOL/Induct/Comb.thy
src/HOL/Induct/LList.ML
src/HOL/Induct/Mutil.ML
src/HOL/Induct/Perm.ML
src/HOL/Induct/PropLog.ML
src/HOL/Induct/PropLog.thy
src/HOL/Integ/Bin.ML
src/HOL/Integ/Bin.thy
src/HOL/Integ/Integ.ML
src/HOL/Lambda/Eta.ML
src/HOL/Lambda/Eta.thy
src/HOL/Lambda/Lambda.ML
src/HOL/Lambda/Lambda.thy
src/HOL/Lambda/ParRed.ML
src/HOL/Lex/AutoChopper.thy
src/HOL/Lex/AutoMaxChop.thy
src/HOL/Lex/MaxChop.ML
src/HOL/Lex/MaxPrefix.thy
src/HOL/Lex/NA.thy
src/HOL/Lex/NAe.thy
src/HOL/Lex/Prefix.ML
src/HOL/Lex/RegExp.thy
src/HOL/Lex/RegExp2NAe.ML
src/HOL/Lex/RegExp2NAe.thy
src/HOL/Lex/RegSet_of_nat_DA.ML
src/HOL/Lex/RegSet_of_nat_DA.thy
src/HOL/MiniML/Generalize.ML
src/HOL/MiniML/Generalize.thy
src/HOL/MiniML/Instance.ML
src/HOL/MiniML/Instance.thy
src/HOL/MiniML/Maybe.ML
src/HOL/MiniML/MiniML.ML
src/HOL/MiniML/Type.ML
src/HOL/MiniML/Type.thy
src/HOL/MiniML/W.ML
src/HOL/MiniML/W.thy
src/HOL/Quot/NPAIR.thy
src/HOL/Real/PNat.ML
src/HOL/Real/Real.ML
src/HOL/Subst/Subst.thy
src/HOL/Subst/UTerm.thy
src/HOL/Subst/Unify.ML
src/HOL/TLA/Inc/Pcount.thy
src/HOL/TLA/Memory/MIParameters.thy
src/HOL/TLA/Memory/Memory.ML
src/HOL/TLA/Memory/MemoryParameters.thy
src/HOL/W0/I.ML
src/HOL/W0/I.thy
src/HOL/W0/Type.ML
src/HOL/W0/Type.thy
src/HOL/W0/W.ML
src/HOL/W0/W.thy
src/HOL/ex/BT.ML
src/HOL/ex/BT.thy
src/HOL/ex/InSort.ML
src/HOL/ex/InSort.thy
src/HOL/ex/NatSum.thy
src/HOL/ex/Primes.thy
src/HOL/ex/Primrec.thy
src/HOL/ex/Qsort.ML
src/HOL/ex/Sorting.ML
src/HOL/ex/Sorting.thy
     1.1 --- a/src/HOL/IOA/IOA.ML	Fri Jul 24 13:03:20 1998 +0200
     1.2 +++ b/src/HOL/IOA/IOA.ML	Fri Jul 24 13:19:38 1998 +0200
     1.3 @@ -83,10 +83,10 @@
     1.4    by (rename_tac "ex1 ex2 n" 1);
     1.5    by (res_inst_tac [("Q","reachable A (ex2 n)")] conjunct1 1);
     1.6    by (Asm_full_simp_tac 1);
     1.7 -  by (nat_ind_tac "n" 1);
     1.8 +  by (induct_tac "n" 1);
     1.9     by (fast_tac (claset() addIs [p1,reachable_0]) 1);
    1.10 -  by (eres_inst_tac[("x","n")] allE 1);
    1.11 -  by (exhaust_tac "ex1 n" 1 THEN ALLGOALS Asm_full_simp_tac);
    1.12 +  by (eres_inst_tac[("x","na")] allE 1);
    1.13 +  by (exhaust_tac "ex1 na" 1 THEN ALLGOALS Asm_full_simp_tac);
    1.14    by Safe_tac;
    1.15     by (etac (p2 RS mp) 1);
    1.16      by (ALLGOALS(fast_tac(claset() addDs [reachable_n])));
     2.1 --- a/src/HOL/IOA/Solve.ML	Fri Jul 24 13:03:20 1998 +0200
     2.2 +++ b/src/HOL/IOA/Solve.ML	Fri Jul 24 13:19:38 1998 +0200
     2.3 @@ -79,7 +79,7 @@
     2.4  by (asm_full_simp_tac
     2.5        (simpset() addsimps [executions_def,is_execution_fragment_def,
     2.6                            par_def,starts_of_def,trans_of_def,filter_oseq_def]
     2.7 -                addsplits [split_option_case]) 1);
     2.8 +                addsplits [option.split]) 1);
     2.9  qed"comp1_reachable";
    2.10  
    2.11  
    2.12 @@ -99,7 +99,7 @@
    2.13  by (asm_full_simp_tac
    2.14        (simpset() addsimps [executions_def,is_execution_fragment_def,
    2.15                            par_def,starts_of_def,trans_of_def,filter_oseq_def]
    2.16 -                addsplits [split_option_case]) 1);
    2.17 +                addsplits [option.split]) 1);
    2.18  qed"comp2_reachable";
    2.19  
    2.20  Delsplits [split_if];
    2.21 @@ -161,7 +161,7 @@
    2.22  by (asm_full_simp_tac
    2.23        (simpset() addsimps [executions_def,is_execution_fragment_def,
    2.24                            par_def,starts_of_def,trans_of_def,rename_def]
    2.25 -                addsplits [split_option_case]) 1);
    2.26 +                addsplits [option.split]) 1);
    2.27  by (best_tac (claset() addSDs [spec] addDs [sym] addss (simpset())) 1);
    2.28  qed"reachable_rename_ioa";
    2.29  
     3.1 --- a/src/HOL/Induct/Com.thy	Fri Jul 24 13:03:20 1998 +0200
     3.2 +++ b/src/HOL/Induct/Com.thy	Fri Jul 24 13:19:38 1998 +0200
     3.3 @@ -6,7 +6,7 @@
     3.4  Example of Mutual Induction via Iteratived Inductive Definitions: Commands
     3.5  *)
     3.6  
     3.7 -Com = Arith + Inductive +
     3.8 +Com = Datatype +
     3.9  
    3.10  types loc
    3.11        state = "loc => nat"
     4.1 --- a/src/HOL/Induct/Comb.thy	Fri Jul 24 13:03:20 1998 +0200
     4.2 +++ b/src/HOL/Induct/Comb.thy	Fri Jul 24 13:19:38 1998 +0200
     4.3 @@ -13,7 +13,7 @@
     4.4  *)
     4.5  
     4.6  
     4.7 -Comb = Arith + Inductive +
     4.8 +Comb = Datatype +
     4.9  
    4.10  (** Datatype definition of combinators S and K, with infixed application **)
    4.11  datatype comb = K
     5.1 --- a/src/HOL/Induct/LList.ML	Fri Jul 24 13:03:20 1998 +0200
     5.2 +++ b/src/HOL/Induct/LList.ML	Fri Jul 24 13:19:38 1998 +0200
     5.3 @@ -155,10 +155,10 @@
     5.4  by (safe_tac ((claset_of Fun.thy) delrules [equalityI]));
     5.5  by (etac LListD.elim 1);
     5.6  by (safe_tac (claset_of Prod.thy delrules [equalityI] addSEs [diagE]));
     5.7 -by (res_inst_tac [("n", "n")] natE 1);
     5.8 +by (exhaust_tac "n" 1);
     5.9  by (Asm_simp_tac 1);
    5.10  by (rename_tac "n'" 1);
    5.11 -by (res_inst_tac [("n", "n'")] natE 1);
    5.12 +by (exhaust_tac "n'" 1);
    5.13  by (asm_simp_tac (simpset() addsimps [CONS_def]) 1);
    5.14  by (asm_simp_tac (simpset() addsimps [CONS_def, less_Suc_eq]) 1);
    5.15  qed "LListD_implies_ntrunc_equality";
    5.16 @@ -317,9 +317,9 @@
    5.17  by (stac prem2 1);
    5.18  by (Simp_tac 1);
    5.19  by (strip_tac 1);
    5.20 -by (res_inst_tac [("n", "n")] natE 1);
    5.21 +by (exhaust_tac "n" 1);
    5.22  by (rename_tac "m" 2);
    5.23 -by (res_inst_tac [("n", "m")] natE 2);
    5.24 +by (exhaust_tac "m" 2);
    5.25  by (ALLGOALS (asm_simp_tac (simpset() addsimps [less_Suc_eq])));
    5.26  result();
    5.27  
    5.28 @@ -782,12 +782,12 @@
    5.29  Goal
    5.30      "nat_rec (LCons b l) (%m. lmap(f)) n =      \
    5.31  \    LCons (nat_rec b (%m. f) n) (nat_rec l (%m. lmap(f)) n)";
    5.32 -by (nat_ind_tac "n" 1);
    5.33 +by (induct_tac "n" 1);
    5.34  by (ALLGOALS Asm_simp_tac);
    5.35  qed "fun_power_lmap";
    5.36  
    5.37  goal Nat.thy "nat_rec (g x) (%m. g) n = nat_rec x (%m. g) (Suc n)";
    5.38 -by (nat_ind_tac "n" 1);
    5.39 +by (induct_tac "n" 1);
    5.40  by (ALLGOALS Asm_simp_tac);
    5.41  qed "fun_power_Suc";
    5.42  
     6.1 --- a/src/HOL/Induct/Mutil.ML	Fri Jul 24 13:03:20 1998 +0200
     6.2 +++ b/src/HOL/Induct/Mutil.ML	Fri Jul 24 13:19:38 1998 +0200
     6.3 @@ -44,7 +44,7 @@
     6.4  qed "Sigma_Suc2";
     6.5  
     6.6  Goal "{i} Times below(n+n) : tiling domino";
     6.7 -by (nat_ind_tac "n" 1);
     6.8 +by (induct_tac "n" 1);
     6.9  by (ALLGOALS (asm_simp_tac (simpset() addsimps [Un_assoc RS sym, Sigma_Suc2])));
    6.10  by (resolve_tac tiling.intrs 1);
    6.11  by (assume_tac 2);
    6.12 @@ -57,7 +57,7 @@
    6.13  qed "dominoes_tile_row";
    6.14  
    6.15  Goal "(below m) Times below(n+n) : tiling domino";
    6.16 -by (nat_ind_tac "m" 1);
    6.17 +by (induct_tac "m" 1);
    6.18  by (ALLGOALS (asm_simp_tac (simpset() addsimps [Sigma_Suc1])));
    6.19  by (blast_tac (claset() addSIs [tiling_UnI, dominoes_tile_row]
    6.20                         addSEs [below_less_iff RS iffD1 RS less_irrefl]) 1);
     7.1 --- a/src/HOL/Induct/Perm.ML	Fri Jul 24 13:03:20 1998 +0200
     7.2 +++ b/src/HOL/Induct/Perm.ML	Fri Jul 24 13:19:38 1998 +0200
     7.3 @@ -14,7 +14,7 @@
     7.4  open Perm;
     7.5  
     7.6  Goal "l <~~> l";
     7.7 -by (list.induct_tac "l" 1);
     7.8 +by (induct_tac "l" 1);
     7.9  by (REPEAT (ares_tac perm.intrs 1));
    7.10  qed "perm_refl";
    7.11  
    7.12 @@ -50,7 +50,7 @@
    7.13  
    7.14  (*We can insert the head anywhere in the list*)
    7.15  Goal "a # xs @ ys <~~> xs @ a # ys";
    7.16 -by (list.induct_tac "xs" 1);
    7.17 +by (induct_tac "xs" 1);
    7.18  by (simp_tac (simpset() addsimps [perm_refl]) 1);
    7.19  by (Simp_tac 1);
    7.20  by (etac ([perm.swap, perm.Cons] MRS perm.trans) 1);
    7.21 @@ -63,7 +63,7 @@
    7.22  *)
    7.23  
    7.24  Goal "xs@ys <~~> ys@xs";
    7.25 -by (list.induct_tac "xs" 1);
    7.26 +by (induct_tac "xs" 1);
    7.27  by (simp_tac (simpset() addsimps [perm_refl]) 1);
    7.28  by (Simp_tac 1);
    7.29  by (etac ([perm.Cons, perm_append_Cons] MRS perm.trans) 1);
    7.30 @@ -77,7 +77,7 @@
    7.31  qed "perm_append_single";
    7.32  
    7.33  Goal "rev xs <~~> xs";
    7.34 -by (list.induct_tac "xs" 1);
    7.35 +by (induct_tac "xs" 1);
    7.36  by (simp_tac (simpset() addsimps [perm_refl]) 1);
    7.37  by (Simp_tac 1);
    7.38  by (rtac (perm_append_single RS perm_sym RS perm.trans) 1);
    7.39 @@ -85,7 +85,7 @@
    7.40  qed "perm_rev";
    7.41  
    7.42  Goal "xs <~~> ys ==> l@xs <~~> l@ys";
    7.43 -by (list.induct_tac "l" 1);
    7.44 +by (induct_tac "l" 1);
    7.45  by (Simp_tac 1);
    7.46  by (asm_simp_tac (simpset() addsimps [perm.Cons]) 1);
    7.47  qed "perm_append1";
     8.1 --- a/src/HOL/Induct/PropLog.ML	Fri Jul 24 13:03:20 1998 +0200
     8.2 +++ b/src/HOL/Induct/PropLog.ML	Fri Jul 24 13:19:38 1998 +0200
     8.3 @@ -102,7 +102,7 @@
     8.4  (*This formulation is required for strong induction hypotheses*)
     8.5  Goal "hyps p tt |- (if tt[p] then p else p->false)";
     8.6  by (rtac (split_if RS iffD2) 1);
     8.7 -by (PropLog.pl.induct_tac "p" 1);
     8.8 +by (induct_tac "p" 1);
     8.9  by (ALLGOALS (simp_tac (simpset() addsimps [thms_I, thms.H])));
    8.10  by (fast_tac (claset() addIs [weaken_left_Un1, weaken_left_Un2, 
    8.11  			      weaken_right, imp_false]
    8.12 @@ -140,7 +140,7 @@
    8.13  (*For the case hyps(p,t)-insert(#v,Y) |- p;
    8.14    we also have hyps(p,t)-{#v} <= hyps(p, t-{v}) *)
    8.15  Goal "hyps p (t-{v}) <= insert (#v->false) ((hyps p t)-{#v})";
    8.16 -by (PropLog.pl.induct_tac "p" 1);
    8.17 +by (induct_tac "p" 1);
    8.18  by (ALLGOALS Simp_tac);
    8.19  by (Fast_tac 1);
    8.20  qed "hyps_Diff";
    8.21 @@ -148,7 +148,7 @@
    8.22  (*For the case hyps(p,t)-insert(#v -> false,Y) |- p;
    8.23    we also have hyps(p,t)-{#v->false} <= hyps(p, insert(v,t)) *)
    8.24  Goal "hyps p (insert v t) <= insert (#v) (hyps p t-{#v->false})";
    8.25 -by (PropLog.pl.induct_tac "p" 1);
    8.26 +by (induct_tac "p" 1);
    8.27  by (ALLGOALS Simp_tac);
    8.28  by (Fast_tac 1);
    8.29  qed "hyps_insert";
    8.30 @@ -169,7 +169,7 @@
    8.31  qed "hyps_finite";
    8.32  
    8.33  Goal "hyps p t <= (UN v. {#v, #v->false})";
    8.34 -by (PropLog.pl.induct_tac "p" 1);
    8.35 +by (induct_tac "p" 1);
    8.36  by (ALLGOALS Simp_tac);
    8.37  by (Blast_tac 1);
    8.38  qed "hyps_subset";
     9.1 --- a/src/HOL/Induct/PropLog.thy	Fri Jul 24 13:03:20 1998 +0200
     9.2 +++ b/src/HOL/Induct/PropLog.thy	Fri Jul 24 13:19:38 1998 +0200
     9.3 @@ -6,7 +6,8 @@
     9.4  Inductive definition of propositional logic.
     9.5  *)
     9.6  
     9.7 -PropLog = Finite +
     9.8 +PropLog = Finite + Datatype +
     9.9 +
    9.10  datatype
    9.11      'a pl = false | var 'a ("#_" [1000]) | "->" ('a pl) ('a pl) (infixr 90)
    9.12  consts
    9.13 @@ -32,12 +33,12 @@
    9.14    sat_def  "H |= p  ==  (!tt. (!q:H. tt[q]) --> tt[p])"
    9.15    eval_def "tt[p] == eval2 p tt"
    9.16  
    9.17 -primrec eval2 pl
    9.18 +primrec
    9.19    "eval2(false) = (%x. False)"
    9.20    "eval2(#v) = (%tt. v:tt)"
    9.21    "eval2(p->q) = (%tt. eval2 p tt-->eval2 q tt)"
    9.22  
    9.23 -primrec hyps pl
    9.24 +primrec
    9.25    "hyps(false) = (%tt.{})"
    9.26    "hyps(#v) = (%tt.{if v:tt then #v else #v->false})"
    9.27    "hyps(p->q) = (%tt. hyps p tt Un hyps q tt)"
    10.1 --- a/src/HOL/Integ/Bin.ML	Fri Jul 24 13:03:20 1998 +0200
    10.2 +++ b/src/HOL/Integ/Bin.ML	Fri Jul 24 13:19:38 1998 +0200
    10.3 @@ -106,7 +106,7 @@
    10.4  
    10.5  qed_goal "integ_of_bin_norm_Bcons" Bin.thy
    10.6      "integ_of_bin(norm_Bcons w b) = integ_of_bin(Bcons w b)"
    10.7 - (fn _ =>[(bin.induct_tac "w" 1),
    10.8 + (fn _ =>[(induct_tac "w" 1),
    10.9            (ALLGOALS Simp_tac) ]);
   10.10  
   10.11  qed_goal "integ_of_bin_succ" Bin.thy
   10.12 @@ -140,11 +140,11 @@
   10.13  
   10.14  Goal
   10.15      "! w. integ_of_bin(bin_add v w) = integ_of_bin v + integ_of_bin w";
   10.16 -by (bin.induct_tac "v" 1);
   10.17 +by (induct_tac "v" 1);
   10.18  by (simp_tac (simpset() addsimps bin_add_simps) 1);
   10.19  by (simp_tac (simpset() addsimps bin_add_simps) 1);
   10.20  by (rtac allI 1);
   10.21 -by (bin.induct_tac "w" 1);
   10.22 +by (induct_tac "w" 1);
   10.23  by (asm_simp_tac (simpset() addsimps (bin_add_simps)) 1);
   10.24  by (asm_simp_tac (simpset() addsimps (bin_add_simps @ zadd_ac)) 1);
   10.25  by (cut_inst_tac [("P","bool")] True_or_False 1);
   10.26 @@ -162,7 +162,7 @@
   10.27                        integ_of_bin_norm_Bcons];
   10.28  
   10.29  Goal "integ_of_bin(bin_mult v w) = integ_of_bin v * integ_of_bin w";
   10.30 -by (bin.induct_tac "v" 1);
   10.31 +by (induct_tac "v" 1);
   10.32  by (simp_tac (simpset() addsimps bin_mult_simps) 1);
   10.33  by (simp_tac (simpset() addsimps bin_mult_simps) 1);
   10.34  by (cut_inst_tac [("P","bool")] True_or_False 1);
    11.1 --- a/src/HOL/Integ/Bin.thy	Fri Jul 24 13:03:20 1998 +0200
    11.2 +++ b/src/HOL/Integ/Bin.thy	Fri Jul 24 13:19:38 1998 +0200
    11.3 @@ -22,7 +22,7 @@
    11.4  quoting the previously computed values.  (Or code an oracle...)
    11.5  *)
    11.6  
    11.7 -Bin = Integ + 
    11.8 +Bin = Integ + Datatype +
    11.9  
   11.10  syntax
   11.11    "_Int"           :: xnum => int        ("_")
   11.12 @@ -43,42 +43,42 @@
   11.13  
   11.14  (*norm_Bcons adds a bit, suppressing leading 0s and 1s*)
   11.15  
   11.16 -primrec norm_Bcons bin
   11.17 +primrec
   11.18    norm_Plus  "norm_Bcons PlusSign  b = (if b then (Bcons PlusSign b) else PlusSign)"
   11.19    norm_Minus "norm_Bcons MinusSign b = (if b then MinusSign else (Bcons MinusSign b))"
   11.20    norm_Bcons "norm_Bcons (Bcons w' x') b = Bcons (Bcons w' x') b"
   11.21   
   11.22 -primrec integ_of_bin bin
   11.23 +primrec
   11.24    iob_Plus  "integ_of_bin PlusSign = $#0"
   11.25    iob_Minus "integ_of_bin MinusSign = $~($#1)"
   11.26    iob_Bcons "integ_of_bin(Bcons w x) = (if x then $#1 else $#0) + (integ_of_bin w) + (integ_of_bin w)" 
   11.27  
   11.28 -primrec bin_succ bin
   11.29 +primrec
   11.30    succ_Plus  "bin_succ PlusSign = Bcons PlusSign True" 
   11.31    succ_Minus "bin_succ MinusSign = PlusSign"
   11.32    succ_Bcons "bin_succ(Bcons w x) = (if x then (Bcons (bin_succ w) False) else (norm_Bcons w True))"
   11.33  
   11.34 -primrec bin_pred bin
   11.35 +primrec
   11.36    pred_Plus  "bin_pred(PlusSign) = MinusSign"
   11.37    pred_Minus "bin_pred(MinusSign) = Bcons MinusSign False"
   11.38    pred_Bcons "bin_pred(Bcons w x) = (if x then (norm_Bcons w False) else (Bcons (bin_pred w) True))"
   11.39   
   11.40 -primrec bin_minus bin
   11.41 +primrec
   11.42    min_Plus  "bin_minus PlusSign = PlusSign"
   11.43    min_Minus "bin_minus MinusSign = Bcons PlusSign True"
   11.44    min_Bcons "bin_minus(Bcons w x) = (if x then (bin_pred (Bcons (bin_minus w) False)) else (Bcons (bin_minus w) False))"
   11.45  
   11.46 -primrec bin_add bin
   11.47 +primrec
   11.48    add_Plus  "bin_add PlusSign w = w"
   11.49    add_Minus "bin_add MinusSign w = bin_pred w"
   11.50    add_Bcons "bin_add (Bcons v x) w = h_bin v x w"
   11.51  
   11.52 -primrec bin_mult bin
   11.53 +primrec
   11.54    mult_Plus "bin_mult PlusSign w = PlusSign"
   11.55    mult_Minus "bin_mult MinusSign w = bin_minus w"
   11.56    mult_Bcons "bin_mult (Bcons v x) w = (if x then (bin_add (norm_Bcons (bin_mult v w) False) w) else (norm_Bcons (bin_mult v w) False))"
   11.57  
   11.58 -primrec h_bin bin
   11.59 +primrec
   11.60    h_Plus  "h_bin v x PlusSign =  Bcons v x"
   11.61    h_Minus "h_bin v x MinusSign = bin_pred (Bcons v x)"
   11.62    h_BCons "h_bin v x (Bcons w y) = norm_Bcons (bin_add v (if (x & y) then bin_succ w else w)) (x~=y)" 
    12.1 --- a/src/HOL/Integ/Integ.ML	Fri Jul 24 13:03:20 1998 +0200
    12.2 +++ b/src/HOL/Integ/Integ.ML	Fri Jul 24 13:19:38 1998 +0200
    12.3 @@ -173,12 +173,12 @@
    12.4  (**** zmagnitude: magnitide of an integer, as a natural number ****)
    12.5  
    12.6  goal Arith.thy "!!n::nat. n - Suc(n+m)=0";
    12.7 -by (nat_ind_tac "n" 1);
    12.8 +by (induct_tac "n" 1);
    12.9  by (ALLGOALS Asm_simp_tac);
   12.10  qed "diff_Suc_add_0";
   12.11  
   12.12  goal Arith.thy "Suc((n::nat)+m)-n=Suc(m)";
   12.13 -by (nat_ind_tac "n" 1);
   12.14 +by (induct_tac "n" 1);
   12.15  by (ALLGOALS Asm_simp_tac);
   12.16  qed "diff_Suc_add_inverse";
   12.17  
   12.18 @@ -785,7 +785,7 @@
   12.19  
   12.20  Goal "$~ $#  n <= $#0";
   12.21    by (rtac zless_or_eq_imp_zle 1); 
   12.22 -  by (nat_ind_tac "n" 1); 
   12.23 +  by (induct_tac "n" 1); 
   12.24    by (ALLGOALS Asm_simp_tac); 
   12.25  qed "negative_zle_0"; 
   12.26  Addsimps[negative_zle_0]; 
    13.1 --- a/src/HOL/Lambda/Eta.ML	Fri Jul 24 13:03:20 1998 +0200
    13.2 +++ b/src/HOL/Lambda/Eta.ML	Fri Jul 24 13:19:38 1998 +0200
    13.3 @@ -25,7 +25,7 @@
    13.4  section "eta, subst and free";
    13.5  
    13.6  Goal "!i t u. ~free s i --> s[t/i] = s[u/i]";
    13.7 -by (dB.induct_tac "s" 1);
    13.8 +by (induct_tac "s" 1);
    13.9  by (ALLGOALS(simp_tac (addsplit (simpset()))));
   13.10  by (Blast_tac 1);
   13.11  by (Blast_tac 1);
   13.12 @@ -33,10 +33,10 @@
   13.13  Addsimps [subst_not_free RS eqTrueI];
   13.14  
   13.15  Goal "!i k. free (lift t k) i = (i < k & free t i | k < i & free t (i-1))";
   13.16 -by (dB.induct_tac "t" 1);
   13.17 +by (induct_tac "t" 1);
   13.18  by (ALLGOALS(asm_full_simp_tac (addsplit (simpset()) addcongs [conj_cong])));
   13.19  by (Blast_tac 2);
   13.20 -by (simp_tac (simpset() addsimps [diff_Suc] addsplits [split_nat_case]) 1);
   13.21 +by (simp_tac (simpset() addsimps [diff_Suc] addsplits [nat.split]) 1);
   13.22  by (safe_tac HOL_cs);
   13.23  by (ALLGOALS trans_tac);
   13.24  qed "free_lift";
   13.25 @@ -44,12 +44,12 @@
   13.26  
   13.27  Goal "!i k t. free (s[t/k]) i = \
   13.28  \              (free s k & free t i | free s (if i<k then i else Suc i))";
   13.29 -by (dB.induct_tac "s" 1);
   13.30 +by (induct_tac "s" 1);
   13.31  by (Asm_simp_tac 2);
   13.32  by (Blast_tac 2);
   13.33  by (asm_full_simp_tac (addsplit (simpset())) 2);
   13.34  by (simp_tac (simpset() addsimps [diff_Suc,subst_Var]
   13.35 -                      addsplits [split_nat_case]) 1);
   13.36 +                      addsplits [nat.split]) 1);
   13.37  by (safe_tac (HOL_cs addSEs [nat_neqE]));
   13.38  by (ALLGOALS trans_tac);
   13.39  qed "free_subst";
   13.40 @@ -123,7 +123,7 @@
   13.41  AddIs [beta_subst];
   13.42  
   13.43  Goal "!i. t[Var i/i] = t[Var(i)/Suc i]";
   13.44 -by (dB.induct_tac "t" 1);
   13.45 +by (induct_tac "t" 1);
   13.46  by (ALLGOALS (asm_simp_tac (addsplit (simpset()))));
   13.47  by (safe_tac (HOL_cs addSEs [nat_neqE]));
   13.48  by (ALLGOALS trans_tac);
   13.49 @@ -137,7 +137,7 @@
   13.50  Addsimps [eta_lift];
   13.51  
   13.52  Goal "!s t i. s -e> t --> u[s/i] -e>> u[t/i]";
   13.53 -by (dB.induct_tac "u" 1);
   13.54 +by (induct_tac "u" 1);
   13.55  by (ALLGOALS(asm_simp_tac (addsplit (simpset()))));
   13.56  by (blast_tac (claset() addIs [r_into_rtrancl]) 1);
   13.57  by (blast_tac (claset() addSIs [rtrancl_eta_App]) 1);
   13.58 @@ -166,7 +166,7 @@
   13.59  section "Implicit definition of -e>: Abs(lift s 0 $ Var 0) -e> s";
   13.60  
   13.61  Goal "!i. (~free s i) = (? t. s = lift t i)";
   13.62 -by (dB.induct_tac "s" 1);
   13.63 +by (induct_tac "s" 1);
   13.64    by (Simp_tac 1);
   13.65    by (SELECT_GOAL(safe_tac HOL_cs)1);
   13.66     by (etac nat_neqE 1);
    14.1 --- a/src/HOL/Lambda/Eta.thy	Fri Jul 24 13:03:20 1998 +0200
    14.2 +++ b/src/HOL/Lambda/Eta.thy	Fri Jul 24 13:19:38 1998 +0200
    14.3 @@ -19,7 +19,7 @@
    14.4    "s -e>= t" == "(s,t) : eta^="
    14.5    "s ->=  t" == "(s,t) : beta^="
    14.6  
    14.7 -primrec free Lambda.dB
    14.8 +primrec
    14.9    "free (Var j) i = (j=i)"
   14.10    "free (s $ t) i = (free s i | free t i)"
   14.11    "free (Abs s) i = free s (Suc i)"
    15.1 --- a/src/HOL/Lambda/Lambda.ML	Fri Jul 24 13:03:20 1998 +0200
    15.2 +++ b/src/HOL/Lambda/Lambda.ML	Fri Jul 24 13:19:38 1998 +0200
    15.3 @@ -66,16 +66,16 @@
    15.4  
    15.5  Goal
    15.6    "!i k. i < Suc k --> lift (lift t i) (Suc k) = lift (lift t k) i";
    15.7 -by (dB.induct_tac "t" 1);
    15.8 +by (induct_tac "t" 1);
    15.9  by (ALLGOALS(asm_simp_tac (simpset() addSolver cut_trans_tac)));
   15.10  by (safe_tac HOL_cs);
   15.11  by (ALLGOALS trans_tac);
   15.12  qed_spec_mp "lift_lift";
   15.13  
   15.14  Goal "!i j s. j < Suc i --> lift (t[s/j]) i = (lift t (Suc i)) [lift s i / j]";
   15.15 -by (dB.induct_tac "t" 1);
   15.16 +by (induct_tac "t" 1);
   15.17  by (ALLGOALS(asm_simp_tac (simpset() addsimps [diff_Suc,subst_Var,lift_lift]
   15.18 -                                addsplits [split_nat_case]
   15.19 +                                addsplits [nat.split]
   15.20                                  addSolver cut_trans_tac)));
   15.21  by (safe_tac HOL_cs);
   15.22  by (ALLGOALS trans_tac);
   15.23 @@ -84,7 +84,7 @@
   15.24  
   15.25  Goal
   15.26    "!i j s. i < Suc j --> lift (t[s/j]) i = (lift t i) [lift s i / Suc j]";
   15.27 -by (dB.induct_tac "t" 1);
   15.28 +by (induct_tac "t" 1);
   15.29  by (ALLGOALS(asm_simp_tac (simpset() addsimps [subst_Var,lift_lift]
   15.30                                  addSolver cut_trans_tac)));
   15.31  by (safe_tac (HOL_cs addSEs [nat_neqE]));
   15.32 @@ -92,18 +92,18 @@
   15.33  qed "lift_subst_lt";
   15.34  
   15.35  Goal "!k s. (lift t k)[s/k] = t";
   15.36 -by (dB.induct_tac "t" 1);
   15.37 +by (induct_tac "t" 1);
   15.38  by (ALLGOALS Asm_full_simp_tac);
   15.39  qed "subst_lift";
   15.40  Addsimps [subst_lift];
   15.41  
   15.42  
   15.43  Goal "!i j u v. i < Suc j --> t[lift v i / Suc j][u[v/j]/i] = t[u/i][v/j]";
   15.44 -by (dB.induct_tac "t" 1);
   15.45 +by (induct_tac "t" 1);
   15.46  by (ALLGOALS(asm_simp_tac
   15.47        (simpset() addsimps [diff_Suc,subst_Var,lift_lift RS sym,lift_subst_lt]
   15.48                   delsplits [split_if]
   15.49 -                 addsplits [split_nat_case]
   15.50 +                 addsplits [nat.split]
   15.51                   addloop ("if",split_inside_tac[split_if])
   15.52                  addSolver cut_trans_tac)));
   15.53  by (safe_tac (HOL_cs addSEs [nat_neqE]));
   15.54 @@ -114,20 +114,20 @@
   15.55  (*** Equivalence proof for optimized substitution ***)
   15.56  
   15.57  Goal "!k. liftn 0 t k = t";
   15.58 -by (dB.induct_tac "t" 1);
   15.59 +by (induct_tac "t" 1);
   15.60  by (ALLGOALS(asm_simp_tac(addsplit(simpset()))));
   15.61  qed "liftn_0";
   15.62  Addsimps [liftn_0];
   15.63  
   15.64  Goal "!k. liftn (Suc n) t k = lift (liftn n t k) k";
   15.65 -by (dB.induct_tac "t" 1);
   15.66 +by (induct_tac "t" 1);
   15.67  by (ALLGOALS(asm_simp_tac(addsplit(simpset()))));
   15.68  by (blast_tac (claset() addDs [add_lessD1]) 1);
   15.69  qed "liftn_lift";
   15.70  Addsimps [liftn_lift];
   15.71  
   15.72  Goal "!n. substn t s n = t[liftn n s 0 / n]";
   15.73 -by (dB.induct_tac "t" 1);
   15.74 +by (induct_tac "t" 1);
   15.75  by (ALLGOALS(asm_simp_tac(addsplit(simpset()))));
   15.76  qed "substn_subst_n";
   15.77  Addsimps [substn_subst_n];
    16.1 --- a/src/HOL/Lambda/Lambda.thy	Fri Jul 24 13:03:20 1998 +0200
    16.2 +++ b/src/HOL/Lambda/Lambda.thy	Fri Jul 24 13:19:38 1998 +0200
    16.3 @@ -7,7 +7,7 @@
    16.4  substitution and beta-reduction.
    16.5  *)
    16.6  
    16.7 -Lambda = Arith + Inductive +
    16.8 +Lambda = Datatype +
    16.9  
   16.10  datatype dB = Var nat | "$" dB dB (infixl 200) | Abs dB
   16.11  
   16.12 @@ -18,23 +18,23 @@
   16.13    substn :: [dB,dB,nat] => dB
   16.14    liftn  :: [nat,dB,nat] => dB
   16.15  
   16.16 -primrec lift dB
   16.17 +primrec
   16.18    "lift (Var i) k = (if i < k then Var i else Var(Suc i))"
   16.19    "lift (s $ t) k = (lift s k) $ (lift t k)"
   16.20    "lift (Abs s) k = Abs(lift s (Suc k))"
   16.21  
   16.22 -primrec subst dB
   16.23 +primrec
   16.24    subst_Var "(Var i)[s/k] = (if k < i then Var(i-1)
   16.25                              else if i = k then s else Var i)"
   16.26    subst_App "(t $ u)[s/k] = t[s/k] $ u[s/k]"
   16.27    subst_Abs "(Abs t)[s/k] = Abs (t[lift s 0 / Suc k])"
   16.28  
   16.29 -primrec liftn dB
   16.30 +primrec
   16.31    "liftn n (Var i) k = (if i < k then Var i else Var(i+n))"
   16.32    "liftn n (s $ t) k = (liftn n s k) $ (liftn n t k)"
   16.33    "liftn n (Abs s) k = Abs(liftn n s (Suc k))"
   16.34  
   16.35 -primrec substn dB
   16.36 +primrec
   16.37    "substn (Var i) s k = (if k < i then Var(i-1)
   16.38                           else if i = k then liftn k s 0 else Var i)"
   16.39    "substn (t $ u) s k = (substn t s k) $ (substn u s k)"
    17.1 --- a/src/HOL/Lambda/ParRed.ML	Fri Jul 24 13:03:20 1998 +0200
    17.2 +++ b/src/HOL/Lambda/ParRed.ML	Fri Jul 24 13:19:38 1998 +0200
    17.3 @@ -26,7 +26,7 @@
    17.4  Addsimps [par_beta_varL];
    17.5  
    17.6  Goal "t => t";
    17.7 -by (dB.induct_tac "t" 1);
    17.8 +by (induct_tac "t" 1);
    17.9  by (ALLGOALS Asm_simp_tac);
   17.10  qed"par_beta_refl";
   17.11  Addsimps [par_beta_refl];
   17.12 @@ -52,14 +52,14 @@
   17.13  (*** => ***)
   17.14  
   17.15  Goal "!t' n. t => t' --> lift t n => lift t' n";
   17.16 -by (dB.induct_tac "t" 1);
   17.17 +by (induct_tac "t" 1);
   17.18  by (ALLGOALS(fast_tac (claset() addss (simpset()))));
   17.19  qed_spec_mp "par_beta_lift";
   17.20  Addsimps [par_beta_lift];
   17.21  
   17.22  Goal
   17.23    "!s s' t' n. s => s' --> t => t' --> t[s/n] => t'[s'/n]";
   17.24 -by (dB.induct_tac "t" 1);
   17.25 +by (induct_tac "t" 1);
   17.26    by (asm_simp_tac (addsplit(simpset())) 1);
   17.27   by (strip_tac 1);
   17.28   by (eresolve_tac par_beta_cases 1);
    18.1 --- a/src/HOL/Lex/AutoChopper.thy	Fri Jul 24 13:03:20 1998 +0200
    18.2 +++ b/src/HOL/Lex/AutoChopper.thy	Fri Jul 24 13:19:38 1998 +0200
    18.3 @@ -29,7 +29,8 @@
    18.4  consts
    18.5    acc :: "[('a,'s)da, 's, 'a list list*'a list, 'a list, 'a list, 'a list]
    18.6            => 'a list list * 'a list"
    18.7 -primrec acc List.list
    18.8 +
    18.9 +primrec
   18.10    "acc A s r ps []     zs = (if ps=[] then r else (ps#fst(r),snd(r)))" 
   18.11    "acc A s r ps (x#xs) zs =
   18.12              (let t = next A x s
    19.1 --- a/src/HOL/Lex/AutoMaxChop.thy	Fri Jul 24 13:03:20 1998 +0200
    19.2 +++ b/src/HOL/Lex/AutoMaxChop.thy	Fri Jul 24 13:19:38 1998 +0200
    19.3 @@ -8,7 +8,7 @@
    19.4  
    19.5  consts
    19.6   auto_split :: "('a,'s)da => 's  => 'a list * 'a list => 'a list => 'a splitter"
    19.7 -primrec auto_split list
    19.8 +primrec
    19.9  "auto_split A q res ps []     = (if fin A q then (ps,[]) else res)"
   19.10  "auto_split A q res ps (x#xs) =
   19.11     auto_split A (next A x q) (if fin A q then (ps,x#xs) else res) (ps@[x]) xs"
    20.1 --- a/src/HOL/Lex/MaxChop.ML	Fri Jul 24 13:03:20 1998 +0200
    20.2 +++ b/src/HOL/Lex/MaxChop.ML	Fri Jul 24 13:19:38 1998 +0200
    20.3 @@ -84,7 +84,7 @@
    20.4                          addsplits [split_split]) 1);
    20.5  by (Clarify_tac 1);
    20.6  by (rename_tac "xs1 ys1 xss1 ys" 1);
    20.7 -by (split_asm_tac [split_list_case_asm] 1);
    20.8 +by (split_asm_tac [list.split_asm] 1);
    20.9   by (Asm_full_simp_tac 1);
   20.10   by (full_simp_tac (simpset() addsimps [is_maxpref_def]) 1);
   20.11   by (blast_tac (claset() addIs [prefix_append RS iffD2]) 1);
    21.1 --- a/src/HOL/Lex/MaxPrefix.thy	Fri Jul 24 13:03:20 1998 +0200
    21.2 +++ b/src/HOL/Lex/MaxPrefix.thy	Fri Jul 24 13:19:38 1998 +0200
    21.3 @@ -19,7 +19,7 @@
    21.4  
    21.5  consts
    21.6   maxsplit :: "('a list => bool) => 'a list * 'a list => 'a list => 'a splitter"
    21.7 -primrec maxsplit list
    21.8 +primrec
    21.9  "maxsplit P res ps []     = (if P ps then (ps,[]) else res)"
   21.10  "maxsplit P res ps (q#qs) = maxsplit P (if P ps then (ps,q#qs) else res)
   21.11                                       (ps@[q]) qs"
    22.1 --- a/src/HOL/Lex/NA.thy	Fri Jul 24 13:03:20 1998 +0200
    22.2 +++ b/src/HOL/Lex/NA.thy	Fri Jul 24 13:19:38 1998 +0200
    22.3 @@ -11,7 +11,7 @@
    22.4  types ('a,'s)na = "'s * ('a => 's => 's set) * ('s => bool)"
    22.5  
    22.6  consts delta :: "('a,'s)na => 'a list => 's => 's set"
    22.7 -primrec delta list
    22.8 +primrec
    22.9  "delta A []    p = {p}"
   22.10  "delta A (a#w) p = Union(delta A w `` next A a p)"
   22.11  
    23.1 --- a/src/HOL/Lex/NAe.thy	Fri Jul 24 13:03:20 1998 +0200
    23.2 +++ b/src/HOL/Lex/NAe.thy	Fri Jul 24 13:19:38 1998 +0200
    23.3 @@ -18,7 +18,7 @@
    23.4  translations "eps A" == "step A None"
    23.5  
    23.6  consts steps :: "('a,'s)nae => 'a list =>   ('s * 's)set"
    23.7 -primrec steps list
    23.8 +primrec
    23.9  "steps A [] = (eps A)^*"
   23.10  "steps A (a#w) = steps A w  O  step A (Some a)  O  (eps A)^*"
   23.11  
   23.12 @@ -28,7 +28,7 @@
   23.13  
   23.14  (* not really used:
   23.15  consts delta :: "('a,'s)nae => 'a list => 's => 's set"
   23.16 -primrec delta list
   23.17 +primrec
   23.18  "delta A [] s = (eps A)^* ^^ {s}"
   23.19  "delta A (a#w) s = lift(delta A w) (lift(next A (Some a)) ((eps A)^* ^^ {s}))"
   23.20  *)
    24.1 --- a/src/HOL/Lex/Prefix.ML	Fri Jul 24 13:03:20 1998 +0200
    24.2 +++ b/src/HOL/Lex/Prefix.ML	Fri Jul 24 13:19:38 1998 +0200
    24.3 @@ -7,7 +7,7 @@
    24.4  (* Junk: *)
    24.5  val [maj,min] = goal Prefix.thy "[| Q([]); !! y ys. Q(y#ys) |] ==> ! l. Q(l)";
    24.6  by (rtac allI 1);
    24.7 -by (list.induct_tac "l" 1);
    24.8 +by (induct_tac "l" 1);
    24.9  by (rtac maj 1);
   24.10  by (rtac min 1);
   24.11  val list_cases = result();
   24.12 @@ -37,7 +37,7 @@
   24.13  AddIffs[Nil_prefix];
   24.14  
   24.15  Goalw [prefix_def] "(xs <= []) = (xs = [])";
   24.16 -by (list.induct_tac "xs" 1);
   24.17 +by (induct_tac "xs" 1);
   24.18  by (Simp_tac 1);
   24.19  by (Simp_tac 1);
   24.20  qed "prefix_Nil";
   24.21 @@ -83,7 +83,7 @@
   24.22  (* nicht sehr elegant bewiesen - Induktion eigentlich ueberfluessig *)
   24.23  Goalw [prefix_def]
   24.24     "(xs <= y#ys) = (xs=[] | (? zs. xs=y#zs & zs <= ys))";
   24.25 -by (list.induct_tac "xs" 1);
   24.26 +by (induct_tac "xs" 1);
   24.27  by (Simp_tac 1);
   24.28  by (Simp_tac 1);
   24.29  by (Fast_tac 1);
    25.1 --- a/src/HOL/Lex/RegExp.thy	Fri Jul 24 13:03:20 1998 +0200
    25.2 +++ b/src/HOL/Lex/RegExp.thy	Fri Jul 24 13:19:38 1998 +0200
    25.3 @@ -15,7 +15,7 @@
    25.4                   | Star ('a rexp)
    25.5  
    25.6  consts lang :: 'a rexp => 'a list set
    25.7 -primrec lang rexp
    25.8 +primrec
    25.9  lang_Emp  "lang Empty = {}"
   25.10  lang_Atom "lang (Atom a) = {[a]}"
   25.11  lang_Un   "lang (Union el er) = (lang el) Un (lang er)"
    26.1 --- a/src/HOL/Lex/RegExp2NAe.ML	Fri Jul 24 13:03:20 1998 +0200
    26.2 +++ b/src/HOL/Lex/RegExp2NAe.ML	Fri Jul 24 13:19:38 1998 +0200
    26.3 @@ -446,7 +446,7 @@
    26.4  
    26.5  Goalw [conc_def]
    26.6   "!L R. fin(conc L R) p = (? s. p = False#s & fin R s)";
    26.7 -by (simp_tac (simpset() addsplits [split_list_case]) 1);
    26.8 +by (simp_tac (simpset() addsplits [list.split]) 1);
    26.9  qed_spec_mp "final_conc";
   26.10  
   26.11  Goal
    27.1 --- a/src/HOL/Lex/RegExp2NAe.thy	Fri Jul 24 13:03:20 1998 +0200
    27.2 +++ b/src/HOL/Lex/RegExp2NAe.thy	Fri Jul 24 13:19:38 1998 +0200
    27.3 @@ -50,7 +50,7 @@
    27.4      %s. case s of [] => True | left#s => left & f s)"
    27.5  
    27.6  consts rexp2nae :: 'a rexp => 'a bitsNAe
    27.7 -primrec rexp2nae rexp
    27.8 +primrec
    27.9  "rexp2nae Empty      = ([], %a s. {}, %s. False)"
   27.10  "rexp2nae(Atom a)    = atom a"
   27.11  "rexp2nae(Union r s) = union (rexp2nae r) (rexp2nae s)"
    28.1 --- a/src/HOL/Lex/RegSet_of_nat_DA.ML	Fri Jul 24 13:03:20 1998 +0200
    28.2 +++ b/src/HOL/Lex/RegSet_of_nat_DA.ML	Fri Jul 24 13:19:38 1998 +0200
    28.3 @@ -140,7 +140,7 @@
    28.4   "!i j xs. xs : regset d i j k = \
    28.5  \          ((!n:set(butlast(trace d i xs)). n < k) & deltas d xs i = j)";
    28.6  by (induct_tac "k" 1);
    28.7 - by (simp_tac (simpset() addcongs [conj_cong] addsplits [split_list_case]) 1);
    28.8 + by (simp_tac (simpset() addcongs [conj_cong] addsplits [list.split]) 1);
    28.9  by (strip_tac 1);
   28.10  by (asm_simp_tac (simpset() addsimps [conc_def]) 1);
   28.11  by (rtac iffI 1);
   28.12 @@ -149,12 +149,12 @@
   28.13   by (REPEAT(eresolve_tac[exE,conjE] 1));
   28.14   by (Asm_full_simp_tac 1);
   28.15   by (subgoal_tac
   28.16 -      "(!n:set(butlast(trace d k xsb)). n < Suc k) & deltas d xsb k = k" 1);
   28.17 +      "(!m:set(butlast(trace d n xsb)). m < Suc n) & deltas d xsb n = n" 1);
   28.18    by (asm_simp_tac (simpset() addsimps [set_trace_conv,butlast_append,ball_Un]) 1);
   28.19   by (etac star.induct 1);
   28.20    by (Simp_tac 1);
   28.21   by (asm_full_simp_tac (simpset() addsimps [set_trace_conv,butlast_append,ball_Un]) 1);
   28.22 -by (case_tac "k : set(butlast(trace d i xs))" 1);
   28.23 +by (case_tac "n : set(butlast(trace d i xs))" 1);
   28.24   by (rtac disjI1 2);
   28.25   by (blast_tac (claset() addIs [lemma]) 2);
   28.26  by (rtac disjI2 1);
    29.1 --- a/src/HOL/Lex/RegSet_of_nat_DA.thy	Fri Jul 24 13:03:20 1998 +0200
    29.2 +++ b/src/HOL/Lex/RegSet_of_nat_DA.thy	Fri Jul 24 13:19:38 1998 +0200
    29.3 @@ -23,14 +23,14 @@
    29.4  translations "deltas" == "foldl2"
    29.5  
    29.6  consts trace :: 'a nat_next => nat => 'a list => nat list
    29.7 -primrec trace list
    29.8 +primrec
    29.9  "trace d i [] = []"
   29.10  "trace d i (x#xs) = d x i # trace d (d x i) xs"
   29.11  
   29.12  (* conversion a la Warshall *)
   29.13  
   29.14  consts regset :: 'a nat_next => nat => nat => nat => 'a list set
   29.15 -primrec regset nat
   29.16 +primrec
   29.17  "regset d i j 0 = (if i=j then insert [] {[a] | a. d a i = j}
   29.18                            else {[a] | a. d a i = j})"
   29.19  "regset d i j (Suc k) = regset d i j k Un
    30.1 --- a/src/HOL/MiniML/Generalize.ML	Fri Jul 24 13:03:20 1998 +0200
    30.2 +++ b/src/HOL/MiniML/Generalize.ML	Fri Jul 24 13:19:38 1998 +0200
    30.3 @@ -7,12 +7,12 @@
    30.4  AddSEs [equalityE];
    30.5  
    30.6  Goal "free_tv A = free_tv B ==> gen A t = gen B t";
    30.7 -by (typ.induct_tac "t" 1);
    30.8 +by (induct_tac "t" 1);
    30.9  by (ALLGOALS Asm_simp_tac);
   30.10  qed "gen_eq_on_free_tv";
   30.11  
   30.12  Goal "(free_tv t) <= (free_tv sch) --> gen sch t = (mk_scheme t)";
   30.13 -by (typ.induct_tac "t" 1);
   30.14 +by (induct_tac "t" 1);
   30.15  by (Asm_simp_tac 1);
   30.16  by (Simp_tac 1);
   30.17  by (Fast_tac 1);
   30.18 @@ -21,7 +21,7 @@
   30.19  Addsimps [gen_without_effect];
   30.20  
   30.21  Goal "free_tv (gen ($ S A) t) = free_tv t Int free_tv ($ S A)";
   30.22 -by (typ.induct_tac "t" 1);
   30.23 +by (induct_tac "t" 1);
   30.24  by (Simp_tac 1);
   30.25  by (case_tac "nat : free_tv ($ S A)" 1);
   30.26  by (Asm_simp_tac 1);
   30.27 @@ -42,7 +42,7 @@
   30.28  Addsimps [free_tv_gen_cons];
   30.29  
   30.30  Goal "bound_tv (gen A t1) = (free_tv t1) - (free_tv A)";
   30.31 -by (typ.induct_tac "t1" 1);
   30.32 +by (induct_tac "t1" 1);
   30.33  by (Simp_tac 1);
   30.34  by (case_tac "nat : free_tv A" 1);
   30.35  by (Asm_simp_tac 1);
   30.36 @@ -55,7 +55,7 @@
   30.37  Addsimps [bound_tv_gen];
   30.38  
   30.39  Goal "new_tv n t --> new_tv n (gen A t)";
   30.40 -by (typ.induct_tac "t" 1);
   30.41 +by (induct_tac "t" 1);
   30.42  by (Simp_tac 1);
   30.43  by (case_tac "nat : free_tv A" 1);
   30.44  by (Asm_simp_tac 1);
   30.45 @@ -63,7 +63,7 @@
   30.46  qed_spec_mp "new_tv_compatible_gen";
   30.47  
   30.48  Goalw [gen_ML_def] "gen A t = gen_ML A t";
   30.49 -by (typ.induct_tac "t" 1);
   30.50 +by (induct_tac "t" 1);
   30.51  by (simp_tac (simpset() addsimps [free_tv_ML_scheme_list]) 1);
   30.52  by (asm_simp_tac (simpset() addsimps [free_tv_ML_scheme_list]) 1);
   30.53  qed "gen_eq_gen_ML";
   30.54 @@ -85,7 +85,7 @@
   30.55  qed_spec_mp "gen_subst_commutes";
   30.56  
   30.57  Goal "free_tv(t::typ) <= free_tv(A) --> bound_typ_inst S (gen A t) = t";
   30.58 -by (typ.induct_tac "t" 1);
   30.59 +by (induct_tac "t" 1);
   30.60  by (ALLGOALS Asm_simp_tac);
   30.61  by (Fast_tac 1);
   30.62  qed_spec_mp "bound_typ_inst_gen";
   30.63 @@ -96,7 +96,7 @@
   30.64  by Safe_tac;
   30.65  by (rename_tac "R" 1);
   30.66  by (res_inst_tac [("x", "(%a. bound_typ_inst R (gen ($S A) (S a)))")] exI 1);
   30.67 -by (typ.induct_tac "t" 1);
   30.68 +by (induct_tac "t" 1);
   30.69   by (Simp_tac 1);
   30.70  by (Asm_simp_tac 1);
   30.71  qed "gen_bound_typ_instance";
   30.72 @@ -106,7 +106,7 @@
   30.73  by Safe_tac;
   30.74  by (rename_tac "S" 1);
   30.75  by (res_inst_tac [("x","%b. if b:free_tv A then TVar b else S b")] exI 1);
   30.76 -by (typ.induct_tac "t" 1);
   30.77 +by (induct_tac "t" 1);
   30.78   by (Asm_simp_tac 1);
   30.79   by (Fast_tac 1);
   30.80  by (Asm_simp_tac 1);
   30.81 @@ -119,7 +119,7 @@
   30.82  by (etac exE 1);
   30.83  by (hyp_subst_tac 1);
   30.84  by (res_inst_tac [("x","(%x. S (if n <= x then x - n else x))")] exI 1);
   30.85 -by (typ.induct_tac "t" 1);
   30.86 +by (induct_tac "t" 1);
   30.87  by (Simp_tac 1);
   30.88  by (case_tac "nat : free_tv A" 1);
   30.89  by (Asm_simp_tac 1);
    31.1 --- a/src/HOL/MiniML/Generalize.thy	Fri Jul 24 13:03:20 1998 +0200
    31.2 +++ b/src/HOL/MiniML/Generalize.thy	Fri Jul 24 13:19:38 1998 +0200
    31.3 @@ -16,7 +16,7 @@
    31.4  consts
    31.5    gen :: [ctxt, typ] => type_scheme
    31.6  
    31.7 -primrec gen typ
    31.8 +primrec
    31.9    "gen A (TVar n) = (if (n:(free_tv A)) then (FVar n) else (BVar n))"
   31.10    "gen A (t1 -> t2) = (gen A t1) =-> (gen A t2)"
   31.11  
   31.12 @@ -25,7 +25,7 @@
   31.13  consts
   31.14    gen_ML_aux :: [nat list, typ] => type_scheme
   31.15  
   31.16 -primrec gen_ML_aux typ
   31.17 +primrec
   31.18    "gen_ML_aux A (TVar n) = (if (n mem A) then (FVar n) else (BVar n))"
   31.19    "gen_ML_aux A (t1 -> t2) = (gen_ML_aux A t1) =-> (gen_ML_aux A t2)"
   31.20  
    32.1 --- a/src/HOL/MiniML/Instance.ML	Fri Jul 24 13:03:20 1998 +0200
    32.2 +++ b/src/HOL/MiniML/Instance.ML	Fri Jul 24 13:19:38 1998 +0200
    32.3 @@ -10,14 +10,14 @@
    32.4  (* lemmatas for bound_typ_inst *)
    32.5  
    32.6  Goal "bound_typ_inst S (mk_scheme t) = t";
    32.7 -by (typ.induct_tac "t" 1);
    32.8 +by (induct_tac "t" 1);
    32.9  by (ALLGOALS Asm_simp_tac);
   32.10  qed "bound_typ_inst_mk_scheme";
   32.11  
   32.12  Addsimps [bound_typ_inst_mk_scheme];
   32.13  
   32.14  Goal "bound_typ_inst ($S o R) ($S sch) = $S (bound_typ_inst R sch)";
   32.15 -by (type_scheme.induct_tac "sch" 1);
   32.16 +by (induct_tac "sch" 1);
   32.17  by (ALLGOALS Asm_full_simp_tac);
   32.18  qed "bound_typ_inst_composed_subst";
   32.19  
   32.20 @@ -32,7 +32,7 @@
   32.21  (* lemmatas for bound_scheme_inst *)
   32.22  
   32.23  Goal "bound_scheme_inst B (mk_scheme t) = mk_scheme t";
   32.24 -by (typ.induct_tac "t" 1);
   32.25 +by (induct_tac "t" 1);
   32.26  by (Simp_tac 1);
   32.27  by (Asm_simp_tac 1);
   32.28  qed "bound_scheme_inst_mk_scheme";
   32.29 @@ -40,7 +40,7 @@
   32.30  Addsimps [bound_scheme_inst_mk_scheme];
   32.31  
   32.32  Goal "$S (bound_scheme_inst B sch) = (bound_scheme_inst ($S o B) ($ S sch))";
   32.33 -by (type_scheme.induct_tac "sch" 1);
   32.34 +by (induct_tac "sch" 1);
   32.35  by (Simp_tac 1);
   32.36  by (Simp_tac 1);
   32.37  by (Asm_simp_tac 1);
   32.38 @@ -48,7 +48,7 @@
   32.39  
   32.40  Goal "!t. mk_scheme t = bound_scheme_inst B sch --> \
   32.41  \         (? S. !x:bound_tv sch. B x = mk_scheme (S x))";
   32.42 -by (type_scheme.induct_tac "sch" 1);
   32.43 +by (induct_tac "sch" 1);
   32.44  by (Simp_tac 1);
   32.45  by Safe_tac;
   32.46  by (rtac exI 1);
   32.47 @@ -81,7 +81,7 @@
   32.48  
   32.49  Goal "new_tv n sch --> subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) \
   32.50  \                                                 (bound_typ_inst (%k. TVar (k + n)) sch) = sch";
   32.51 -by (type_scheme.induct_tac "sch" 1);
   32.52 +by (induct_tac "sch" 1);
   32.53  by (simp_tac (simpset() addsimps [leD]) 1);
   32.54  by (simp_tac (simpset() addsimps [le_add2,diff_add_inverse2]) 1);
   32.55  by (Asm_simp_tac 1);
   32.56 @@ -96,7 +96,7 @@
   32.57  Goal "new_tv n sch --> \
   32.58  \     subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) (bound_typ_inst S sch) = \
   32.59  \      bound_scheme_inst ((subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k)) o S) sch";
   32.60 -by (type_scheme.induct_tac "sch" 1);
   32.61 +by (induct_tac "sch" 1);
   32.62  by (simp_tac (simpset() addsimps [leD]) 1);
   32.63  by (Asm_simp_tac 1);
   32.64  by (asm_full_simp_tac (simpset() addsimps [leD]) 1);
   32.65 @@ -127,7 +127,7 @@
   32.66  by (asm_simp_tac (simpset() addsimps [aux2]) 1);
   32.67  by Safe_tac;
   32.68  by (res_inst_tac [("x","%n. bound_typ_inst S (B n)")] exI 1);
   32.69 -by (type_scheme.induct_tac "sch" 1);
   32.70 +by (induct_tac "sch" 1);
   32.71  by (Simp_tac 1);
   32.72  by (Simp_tac 1);
   32.73  by (Asm_simp_tac 1);
   32.74 @@ -145,7 +145,7 @@
   32.75  by (rotate_tac 1 1);
   32.76  by (rtac mp 1);
   32.77  by (assume_tac 2);
   32.78 -by (type_scheme.induct_tac "sch" 1);
   32.79 +by (induct_tac "sch" 1);
   32.80  by (Simp_tac 1);
   32.81  by (Asm_full_simp_tac 1);
   32.82  by (Fast_tac 1);
   32.83 @@ -154,7 +154,7 @@
   32.84  by (etac exE 1);
   32.85  by (Asm_full_simp_tac 1);
   32.86  by (rtac exI 1);
   32.87 -by (type_scheme.induct_tac "sch" 1);
   32.88 +by (induct_tac "sch" 1);
   32.89  by (Simp_tac 1);
   32.90  by (Simp_tac 1);
   32.91  by (Asm_full_simp_tac 1);
   32.92 @@ -172,7 +172,7 @@
   32.93  by (rtac conjI 1);
   32.94   by (Fast_tac 1);
   32.95  by (rtac allI 1);
   32.96 -by (nat_ind_tac "i" 1);
   32.97 +by (induct_tac "i" 1);
   32.98  by (ALLGOALS Asm_simp_tac);
   32.99  qed "le_env_Cons";
  32.100  AddIffs [le_env_Cons];
  32.101 @@ -221,7 +221,7 @@
  32.102  
  32.103  Goalw [le_type_scheme_def,is_bound_typ_instance]
  32.104   "(sch <= FVar n) = (sch = FVar n)";
  32.105 -by (type_scheme.induct_tac "sch" 1);
  32.106 +by (induct_tac "sch" 1);
  32.107    by (Simp_tac 1);
  32.108   by (Simp_tac 1);
  32.109   by (Fast_tac 1);
  32.110 @@ -249,26 +249,26 @@
  32.111  qed "Fun_le_FunD";
  32.112  
  32.113  Goal "(sch' <= sch1 =-> sch2) --> (? sch'1 sch'2. sch' = sch'1 =-> sch'2)";
  32.114 -by (type_scheme.induct_tac "sch'" 1);
  32.115 +by (induct_tac "sch'" 1);
  32.116  by (Asm_simp_tac 1);
  32.117  by (Asm_simp_tac 1);
  32.118  by (Fast_tac 1);
  32.119  qed_spec_mp "scheme_le_Fun";
  32.120  
  32.121  Goal "!sch'::type_scheme. sch <= sch' --> free_tv sch' <= free_tv sch";
  32.122 -by (type_scheme.induct_tac "sch" 1);
  32.123 +by (induct_tac "sch" 1);
  32.124    by (rtac allI 1);
  32.125 -  by (type_scheme.induct_tac "sch'" 1);
  32.126 +  by (induct_tac "sch'" 1);
  32.127      by (Simp_tac 1);
  32.128     by (Simp_tac 1);
  32.129    by (Simp_tac 1);
  32.130   by (rtac allI 1);
  32.131 - by (type_scheme.induct_tac "sch'" 1);
  32.132 + by (induct_tac "sch'" 1);
  32.133     by (Simp_tac 1);
  32.134    by (Simp_tac 1);
  32.135   by (Simp_tac 1);
  32.136  by (rtac allI 1);
  32.137 -by (type_scheme.induct_tac "sch'" 1);
  32.138 +by (induct_tac "sch'" 1);
  32.139    by (Simp_tac 1);
  32.140   by (Simp_tac 1);
  32.141  by (Asm_full_simp_tac 1);
  32.142 @@ -278,10 +278,10 @@
  32.143  qed_spec_mp "le_type_scheme_free_tv";
  32.144  
  32.145  Goal "!A::type_scheme list. A <= B --> free_tv B <= free_tv A";
  32.146 -by (list.induct_tac "B" 1);
  32.147 +by (induct_tac "B" 1);
  32.148   by (Simp_tac 1);
  32.149  by (rtac allI 1);
  32.150 -by (list.induct_tac "A" 1);
  32.151 +by (induct_tac "A" 1);
  32.152   by (simp_tac (simpset() addsimps [le_env_def]) 1);
  32.153  by (Simp_tac 1);
  32.154  by (fast_tac (claset() addDs [le_type_scheme_free_tv]) 1);
    33.1 --- a/src/HOL/MiniML/Instance.thy	Fri Jul 24 13:03:20 1998 +0200
    33.2 +++ b/src/HOL/MiniML/Instance.thy	Fri Jul 24 13:19:38 1998 +0200
    33.3 @@ -14,7 +14,7 @@
    33.4  consts
    33.5    bound_typ_inst :: [subst, type_scheme] => typ
    33.6  
    33.7 -primrec bound_typ_inst type_scheme
    33.8 +primrec
    33.9    "bound_typ_inst S (FVar n) = (TVar n)"
   33.10    "bound_typ_inst S (BVar n) = (S n)"
   33.11    "bound_typ_inst S (sch1 =-> sch2) = ((bound_typ_inst S sch1) -> (bound_typ_inst S sch2))"
   33.12 @@ -22,7 +22,7 @@
   33.13  consts
   33.14    bound_scheme_inst :: [nat => type_scheme, type_scheme] => type_scheme
   33.15  
   33.16 -primrec bound_scheme_inst type_scheme
   33.17 +primrec
   33.18    "bound_scheme_inst S (FVar n) = (FVar n)"
   33.19    "bound_scheme_inst S (BVar n) = (S n)"
   33.20    "bound_scheme_inst S (sch1 =-> sch2) = ((bound_scheme_inst S sch1) =-> (bound_scheme_inst S sch2))"
   33.21 @@ -38,7 +38,7 @@
   33.22  consts
   33.23    subst_to_scheme :: [nat => type_scheme, typ] => type_scheme
   33.24  
   33.25 -primrec subst_to_scheme typ
   33.26 +primrec
   33.27    "subst_to_scheme B (TVar n) = (B n)"
   33.28    "subst_to_scheme B (t1 -> t2) = ((subst_to_scheme B t1) =-> (subst_to_scheme B t2))"
   33.29    
    34.1 --- a/src/HOL/MiniML/Maybe.ML	Fri Jul 24 13:03:20 1998 +0200
    34.2 +++ b/src/HOL/MiniML/Maybe.ML	Fri Jul 24 13:19:38 1998 +0200
    34.3 @@ -18,7 +18,7 @@
    34.4  (* expansion of option_bind *)
    34.5  Goalw [option_bind_def] "P(option_bind res f) = \
    34.6  \         ((res = None --> P None) & (!s. res = Some s --> P(f s)))";
    34.7 -by (rtac split_option_case 1);
    34.8 +by (rtac option.split 1);
    34.9  qed "split_option_bind";
   34.10  
   34.11  Goal
    35.1 --- a/src/HOL/MiniML/MiniML.ML	Fri Jul 24 13:03:20 1998 +0200
    35.2 +++ b/src/HOL/MiniML/MiniML.ML	Fri Jul 24 13:19:38 1998 +0200
    35.3 @@ -47,22 +47,22 @@
    35.4  qed "alpha_A";
    35.5  
    35.6  Goal "$ (S o alpha) (t::typ) = $ S ($ (%x. TVar (alpha x)) t)";
    35.7 -by (typ.induct_tac "t" 1);
    35.8 +by (induct_tac "t" 1);
    35.9  by (ALLGOALS (Asm_full_simp_tac));
   35.10  qed "S_o_alpha_typ";
   35.11  
   35.12  Goal "$ (%u. (S o alpha) u) (t::typ) = $ S ($ (%x. TVar (alpha x)) t)";
   35.13 -by (typ.induct_tac "t" 1);
   35.14 +by (induct_tac "t" 1);
   35.15  by (ALLGOALS (Asm_full_simp_tac));
   35.16  val S_o_alpha_typ' = result ();
   35.17  
   35.18  Goal "$ (S o alpha) (sch::type_scheme) = $ S ($ (%x. TVar (alpha x)) sch)";
   35.19 -by (type_scheme.induct_tac "sch" 1);
   35.20 +by (induct_tac "sch" 1);
   35.21  by (ALLGOALS (Asm_full_simp_tac));
   35.22  qed "S_o_alpha_type_scheme";
   35.23  
   35.24  Goal "$ (S o alpha) (A::type_scheme list) = $ S ($ (%x. TVar (alpha x)) A)";
   35.25 -by (list.induct_tac "A" 1);
   35.26 +by (induct_tac "A" 1);
   35.27  by (ALLGOALS (Asm_full_simp_tac));
   35.28  by (rtac (rewrite_rule [o_def] S_o_alpha_type_scheme) 1);
   35.29  qed "S_o_alpha_type_scheme_list";
   35.30 @@ -106,7 +106,7 @@
   35.31  Goal "!!t1::typ. \
   35.32  \     (free_tv ($ (%x. TVar (if x : free_tv A then x else n + x)) t1) - free_tv A) <= \
   35.33  \         {x. ? y. x = n + y}";
   35.34 -by (typ.induct_tac "t1" 1);
   35.35 +by (induct_tac "t1" 1);
   35.36  by (Simp_tac 1);
   35.37  by (Fast_tac 1);
   35.38  by (Simp_tac 1);
   35.39 @@ -143,7 +143,7 @@
   35.40  
   35.41  Goal "!A::type_scheme list. new_tv n A --> {x. ? y. x = n + y} Int free_tv A = {}";
   35.42  by (rtac allI 1);
   35.43 -by (list.induct_tac "A" 1);
   35.44 +by (induct_tac "A" 1);
   35.45  by (Simp_tac 1);
   35.46  by (Simp_tac 1);
   35.47  by (fast_tac (claset() addDs [new_tv_Int_free_tv_empty_scheme ]) 1);
   35.48 @@ -155,7 +155,7 @@
   35.49  by (etac exE 1);
   35.50  by (hyp_subst_tac 1);
   35.51  by (res_inst_tac [("x","(%x. S (if n <= x then x - n else x))")] exI 1);
   35.52 -by (typ.induct_tac "t" 1);
   35.53 +by (induct_tac "t" 1);
   35.54  by (Simp_tac 1);
   35.55  by (case_tac "nat : free_tv A" 1);
   35.56  by (Asm_simp_tac 1);
    36.1 --- a/src/HOL/MiniML/Type.ML	Fri Jul 24 13:03:20 1998 +0200
    36.2 +++ b/src/HOL/MiniML/Type.ML	Fri Jul 24 13:19:38 1998 +0200
    36.3 @@ -10,33 +10,33 @@
    36.4  (* lemmata for make scheme *)
    36.5  
    36.6  Goal "mk_scheme t = sch1 =-> sch2 --> (? t1 t2. sch1 = mk_scheme t1 & sch2 = mk_scheme t2)";
    36.7 -by (typ.induct_tac "t" 1);
    36.8 +by (induct_tac "t" 1);
    36.9  by (Simp_tac 1);
   36.10  by (Asm_full_simp_tac 1);
   36.11  by (Fast_tac 1);
   36.12  qed_spec_mp "mk_scheme_Fun";
   36.13  
   36.14  Goal "!t'. mk_scheme t = mk_scheme t' --> t=t'";
   36.15 -by (typ.induct_tac "t" 1);
   36.16 +by (induct_tac "t" 1);
   36.17   by (rtac allI 1);
   36.18 - by (typ.induct_tac "t'" 1);
   36.19 + by (induct_tac "t'" 1);
   36.20    by (Simp_tac 1);
   36.21   by (Asm_full_simp_tac 1);
   36.22  by (rtac allI 1);
   36.23 -by (typ.induct_tac "t'" 1);
   36.24 +by (induct_tac "t'" 1);
   36.25   by (Simp_tac 1);
   36.26  by (Asm_full_simp_tac 1);
   36.27  qed_spec_mp "mk_scheme_injective";
   36.28  
   36.29  Goal "free_tv (mk_scheme t) = free_tv t";
   36.30 -by (typ.induct_tac "t" 1);
   36.31 +by (induct_tac "t" 1);
   36.32  by (ALLGOALS Asm_simp_tac);
   36.33  qed "free_tv_mk_scheme";
   36.34  
   36.35  Addsimps [free_tv_mk_scheme];
   36.36  
   36.37  Goal "$ S (mk_scheme t) = mk_scheme ($ S t)";
   36.38 -by (typ.induct_tac "t" 1);
   36.39 +by (induct_tac "t" 1);
   36.40  by (ALLGOALS Asm_simp_tac);
   36.41  qed "subst_mk_scheme";
   36.42  
   36.43 @@ -110,14 +110,14 @@
   36.44  
   36.45  Goal "new_tv n (sch::type_scheme) --> \
   36.46  \     $(%k. if k<n then S k else S' k) sch = $S sch";
   36.47 -by (type_scheme.induct_tac "sch" 1);
   36.48 +by (induct_tac "sch" 1);
   36.49  by (ALLGOALS Asm_simp_tac);
   36.50  qed "new_if_subst_type_scheme";
   36.51  Addsimps [new_if_subst_type_scheme];
   36.52  
   36.53  Goal "new_tv n (A::type_scheme list) --> \
   36.54  \     $(%k. if k<n then S k else S' k) A = $S A";
   36.55 -by (list.induct_tac "A" 1);
   36.56 +by (induct_tac "A" 1);
   36.57  by (ALLGOALS Asm_simp_tac);
   36.58  qed "new_if_subst_type_scheme_list";
   36.59  Addsimps [new_if_subst_type_scheme_list];
   36.60 @@ -147,7 +147,7 @@
   36.61  Addsimps [free_tv_id_subst];
   36.62  
   36.63  Goal "!n. n < length A --> x : free_tv (A!n) --> x : free_tv A";
   36.64 -by (list.induct_tac "A" 1);
   36.65 +by (induct_tac "A" 1);
   36.66  by (Asm_full_simp_tac 1);
   36.67  by (rtac allI 1);
   36.68  by (res_inst_tac [("n","n")] nat_induct 1);
   36.69 @@ -158,7 +158,7 @@
   36.70  Addsimps [free_tv_nth_A_impl_free_tv_A];
   36.71  
   36.72  Goal "!nat. nat < length A --> x : free_tv (A!nat) --> x : free_tv A";
   36.73 -by (list.induct_tac "A" 1);
   36.74 +by (induct_tac "A" 1);
   36.75  by (Asm_full_simp_tac 1);
   36.76  by (rtac allI 1);
   36.77  by (res_inst_tac [("n","nat")] nat_induct 1);
   36.78 @@ -173,7 +173,7 @@
   36.79     occurring in the type structure *)
   36.80  
   36.81  Goal "(!x:free_tv t. (S x) = (S' x)) --> $ S (t::typ) = $ S' t";
   36.82 -by (typ.induct_tac "t" 1);
   36.83 +by (induct_tac "t" 1);
   36.84  by (Simp_tac 1);
   36.85  by (Asm_full_simp_tac 1);
   36.86  qed_spec_mp "typ_substitutions_only_on_free_variables";
   36.87 @@ -184,7 +184,7 @@
   36.88  qed "eq_free_eq_subst_te";
   36.89  
   36.90  Goal "(!x:free_tv sch. (S x) = (S' x)) --> $ S (sch::type_scheme) = $ S' sch";
   36.91 -by (type_scheme.induct_tac "sch" 1);
   36.92 +by (induct_tac "sch" 1);
   36.93  by (Simp_tac 1);
   36.94  by (Simp_tac 1);
   36.95  by (Asm_full_simp_tac 1);
   36.96 @@ -198,7 +198,7 @@
   36.97  
   36.98  Goal
   36.99    "(!n. n:(free_tv A) --> S1 n = S2 n) --> $S1 (A::type_scheme list) = $S2 A";
  36.100 -by (list.induct_tac "A" 1); 
  36.101 +by (induct_tac "A" 1); 
  36.102  (* case [] *)
  36.103  by (fast_tac (HOL_cs addss simpset()) 1);
  36.104  (* case x#xl *)
  36.105 @@ -210,7 +210,7 @@
  36.106  val weaken_asm_Un = result ();
  36.107  
  36.108  Goal "(!x:free_tv A. (S x) = (S' x)) --> $ S (A::type_scheme list) = $ S' A";
  36.109 -by (list.induct_tac "A" 1);
  36.110 +by (induct_tac "A" 1);
  36.111  by (Simp_tac 1);
  36.112  by (Asm_full_simp_tac 1);
  36.113  by (rtac weaken_asm_Un 1);
  36.114 @@ -220,7 +220,7 @@
  36.115  
  36.116  Goal
  36.117    "$ S1 (t::typ) = $ S2 t --> n:(free_tv t) --> S1 n = S2 n";
  36.118 -by (typ.induct_tac "t" 1);
  36.119 +by (induct_tac "t" 1);
  36.120  (* case TVar n *)
  36.121  by (fast_tac (HOL_cs addss simpset()) 1);
  36.122  (* case Fun t1 t2 *)
  36.123 @@ -229,7 +229,7 @@
  36.124  
  36.125  Goal
  36.126    "$ S1 (sch::type_scheme) = $ S2 sch --> n:(free_tv sch) --> S1 n = S2 n";
  36.127 -by (type_scheme.induct_tac "sch" 1);
  36.128 +by (induct_tac "sch" 1);
  36.129  (* case TVar n *)
  36.130  by (Asm_simp_tac 1);
  36.131  (* case BVar n *)
  36.132 @@ -242,7 +242,7 @@
  36.133  
  36.134  Goal
  36.135    "$S1 (A::type_scheme list) = $S2 A --> n:(free_tv A) --> S1 n = S2 n";
  36.136 -by (list.induct_tac "A" 1);
  36.137 +by (induct_tac "A" 1);
  36.138  (* case [] *)
  36.139  by (fast_tac (HOL_cs addss simpset()) 1);
  36.140  (* case x#xl *)
  36.141 @@ -281,7 +281,7 @@
  36.142  qed "free_tv_subst_var";
  36.143  
  36.144  Goal "free_tv ($ S (t::typ)) <= cod S Un free_tv t";
  36.145 -by (typ.induct_tac "t" 1);
  36.146 +by (induct_tac "t" 1);
  36.147  (* case TVar n *)
  36.148  by (simp_tac (simpset() addsimps [free_tv_subst_var]) 1);
  36.149  (* case Fun t1 t2 *)
  36.150 @@ -289,7 +289,7 @@
  36.151  qed "free_tv_app_subst_te";     
  36.152  
  36.153  Goal "free_tv ($ S (sch::type_scheme)) <= cod S Un free_tv sch";
  36.154 -by (type_scheme.induct_tac "sch" 1);
  36.155 +by (induct_tac "sch" 1);
  36.156  (* case FVar n *)
  36.157  by (simp_tac (simpset() addsimps [free_tv_subst_var]) 1);
  36.158  (* case BVar n *)
  36.159 @@ -299,7 +299,7 @@
  36.160  qed "free_tv_app_subst_type_scheme";  
  36.161  
  36.162  Goal "free_tv ($ S (A::type_scheme list)) <= cod S Un free_tv A";
  36.163 -by (list.induct_tac "A" 1);
  36.164 +by (induct_tac "A" 1);
  36.165  (* case [] *)
  36.166  by (Simp_tac 1);
  36.167  (* case a#al *)
  36.168 @@ -322,14 +322,14 @@
  36.169  qed "free_tv_o_subst";
  36.170  
  36.171  Goal "n : free_tv t --> free_tv (S n) <= free_tv ($ S t::typ)";
  36.172 -by (typ.induct_tac "t" 1);
  36.173 +by (induct_tac "t" 1);
  36.174  by (Simp_tac 1);
  36.175  by (Simp_tac 1);
  36.176  by (Fast_tac 1);
  36.177  qed_spec_mp "free_tv_of_substitutions_extend_to_types";
  36.178  
  36.179  Goal "n : free_tv sch --> free_tv (S n) <= free_tv ($ S sch::type_scheme)";
  36.180 -by (type_scheme.induct_tac "sch" 1);
  36.181 +by (induct_tac "sch" 1);
  36.182  by (Simp_tac 1);
  36.183  by (Simp_tac 1);
  36.184  by (Simp_tac 1);
  36.185 @@ -337,7 +337,7 @@
  36.186  qed_spec_mp "free_tv_of_substitutions_extend_to_schemes";
  36.187  
  36.188  Goal "n : free_tv A --> free_tv (S n) <= free_tv ($ S A::type_scheme list)";
  36.189 -by (list.induct_tac "A" 1);
  36.190 +by (induct_tac "A" 1);
  36.191  by (Simp_tac 1);
  36.192  by (Simp_tac 1);
  36.193  by (fast_tac (claset() addDs [free_tv_of_substitutions_extend_to_schemes]) 1);
  36.194 @@ -346,14 +346,14 @@
  36.195  Addsimps [free_tv_of_substitutions_extend_to_scheme_lists];
  36.196  
  36.197  Goal "!!sch::type_scheme. (n : free_tv sch) = (n mem free_tv_ML sch)";
  36.198 -by (type_scheme.induct_tac "sch" 1);
  36.199 +by (induct_tac "sch" 1);
  36.200  by (ALLGOALS Asm_simp_tac);
  36.201  by (strip_tac 1);
  36.202  by (Fast_tac 1);
  36.203  qed "free_tv_ML_scheme";
  36.204  
  36.205  Goal "!!A::type_scheme list. (n : free_tv A) = (n mem free_tv_ML A)";
  36.206 -by (list.induct_tac "A" 1);
  36.207 +by (induct_tac "A" 1);
  36.208  by (Simp_tac 1);
  36.209  by (asm_simp_tac (simpset() addsimps [free_tv_ML_scheme]) 1);
  36.210  qed "free_tv_ML_scheme_list";
  36.211 @@ -362,14 +362,14 @@
  36.212  (* lemmata for bound_tv *)
  36.213  
  36.214  Goal "bound_tv (mk_scheme t) = {}";
  36.215 -by (typ.induct_tac "t" 1);
  36.216 +by (induct_tac "t" 1);
  36.217  by (ALLGOALS Asm_simp_tac);
  36.218  qed "bound_tv_mk_scheme";
  36.219  
  36.220  Addsimps [bound_tv_mk_scheme];
  36.221  
  36.222  Goal "!!sch::type_scheme. bound_tv ($ S sch) = bound_tv sch";
  36.223 -by (type_scheme.induct_tac "sch" 1);
  36.224 +by (induct_tac "sch" 1);
  36.225  by (ALLGOALS Asm_simp_tac);
  36.226  qed "bound_tv_subst_scheme";
  36.227  
  36.228 @@ -410,28 +410,28 @@
  36.229  Goal 
  36.230    "new_tv n  = list_all (new_tv n)";
  36.231  by (rtac ext 1);
  36.232 -by (list.induct_tac "x" 1);
  36.233 +by (induct_tac "x" 1);
  36.234  by (ALLGOALS Asm_simp_tac);
  36.235  qed "new_tv_list";
  36.236  
  36.237  (* substitution affects only variables occurring freely *)
  36.238  Goal
  36.239    "new_tv n (t::typ) --> $(%x. if x=n then t' else S x) t = $S t";
  36.240 -by (typ.induct_tac "t" 1);
  36.241 +by (induct_tac "t" 1);
  36.242  by (ALLGOALS Asm_simp_tac);
  36.243  qed "subst_te_new_tv";
  36.244  Addsimps [subst_te_new_tv];
  36.245  
  36.246  Goal
  36.247    "new_tv n (sch::type_scheme) --> $(%x. if x=n then sch' else S x) sch = $S sch";
  36.248 -by (type_scheme.induct_tac "sch" 1);
  36.249 +by (induct_tac "sch" 1);
  36.250  by (ALLGOALS Asm_simp_tac);
  36.251  qed_spec_mp "subst_te_new_type_scheme";
  36.252  Addsimps [subst_te_new_type_scheme];
  36.253  
  36.254  Goal
  36.255    "new_tv n (A::type_scheme list) --> $(%x. if x=n then t else S x) A = $S A";
  36.256 -by (list.induct_tac "A" 1);
  36.257 +by (induct_tac "A" 1);
  36.258  by (ALLGOALS Asm_full_simp_tac);
  36.259  qed_spec_mp "subst_tel_new_scheme_list";
  36.260  Addsimps [subst_tel_new_scheme_list];
  36.261 @@ -466,13 +466,13 @@
  36.262  
  36.263  Goal
  36.264    "new_tv n S --> new_tv n (t::typ) --> new_tv n ($ S t)";
  36.265 -by (typ.induct_tac "t" 1);
  36.266 +by (induct_tac "t" 1);
  36.267  by (ALLGOALS(fast_tac (HOL_cs addss (simpset() addsimps [new_tv_subst]))));
  36.268  qed_spec_mp "new_tv_subst_te";
  36.269  Addsimps [new_tv_subst_te];
  36.270  
  36.271  Goal "new_tv n S --> new_tv n (sch::type_scheme) --> new_tv n ($ S sch)";
  36.272 -by (type_scheme.induct_tac "sch" 1);
  36.273 +by (induct_tac "sch" 1);
  36.274  by (ALLGOALS (Asm_full_simp_tac));
  36.275  by (rewtac new_tv_def);
  36.276  by (simp_tac (simpset() addsimps [free_tv_subst,dom_def,cod_def]) 1);
  36.277 @@ -487,7 +487,7 @@
  36.278  
  36.279  Goal
  36.280    "new_tv n S --> new_tv n (A::type_scheme list) --> new_tv n ($ S A)";
  36.281 -by (list.induct_tac "A" 1);
  36.282 +by (induct_tac "A" 1);
  36.283  by (ALLGOALS(fast_tac (HOL_cs addss (simpset()))));
  36.284  qed_spec_mp "new_tv_subst_scheme_list";
  36.285  Addsimps [new_tv_subst_scheme_list];
  36.286 @@ -495,7 +495,7 @@
  36.287  Goal
  36.288    "new_tv n A --> new_tv (Suc n) ((TVar n)#A)";
  36.289  by (simp_tac (simpset() addsimps [new_tv_list]) 1);
  36.290 -by (list.induct_tac "A" 1);
  36.291 +by (induct_tac "A" 1);
  36.292  by (ALLGOALS Asm_full_simp_tac);
  36.293  qed "new_tv_Suc_list";
  36.294  
  36.295 @@ -509,7 +509,7 @@
  36.296  
  36.297  Goalw [new_tv_def]
  36.298    "!nat. nat < length A --> new_tv n A --> (new_tv n (A!nat))";
  36.299 -by (list.induct_tac "A" 1);
  36.300 +by (induct_tac "A" 1);
  36.301  by (Asm_full_simp_tac 1);
  36.302  by (rtac allI 1);
  36.303  by (res_inst_tac [("n","nat")] nat_induct 1);
  36.304 @@ -549,7 +549,7 @@
  36.305  val less_maxR = result();
  36.306  
  36.307  Goalw [new_tv_def] "!!t::typ. ? n. (new_tv n t)";
  36.308 -by (typ.induct_tac "t" 1);
  36.309 +by (induct_tac "t" 1);
  36.310  by (res_inst_tac [("x","Suc nat")] exI 1);
  36.311  by (Asm_simp_tac 1);
  36.312  by (REPEAT (etac exE 1));
  36.313 @@ -562,7 +562,7 @@
  36.314  Addsimps [fresh_variable_types];
  36.315  
  36.316  Goalw [new_tv_def] "!!sch::type_scheme. ? n. (new_tv n sch)";
  36.317 -by (type_scheme.induct_tac "sch" 1);
  36.318 +by (induct_tac "sch" 1);
  36.319  by (res_inst_tac [("x","Suc nat")] exI 1);
  36.320  by (Simp_tac 1);
  36.321  by (res_inst_tac [("x","Suc nat")] exI 1);
  36.322 @@ -586,7 +586,7 @@
  36.323  val le_maxR = result();
  36.324  
  36.325  Goal "!!A::type_scheme list. ? n. (new_tv n A)";
  36.326 -by (list.induct_tac "A" 1);
  36.327 +by (induct_tac "A" 1);
  36.328  by (Simp_tac 1);
  36.329  by (Simp_tac 1);
  36.330  by (etac exE 1);
  36.331 @@ -648,7 +648,7 @@
  36.332  Addsimps [length_app_subst_list];
  36.333  
  36.334  Goal "!!sch::type_scheme. $ TVar sch = sch";
  36.335 -by (type_scheme.induct_tac "sch" 1);
  36.336 +by (induct_tac "sch" 1);
  36.337  by (ALLGOALS Asm_simp_tac);
  36.338  qed "subst_TVar_scheme";
  36.339  
  36.340 @@ -665,7 +665,7 @@
  36.341  Goalw [id_subst_def]
  36.342    "$ id_subst = (%t::typ. t)";
  36.343  by (rtac ext 1);
  36.344 -by (typ.induct_tac "t" 1);
  36.345 +by (induct_tac "t" 1);
  36.346  by (ALLGOALS Asm_simp_tac);
  36.347  qed "app_subst_id_te";
  36.348  Addsimps [app_subst_id_te];
  36.349 @@ -673,7 +673,7 @@
  36.350  Goalw [id_subst_def]
  36.351    "$ id_subst = (%sch::type_scheme. sch)";
  36.352  by (rtac ext 1);
  36.353 -by (type_scheme.induct_tac "t" 1);
  36.354 +by (induct_tac "sch" 1);
  36.355  by (ALLGOALS Asm_simp_tac);
  36.356  qed "app_subst_id_type_scheme";
  36.357  Addsimps [app_subst_id_type_scheme];
  36.358 @@ -682,20 +682,20 @@
  36.359  Goalw [app_subst_list]
  36.360    "$ id_subst = (%A::type_scheme list. A)";
  36.361  by (rtac ext 1); 
  36.362 -by (list.induct_tac "A" 1);
  36.363 +by (induct_tac "A" 1);
  36.364  by (ALLGOALS Asm_simp_tac);
  36.365  qed "app_subst_id_tel";
  36.366  Addsimps [app_subst_id_tel];
  36.367  
  36.368  Goal "!!sch::type_scheme. $ id_subst sch = sch";
  36.369 -by (type_scheme.induct_tac "sch" 1);
  36.370 +by (induct_tac "sch" 1);
  36.371  by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [id_subst_def])));
  36.372  qed "id_subst_sch";
  36.373  
  36.374  Addsimps [id_subst_sch];
  36.375  
  36.376  Goal "!!A::type_scheme list. $ id_subst A = A";
  36.377 -by (list.induct_tac "A" 1);
  36.378 +by (induct_tac "A" 1);
  36.379  by (Asm_full_simp_tac 1);
  36.380  by (Asm_full_simp_tac 1);
  36.381  qed "id_subst_A";
  36.382 @@ -710,18 +710,18 @@
  36.383  Addsimps[o_id_subst];
  36.384  
  36.385  Goal "$ R ($ S t::typ) = $ (%x. $ R (S x) ) t";
  36.386 -by (typ.induct_tac "t" 1);
  36.387 +by (induct_tac "t" 1);
  36.388  by (ALLGOALS Asm_simp_tac);
  36.389  qed "subst_comp_te";
  36.390  
  36.391  Goal "$ R ($ S sch::type_scheme) = $ (%x. $ R (S x) ) sch";
  36.392 -by (type_scheme.induct_tac "sch" 1);
  36.393 +by (induct_tac "sch" 1);
  36.394  by (ALLGOALS Asm_full_simp_tac);
  36.395  qed "subst_comp_type_scheme";
  36.396  
  36.397  Goalw [app_subst_list]
  36.398    "$ R ($ S A::type_scheme list) = $ (%x. $ R (S x)) A";
  36.399 -by (list.induct_tac "A" 1);
  36.400 +by (induct_tac "A" 1);
  36.401  (* case [] *)
  36.402  by (Simp_tac 1);
  36.403  (* case x#xl *)
  36.404 @@ -740,7 +740,7 @@
  36.405  qed "subst_id_on_type_scheme_list";
  36.406  
  36.407  Goal "!n. n < length A --> ($ S A)!n = $S (A!n)";
  36.408 -by (list.induct_tac "A" 1);
  36.409 +by (induct_tac "A" 1);
  36.410  by (Asm_full_simp_tac 1);
  36.411  by (rtac allI 1);
  36.412  by (rename_tac "n1" 1);
    37.1 --- a/src/HOL/MiniML/Type.thy	Fri Jul 24 13:03:20 1998 +0200
    37.2 +++ b/src/HOL/MiniML/Type.thy	Fri Jul 24 13:19:38 1998 +0200
    37.3 @@ -25,7 +25,7 @@
    37.4  consts
    37.5    mk_scheme :: typ => type_scheme
    37.6  
    37.7 -primrec mk_scheme typ
    37.8 +primrec
    37.9    "mk_scheme (TVar n) = (FVar n)"
   37.10    "mk_scheme (t1 -> t2) = ((mk_scheme t1) =-> (mk_scheme t2))"
   37.11  
   37.12 @@ -41,16 +41,16 @@
   37.13  consts
   37.14    free_tv :: ['a::type_struct] => nat set
   37.15  
   37.16 -primrec free_tv typ
   37.17 +primrec
   37.18    free_tv_TVar    "free_tv (TVar m) = {m}"
   37.19    free_tv_Fun     "free_tv (t1 -> t2) = (free_tv t1) Un (free_tv t2)"
   37.20  
   37.21 -primrec free_tv type_scheme
   37.22 +primrec
   37.23    "free_tv (FVar m) = {m}"
   37.24    "free_tv (BVar m) = {}"
   37.25    "free_tv (S1 =-> S2) = (free_tv S1) Un (free_tv S2)"
   37.26  
   37.27 -primrec free_tv list
   37.28 +primrec
   37.29    "free_tv [] = {}"
   37.30    "free_tv (x#l) = (free_tv x) Un (free_tv l)"
   37.31  
   37.32 @@ -59,12 +59,12 @@
   37.33  consts
   37.34    free_tv_ML :: ['a::type_struct] => nat list
   37.35  
   37.36 -primrec free_tv_ML type_scheme
   37.37 +primrec
   37.38    "free_tv_ML (FVar m) = [m]"
   37.39    "free_tv_ML (BVar m) = []"
   37.40    "free_tv_ML (S1 =-> S2) = (free_tv_ML S1) @ (free_tv_ML S2)"
   37.41  
   37.42 -primrec free_tv_ML list
   37.43 +primrec
   37.44    "free_tv_ML [] = []"
   37.45    "free_tv_ML (x#l) = (free_tv_ML x) @ (free_tv_ML l)"
   37.46  
   37.47 @@ -82,12 +82,12 @@
   37.48  consts
   37.49    bound_tv :: ['a::type_struct] => nat set
   37.50  
   37.51 -primrec bound_tv type_scheme
   37.52 +primrec
   37.53    "bound_tv (FVar m) = {}"
   37.54    "bound_tv (BVar m) = {m}"
   37.55    "bound_tv (S1 =-> S2) = (bound_tv S1) Un (bound_tv S2)"
   37.56  
   37.57 -primrec bound_tv list
   37.58 +primrec
   37.59    "bound_tv [] = {}"
   37.60    "bound_tv (x#l) = (bound_tv x) Un (bound_tv l)"
   37.61  
   37.62 @@ -97,7 +97,7 @@
   37.63  consts
   37.64    min_new_bound_tv :: 'a::type_struct => nat
   37.65  
   37.66 -primrec min_new_bound_tv type_scheme
   37.67 +primrec
   37.68    "min_new_bound_tv (FVar n) = 0"
   37.69    "min_new_bound_tv (BVar n) = Suc n"
   37.70    "min_new_bound_tv (sch1 =-> sch2) = max (min_new_bound_tv sch1) (min_new_bound_tv sch2)"
   37.71 @@ -118,11 +118,11 @@
   37.72  consts
   37.73    app_subst :: [subst, 'a::type_struct] => 'a::type_struct ("$")
   37.74  
   37.75 -primrec app_subst typ 
   37.76 +primrec
   37.77    app_subst_TVar "$ S (TVar n) = S n" 
   37.78    app_subst_Fun  "$ S (t1 -> t2) = ($ S t1) -> ($ S t2)" 
   37.79  
   37.80 -primrec app_subst type_scheme
   37.81 +primrec
   37.82    "$ S (FVar n) = mk_scheme (S n)"
   37.83    "$ S (BVar n) = (BVar n)"
   37.84    "$ S (sch1 =-> sch2) = ($ S sch1) =-> ($ S sch2)"
    38.1 --- a/src/HOL/MiniML/W.ML	Fri Jul 24 13:03:20 1998 +0200
    38.2 +++ b/src/HOL/MiniML/W.ML	Fri Jul 24 13:19:38 1998 +0200
    38.3 @@ -16,7 +16,7 @@
    38.4  (* the resulting type variable is always greater or equal than the given one *)
    38.5  Goal
    38.6          "!A n S t m. W e A n  = Some (S,t,m) --> n<=m";
    38.7 -by (expr.induct_tac "e" 1);
    38.8 +by (induct_tac "e" 1);
    38.9  (* case Var(n) *)
   38.10  by (simp_tac (simpset() addsplits [split_option_bind]) 1);
   38.11  (* case Abs e *)
   38.12 @@ -45,7 +45,7 @@
   38.13  qed "new_tv_compatible_W";
   38.14  
   38.15  Goal "new_tv n sch --> new_tv (n + (min_new_bound_tv sch)) (bound_typ_inst (%b. TVar (b + n)) sch)";
   38.16 -by (type_scheme.induct_tac "sch" 1);
   38.17 +by (induct_tac "sch" 1);
   38.18    by (Asm_full_simp_tac 1);
   38.19   by (asm_full_simp_tac (simpset() addsimps [add_commute]) 1);
   38.20  by (strip_tac 1);
   38.21 @@ -74,7 +74,7 @@
   38.22  Goal
   38.23       "!n A S t m. new_tv n A --> W e A n = Some (S,t,m) -->    \
   38.24  \                 new_tv m S & new_tv m t";
   38.25 -by (expr.induct_tac "e" 1);
   38.26 +by (induct_tac "e" 1);
   38.27  (* case Var n *)
   38.28  by (simp_tac (simpset() addsplits [split_option_bind]) 1);
   38.29  by (strip_tac 1);
   38.30 @@ -156,7 +156,7 @@
   38.31  qed_spec_mp "new_tv_W";
   38.32  
   38.33  Goal "(v ~: free_tv sch) --> (v : free_tv (bound_typ_inst (TVar o S) sch)) --> (? x. v = S x)";
   38.34 -by (type_scheme.induct_tac "sch" 1);
   38.35 +by (induct_tac "sch" 1);
   38.36  by (Asm_full_simp_tac 1);
   38.37  by (Asm_full_simp_tac 1);
   38.38  by (strip_tac 1);
   38.39 @@ -170,7 +170,7 @@
   38.40  Goal
   38.41       "!n A S t m v. W e A n = Some (S,t,m) -->            \
   38.42  \         (v:free_tv S | v:free_tv t) --> v<n --> v:free_tv A";
   38.43 -by (expr.induct_tac "e" 1);
   38.44 +by (induct_tac "e" 1);
   38.45  (* case Var n *)
   38.46  by (simp_tac (simpset() addsimps
   38.47      [free_tv_subst] addsplits [split_option_bind]) 1);
   38.48 @@ -265,7 +265,7 @@
   38.49  (* correctness of W with respect to has_type *)
   38.50  Goal
   38.51          "!A S t m n . new_tv n A --> Some (S,t,m) = W e A n --> $S A |- e :: t";
   38.52 -by (expr.induct_tac "e" 1);
   38.53 +by (induct_tac "e" 1);
   38.54  (* case Var n *)
   38.55  by (Asm_full_simp_tac 1);
   38.56  by (strip_tac 1);
   38.57 @@ -388,7 +388,7 @@
   38.58   "!S' A t' n. $S' A |- e :: t' --> new_tv n A -->     \
   38.59  \             (? S t. (? m. W e A n = Some (S,t,m)) &  \
   38.60  \                     (? R. $S' A = $R ($S A) & t' = $R t))";
   38.61 -by (expr.induct_tac "e" 1);
   38.62 +by (induct_tac "e" 1);
   38.63  (* case Var n *)
   38.64  by (strip_tac 1);
   38.65  by (simp_tac (simpset() addcongs [conj_cong]) 1);
    39.1 --- a/src/HOL/MiniML/W.thy	Fri Jul 24 13:03:20 1998 +0200
    39.2 +++ b/src/HOL/MiniML/W.thy	Fri Jul 24 13:19:38 1998 +0200
    39.3 @@ -17,7 +17,7 @@
    39.4  consts
    39.5          W :: [expr, ctxt, nat] => result_W
    39.6  
    39.7 -primrec W expr
    39.8 +primrec
    39.9    "W (Var i) A n =  
   39.10       (if i < length A then Some( id_subst,   
   39.11  	                         bound_typ_inst (%b. TVar(b+n)) (A!i),   
    40.1 --- a/src/HOL/Quot/NPAIR.thy	Fri Jul 24 13:03:20 1998 +0200
    40.2 +++ b/src/HOL/Quot/NPAIR.thy	Fri Jul 24 13:19:38 1998 +0200
    40.3 @@ -6,11 +6,9 @@
    40.4  Example: define a PER on pairs of natural numbers (with embedding)
    40.5  
    40.6  *)
    40.7 -NPAIR = PER + Arith + (* representation for rational numbers *)
    40.8 +NPAIR = PER + Datatype + (* representation for rational numbers *)
    40.9  
   40.10 -types np = "(nat * nat)" (* is needed for datatype *)
   40.11 -
   40.12 -datatype NP = abs_NP np
   40.13 +datatype NP = abs_NP "(nat * nat)"
   40.14  
   40.15  consts	rep_NP :: "NP => nat * nat"
   40.16  
   40.17 @@ -23,4 +21,4 @@
   40.18  (* for proves of this rule see [Slo97diss] *)
   40.19  rules
   40.20  	per_trans_NP	"[| eqv (x::NP) y;eqv y z |] ==> eqv x z"
   40.21 -end
   40.22 \ No newline at end of file
   40.23 +end
    41.1 --- a/src/HOL/Real/PNat.ML	Fri Jul 24 13:03:20 1998 +0200
    41.2 +++ b/src/HOL/Real/PNat.ML	Fri Jul 24 13:19:38 1998 +0200
    41.3 @@ -48,11 +48,8 @@
    41.4  qed "pnat_induct";
    41.5  
    41.6  (*Perform induction on n. *)
    41.7 -local fun raw_pnat_ind_tac a i = 
    41.8 -    res_inst_tac [("n",a)] pnat_induct i  THEN  rename_last_tac a [""] (i+1)
    41.9 -in
   41.10 -val pnat_ind_tac = Datatype.occs_in_prems raw_pnat_ind_tac
   41.11 -end;
   41.12 +fun pnat_ind_tac a i = 
   41.13 +  res_inst_tac [("n",a)] pnat_induct i  THEN  rename_last_tac a [""] (i+1);
   41.14  
   41.15  val prems = goal thy
   41.16      "[| !!x. P x 1p;  \
    42.1 --- a/src/HOL/Real/Real.ML	Fri Jul 24 13:03:20 1998 +0200
    42.2 +++ b/src/HOL/Real/Real.ML	Fri Jul 24 13:19:38 1998 +0200
    42.3 @@ -1267,7 +1267,7 @@
    42.4  
    42.5  Goal "1r <= %%#n";
    42.6  by (simp_tac (simpset() addsimps [real_nat_one RS sym]) 1);
    42.7 -by (nat_ind_tac "n" 1);
    42.8 +by (induct_tac "n" 1);
    42.9  by (auto_tac (claset(),simpset () 
   42.10      addsimps [real_nat_Suc,real_le_refl,real_nat_one]));
   42.11  by (res_inst_tac [("t","1r")] (real_add_zero_left RS subst) 1);
    43.1 --- a/src/HOL/Subst/Subst.thy	Fri Jul 24 13:03:20 1998 +0200
    43.2 +++ b/src/HOL/Subst/Subst.thy	Fri Jul 24 13:19:38 1998 +0200
    43.3 @@ -18,7 +18,7 @@
    43.4    srange ::  "('a*('a uterm)) list => 'a set"
    43.5  
    43.6  
    43.7 -primrec "op <|"   uterm
    43.8 +primrec
    43.9    subst_Var      "(Var v <| s) = assoc v (Var v) s"
   43.10    subst_Const  "(Const c <| s) = Const c"
   43.11    subst_Comb  "(Comb M N <| s) = Comb (M <| s) (N <| s)"
    44.1 --- a/src/HOL/Subst/UTerm.thy	Fri Jul 24 13:03:20 1998 +0200
    44.2 +++ b/src/HOL/Subst/UTerm.thy	Fri Jul 24 13:19:38 1998 +0200
    44.3 @@ -7,7 +7,7 @@
    44.4  Binary trees with leaves that are constants or variables.
    44.5  *)
    44.6  
    44.7 -UTerm = Finite + 
    44.8 +UTerm = Finite + Datatype +
    44.9  
   44.10  datatype 'a uterm = Var ('a) 
   44.11                    | Const ('a)
   44.12 @@ -19,20 +19,20 @@
   44.13  uterm_size ::  'a uterm => nat
   44.14  
   44.15  
   44.16 -primrec vars_of   uterm
   44.17 -vars_of_Var   "vars_of (Var v) = {v}"
   44.18 -vars_of_Const "vars_of (Const c) = {}"
   44.19 -vars_of_Comb  "vars_of (Comb M N) = (vars_of(M) Un vars_of(N))"
   44.20 +primrec
   44.21 +  vars_of_Var   "vars_of (Var v) = {v}"
   44.22 +  vars_of_Const "vars_of (Const c) = {}"
   44.23 +  vars_of_Comb  "vars_of (Comb M N) = (vars_of(M) Un vars_of(N))"
   44.24  
   44.25  
   44.26 -primrec "op <:"   uterm
   44.27 -occs_Var   "u <: (Var v) = False"
   44.28 -occs_Const "u <: (Const c) = False"
   44.29 -occs_Comb  "u <: (Comb M N) = (u=M | u=N | u <: M | u <: N)"
   44.30 +primrec
   44.31 +  occs_Var   "u <: (Var v) = False"
   44.32 +  occs_Const "u <: (Const c) = False"
   44.33 +  occs_Comb  "u <: (Comb M N) = (u=M | u=N | u <: M | u <: N)"
   44.34  
   44.35 -primrec uterm_size  uterm
   44.36 -uterm_size_Var   "uterm_size (Var v) = 0"
   44.37 -uterm_size_Const "uterm_size (Const c) = 0"
   44.38 -uterm_size_Comb  "uterm_size (Comb M N) = Suc(uterm_size M + uterm_size N)"
   44.39 +primrec
   44.40 +  uterm_size_Var   "uterm_size (Var v) = 0"
   44.41 +  uterm_size_Const "uterm_size (Const c) = 0"
   44.42 +  uterm_size_Comb  "uterm_size (Comb M N) = Suc(uterm_size M + uterm_size N)"
   44.43  
   44.44  end
    45.1 --- a/src/HOL/Subst/Unify.ML	Fri Jul 24 13:03:20 1998 +0200
    45.2 +++ b/src/HOL/Subst/Unify.ML	Fri Jul 24 13:19:38 1998 +0200
    45.3 @@ -160,7 +160,7 @@
    45.4  			inv_image_def, less_eq]) 1);
    45.5  (** LEVEL 7 **)
    45.6  (*Comb-Comb case*)
    45.7 -by (asm_simp_tac (simpset() addsplits [split_option_case]) 1);
    45.8 +by (asm_simp_tac (simpset() addsplits [option.split]) 1);
    45.9  by (strip_tac 1);
   45.10  by (rtac (trans_unifyRel RS transD) 1);
   45.11  by (Blast_tac 1);
   45.12 @@ -183,7 +183,7 @@
   45.13  \                            of None => None    \
   45.14  \                             | Some sigma => Some (theta <> sigma)))";
   45.15  by (asm_simp_tac (simpset() addsimps (unify_TC::unifyRules0)
   45.16 -			   addsplits [split_option_case]) 1);
   45.17 +			   addsplits [option.split]) 1);
   45.18  qed "unifyCombComb";
   45.19  
   45.20  
   45.21 @@ -219,7 +219,7 @@
   45.22  by (simp_tac (simpset() addsimps [MGUnifier_Var]) 1);
   45.23  (** LEVEL 8 **)
   45.24  (*Comb-Comb case*)
   45.25 -by (asm_simp_tac (simpset() addsplits [split_option_case]) 1);
   45.26 +by (asm_simp_tac (simpset() addsplits [option.split]) 1);
   45.27  by (strip_tac 1);
   45.28  by (rotate_tac ~2 1);
   45.29  by (asm_full_simp_tac 
   45.30 @@ -244,7 +244,7 @@
   45.31  by (res_inst_tac [("u","M"),("v","N")] unifyInduct 1);
   45.32  by (ALLGOALS 
   45.33      (asm_simp_tac 
   45.34 -       (simpset() addsimps [Var_Idem] addsplits [split_option_case])));
   45.35 +       (simpset() addsimps [Var_Idem] addsplits [option.split])));
   45.36  (*Comb-Comb case*)
   45.37  by Safe_tac;
   45.38  by (REPEAT (dtac spec 1 THEN mp_tac 1));
    46.1 --- a/src/HOL/TLA/Inc/Pcount.thy	Fri Jul 24 13:03:20 1998 +0200
    46.2 +++ b/src/HOL/TLA/Inc/Pcount.thy	Fri Jul 24 13:19:38 1998 +0200
    46.3 @@ -11,7 +11,7 @@
    46.4  and case distinction tactics.
    46.5  *)
    46.6  
    46.7 -Pcount  =  HOL + Arith +
    46.8 +Pcount  =  Datatype +
    46.9  
   46.10  datatype pcount = a | b | g
   46.11  
    47.1 --- a/src/HOL/TLA/Memory/MIParameters.thy	Fri Jul 24 13:03:20 1998 +0200
    47.2 +++ b/src/HOL/TLA/Memory/MIParameters.thy	Fri Jul 24 13:19:38 1998 +0200
    47.3 @@ -9,7 +9,7 @@
    47.4      RPC-Memory example: Parameters of the memory implementation.
    47.5  *)
    47.6  
    47.7 -MIParameters = Arith +
    47.8 +MIParameters = Datatype +
    47.9  
   47.10  datatype  histState  =  histA | histB
   47.11  
    48.1 --- a/src/HOL/TLA/Memory/Memory.ML	Fri Jul 24 13:03:20 1998 +0200
    48.2 +++ b/src/HOL/TLA/Memory/Memory.ML	Fri Jul 24 13:19:38 1998 +0200
    48.3 @@ -148,13 +148,13 @@
    48.4  	     res_inst_tac [("s","arg(ch s p)")] sumE 1,
    48.5  	      action_simp_tac (simpset()addsimps[Read_def,enabled_ex,base_pair])
    48.6  	                      [action_mp ReadInner_enabled,exI] [] 1,
    48.7 -	      split_all_tac 1, rename_tac "a b" 1, Rd.induct_tac "a" 1,
    48.8 +	      split_all_tac 1, rename_tac "a b" 1, induct_tac "a" 1,
    48.9  	     (* introduce a trivial subgoal to solve flex-flex constraint?! *)
   48.10  	      subgoal_tac "b = snd(a,b)" 1,
   48.11  	       TRYALL Simp_tac,  (* solves "read" case *)
   48.12  	     etac swap 1,
   48.13  	     action_simp_tac (simpset()addsimps[Write_def,enabled_ex,base_pair])
   48.14  	                     [action_mp WriteInner_enabled,exI] [] 1,
   48.15 -	     split_all_tac 1, rename_tac "a aa b" 1, Wr.induct_tac "a" 1,
   48.16 +	     split_all_tac 1, rename_tac "a aa b" 1, induct_tac "a" 1,
   48.17  	     subgoal_tac "(aa = fst(snd(a,aa,b))) & (b = snd(snd(a,aa,b)))" 1,
   48.18  	     ALLGOALS Simp_tac ]);
    49.1 --- a/src/HOL/TLA/Memory/MemoryParameters.thy	Fri Jul 24 13:03:20 1998 +0200
    49.2 +++ b/src/HOL/TLA/Memory/MemoryParameters.thy	Fri Jul 24 13:19:38 1998 +0200
    49.3 @@ -9,7 +9,7 @@
    49.4      RPC-Memory example: Memory parameters
    49.5  *)
    49.6  
    49.7 -MemoryParameters = Prod + Sum + Arith + RPCMemoryParams +
    49.8 +MemoryParameters = Datatype + RPCMemoryParams +
    49.9  
   49.10  (* the memory operations. nb: data types must be defined in theories
   49.11     that do not include Intensional -- otherwise the induction rule
    50.1 --- a/src/HOL/W0/I.ML	Fri Jul 24 13:03:20 1998 +0200
    50.2 +++ b/src/HOL/W0/I.ML	Fri Jul 24 13:19:38 1998 +0200
    50.3 @@ -12,7 +12,7 @@
    50.4    "! a m s s' t n.  \
    50.5  \    (new_tv m a & new_tv m s) --> I e a m s = Ok(s',t,n) -->   \
    50.6  \    ( ? r. W e ($ s a) m = Ok(r, $ s' t, n) & s' = ($ r o s) )";
    50.7 -by (expr.induct_tac "e" 1);
    50.8 +by (induct_tac "e" 1);
    50.9  
   50.10    (* case Var n *)
   50.11    by (simp_tac (simpset() addsimps [app_subst_list]
   50.12 @@ -143,7 +143,7 @@
   50.13  
   50.14  Goal "!a m s. \
   50.15  \  new_tv m a & new_tv m s --> I e a m s = Fail --> W e ($s a) m = Fail";
   50.16 -by (expr.induct_tac "e" 1);
   50.17 +by (induct_tac "e" 1);
   50.18    by (simp_tac (simpset() addsimps [app_subst_list]) 1);
   50.19   by (Simp_tac 1);
   50.20   by (strip_tac 1);
    51.1 --- a/src/HOL/W0/I.thy	Fri Jul 24 13:03:20 1998 +0200
    51.2 +++ b/src/HOL/W0/I.thy	Fri Jul 24 13:19:38 1998 +0200
    51.3 @@ -11,7 +11,7 @@
    51.4  consts
    51.5          I :: [expr, typ list, nat, subst] => result_W
    51.6  
    51.7 -primrec I expr
    51.8 +primrec
    51.9          "I (Var i) a n s = (if i < length a then Ok(s, a!i, n)
   51.10                                      else Fail)"
   51.11          "I (Abs e) a n s = ( (s,t,m) := I e ((TVar n)#a) (Suc n) s;
    52.1 --- a/src/HOL/W0/Type.ML	Fri Jul 24 13:03:20 1998 +0200
    52.2 +++ b/src/HOL/W0/Type.ML	Fri Jul 24 13:19:38 1998 +0200
    52.3 @@ -17,7 +17,7 @@
    52.4  Goalw [id_subst_def]
    52.5    "$ id_subst = (%t::typ. t)";
    52.6  by (rtac ext 1);
    52.7 -by (typ.induct_tac "t" 1);
    52.8 +by (induct_tac "t" 1);
    52.9  by (ALLGOALS Asm_simp_tac);
   52.10  qed "app_subst_id_te";
   52.11  Addsimps [app_subst_id_te];
   52.12 @@ -26,7 +26,7 @@
   52.13  Goalw [app_subst_list]
   52.14    "$ id_subst = (%ts::typ list. ts)";
   52.15  by (rtac ext 1); 
   52.16 -by (list.induct_tac "ts" 1);
   52.17 +by (induct_tac "ts" 1);
   52.18  by (ALLGOALS Asm_simp_tac);
   52.19  qed "app_subst_id_tel";
   52.20  Addsimps [app_subst_id_tel];
   52.21 @@ -69,13 +69,13 @@
   52.22  (* composition of substitutions *)
   52.23  Goal
   52.24    "$ g ($ f t::typ) = $ (%x. $ g (f x) ) t";
   52.25 -by (typ.induct_tac "t" 1);
   52.26 +by (induct_tac "t" 1);
   52.27  by (ALLGOALS Asm_simp_tac);
   52.28  qed "subst_comp_te";
   52.29  
   52.30  Goalw [app_subst_list]
   52.31    "$ g ($ f ts::typ list) = $ (%x. $ g (f x)) ts";
   52.32 -by (list.induct_tac "ts" 1);
   52.33 +by (induct_tac "ts" 1);
   52.34  (* case [] *)
   52.35  by (Simp_tac 1);
   52.36  (* case x#xl *)
   52.37 @@ -149,21 +149,21 @@
   52.38  Goal 
   52.39    "new_tv n  = list_all (new_tv n)";
   52.40  by (rtac ext 1);
   52.41 -by (list.induct_tac "x" 1);
   52.42 +by (induct_tac "x" 1);
   52.43  by (ALLGOALS Asm_simp_tac);
   52.44  qed "new_tv_list";
   52.45  
   52.46  (* substitution affects only variables occurring freely *)
   52.47  Goal
   52.48    "new_tv n (t::typ) --> $(%x. if x=n then t' else s x) t = $s t";
   52.49 -by (typ.induct_tac "t" 1);
   52.50 +by (induct_tac "t" 1);
   52.51  by (ALLGOALS Asm_simp_tac);
   52.52  qed "subst_te_new_tv";
   52.53  Addsimps [subst_te_new_tv];
   52.54  
   52.55  Goal
   52.56    "new_tv n (ts::typ list) --> $(%x. if x=n then t else s x) ts = $s ts";
   52.57 -by (list.induct_tac "ts" 1);
   52.58 +by (induct_tac "ts" 1);
   52.59  by (ALLGOALS Asm_full_simp_tac);
   52.60  qed "subst_tel_new_tv";
   52.61  Addsimps [subst_tel_new_tv];
   52.62 @@ -171,7 +171,7 @@
   52.63  (* all greater variables are also new *)
   52.64  Goal
   52.65    "n<=m --> new_tv n (t::typ) --> new_tv m t";
   52.66 -by (typ.induct_tac "t" 1);
   52.67 +by (induct_tac "t" 1);
   52.68  (* case TVar n *)
   52.69  by (fast_tac (HOL_cs addIs [less_le_trans] addss simpset()) 1);
   52.70  (* case Fun t1 t2 *)
   52.71 @@ -181,7 +181,7 @@
   52.72  
   52.73  Goal 
   52.74    "n<=m --> new_tv n (ts::typ list) --> new_tv m ts";
   52.75 -by (list.induct_tac "ts" 1);
   52.76 +by (induct_tac "ts" 1);
   52.77  (* case [] *)
   52.78  by (Simp_tac 1);
   52.79  (* case a#al *)
   52.80 @@ -209,7 +209,7 @@
   52.81  
   52.82  Goal
   52.83    "new_tv n s --> new_tv n (t::typ) --> new_tv n ($ s t)";
   52.84 -by (typ.induct_tac "t" 1);
   52.85 +by (induct_tac "t" 1);
   52.86  by (ALLGOALS(fast_tac (HOL_cs addss (simpset() addsimps [new_tv_subst]))));
   52.87  qed_spec_mp "new_tv_subst_te";
   52.88  Addsimps [new_tv_subst_te];
   52.89 @@ -217,7 +217,7 @@
   52.90  Goal
   52.91    "new_tv n s --> new_tv n (ts::typ list) --> new_tv n ($ s ts)";
   52.92  by (simp_tac (simpset() addsimps [new_tv_list]) 1);
   52.93 -by (list.induct_tac "ts" 1);
   52.94 +by (induct_tac "ts" 1);
   52.95  by (ALLGOALS(fast_tac (HOL_cs addss (simpset() addsimps [new_tv_subst]))));
   52.96  qed_spec_mp "new_tv_subst_tel";
   52.97  Addsimps [new_tv_subst_tel];
   52.98 @@ -226,7 +226,7 @@
   52.99  Goal
  52.100    "new_tv n ts --> new_tv (Suc n) ((TVar n)#ts)";
  52.101  by (simp_tac (simpset() addsimps [new_tv_list]) 1);
  52.102 -by (list.induct_tac "ts" 1);
  52.103 +by (induct_tac "ts" 1);
  52.104  by (ALLGOALS Asm_full_simp_tac);
  52.105  qed "new_tv_Suc_list";
  52.106  
  52.107 @@ -255,7 +255,7 @@
  52.108  
  52.109  Goal
  52.110    "(t::typ) mem ts --> free_tv t <= free_tv ts";
  52.111 -by (list.induct_tac "ts" 1);
  52.112 +by (induct_tac "ts" 1);
  52.113  (* case [] *)
  52.114  by (Simp_tac 1);
  52.115  (* case x#xl *)
  52.116 @@ -269,7 +269,7 @@
  52.117     occurring in the type structure *)
  52.118  Goal
  52.119    "$ s1 (t::typ) = $ s2 t --> n:(free_tv t) --> s1 n = s2 n";
  52.120 -by (typ.induct_tac "t" 1);
  52.121 +by (induct_tac "t" 1);
  52.122  (* case TVar n *)
  52.123  by (fast_tac (HOL_cs addss simpset()) 1);
  52.124  (* case Fun t1 t2 *)
  52.125 @@ -278,7 +278,7 @@
  52.126  
  52.127  Goal
  52.128    "(!n. n:(free_tv t) --> s1 n = s2 n) --> $ s1 (t::typ) = $ s2 t";
  52.129 -by (typ.induct_tac "t" 1);
  52.130 +by (induct_tac "t" 1);
  52.131  (* case TVar n *)
  52.132  by (fast_tac (HOL_cs addss simpset()) 1);
  52.133  (* case Fun t1 t2 *)
  52.134 @@ -286,7 +286,7 @@
  52.135  qed_spec_mp "eq_free_eq_subst_te";
  52.136  
  52.137  Goal "$s1 (ts::typ list) = $s2 ts --> n:(free_tv ts) --> s1 n = s2 n";
  52.138 -by (list.induct_tac "ts" 1);
  52.139 +by (induct_tac "ts" 1);
  52.140  (* case [] *)
  52.141  by (fast_tac (HOL_cs addss simpset()) 1);
  52.142  (* case x#xl *)
  52.143 @@ -294,7 +294,7 @@
  52.144  qed_spec_mp "eq_subst_tel_eq_free";
  52.145  
  52.146  Goal "(!n. n:(free_tv ts) --> s1 n = s2 n) --> $s1 (ts::typ list) = $s2 ts";
  52.147 -by (list.induct_tac "ts" 1); 
  52.148 +by (induct_tac "ts" 1); 
  52.149  (* case [] *)
  52.150  by (fast_tac (HOL_cs addss simpset()) 1);
  52.151  (* case x#xl *)
  52.152 @@ -323,7 +323,7 @@
  52.153  qed "free_tv_subst_var";
  52.154  
  52.155  Goal "free_tv ($ s (t::typ)) <= cod s Un free_tv t";
  52.156 -by (typ.induct_tac "t" 1);
  52.157 +by (induct_tac "t" 1);
  52.158  (* case TVar n *)
  52.159  by (simp_tac (simpset() addsimps [free_tv_subst_var]) 1);
  52.160  (* case Fun t1 t2 *)
  52.161 @@ -331,7 +331,7 @@
  52.162  qed "free_tv_app_subst_te";     
  52.163  
  52.164  Goal "free_tv ($ s (ts::typ list)) <= cod s Un free_tv ts";
  52.165 -by (list.induct_tac "ts" 1);
  52.166 +by (induct_tac "ts" 1);
  52.167  (* case [] *)
  52.168  by (Simp_tac 1);
  52.169  (* case a#al *)
    53.1 --- a/src/HOL/W0/Type.thy	Fri Jul 24 13:03:20 1998 +0200
    53.2 +++ b/src/HOL/W0/Type.thy	Fri Jul 24 13:19:38 1998 +0200
    53.3 @@ -36,7 +36,7 @@
    53.4  consts
    53.5          app_subst :: [subst, 'a::type_struct] => 'a::type_struct ("$")
    53.6  
    53.7 -primrec app_subst typ
    53.8 +primrec
    53.9    app_subst_TVar  "$ s (TVar n) = s n" 
   53.10    app_subst_Fun   "$ s (t1 -> t2) = ($ s t1) -> ($ s t2)" 
   53.11  
   53.12 @@ -47,11 +47,11 @@
   53.13  consts
   53.14          free_tv :: ['a::type_struct] => nat set
   53.15  
   53.16 -primrec free_tv typ
   53.17 +primrec
   53.18    "free_tv (TVar m) = {m}"
   53.19    "free_tv (t1 -> t2) = (free_tv t1) Un (free_tv t2)"
   53.20  
   53.21 -primrec free_tv List.list
   53.22 +primrec
   53.23    "free_tv [] = {}"
   53.24    "free_tv (x#l) = (free_tv x) Un (free_tv l)"
   53.25  
    54.1 --- a/src/HOL/W0/W.ML	Fri Jul 24 13:03:20 1998 +0200
    54.2 +++ b/src/HOL/W0/W.ML	Fri Jul 24 13:19:38 1998 +0200
    54.3 @@ -11,7 +11,7 @@
    54.4  
    54.5  (* correctness of W with respect to has_type *)
    54.6  Goal "!a s t m n . Ok (s,t,m) = W e a n --> $s a |- e :: t";
    54.7 -by (expr.induct_tac "e" 1);
    54.8 +by (induct_tac "e" 1);
    54.9  (* case Var n *)
   54.10  by (Asm_simp_tac 1);
   54.11  (* case Abs e *)
   54.12 @@ -41,7 +41,7 @@
   54.13  
   54.14  (* the resulting type variable is always greater or equal than the given one *)
   54.15  Goal "!a n s t m. W e a n  = Ok (s,t,m) --> n<=m";
   54.16 -by (expr.induct_tac "e" 1);
   54.17 +by (induct_tac "e" 1);
   54.18  (* case Var(n) *)
   54.19  by (fast_tac (HOL_cs addss simpset()) 1);
   54.20  (* case Abs e *)
   54.21 @@ -85,7 +85,7 @@
   54.22  Goal
   54.23       "!n a s t m. new_tv n a --> W e a n = Ok (s,t,m) -->    \
   54.24  \                 new_tv m s & new_tv m t";
   54.25 -by (expr.induct_tac "e" 1);
   54.26 +by (induct_tac "e" 1);
   54.27  (* case Var n *)
   54.28  by (fast_tac (HOL_cs addDs [list_all_nth] addss (simpset() 
   54.29          addsimps [id_subst_def,new_tv_list,new_tv_subst])) 1);
   54.30 @@ -151,7 +151,7 @@
   54.31  
   54.32  Goal "!n a s t m v. W e a n = Ok (s,t,m) -->            \
   54.33  \         (v:free_tv s | v:free_tv t) --> v<n --> v:free_tv a";
   54.34 -by (expr.induct_tac "e" 1);
   54.35 +by (induct_tac "e" 1);
   54.36  (* case Var n *)
   54.37  by (fast_tac (HOL_cs addIs [nth_mem,subsetD,ftv_mem_sub_ftv_list] 
   54.38      addss simpset()) 1);
   54.39 @@ -217,7 +217,7 @@
   54.40   "!s' a t' n. $s' a |- e :: t' --> new_tv n a -->     \
   54.41  \             (? s t. (? m. W e a n = Ok (s,t,m)) &  \
   54.42  \                     (? r. $s' a = $r ($s a) & t' = $r t))";
   54.43 -by (expr.induct_tac "e" 1);
   54.44 +by (induct_tac "e" 1);
   54.45  (* case Var n *)
   54.46  by (strip_tac 1);
   54.47  by (simp_tac (simpset() addcongs [conj_cong]) 1);
    55.1 --- a/src/HOL/W0/W.thy	Fri Jul 24 13:03:20 1998 +0200
    55.2 +++ b/src/HOL/W0/W.thy	Fri Jul 24 13:19:38 1998 +0200
    55.3 @@ -15,7 +15,7 @@
    55.4  consts
    55.5          W :: [expr, typ list, nat] => result_W
    55.6  
    55.7 -primrec W expr
    55.8 +primrec
    55.9    "W (Var i) a n = (if i < length a then Ok(id_subst, a!i, n)
   55.10                      else Fail)"
   55.11    "W (Abs e) a n = ( (s,t,m) := W e ((TVar n)#a) (Suc n);
    56.1 --- a/src/HOL/ex/BT.ML	Fri Jul 24 13:03:20 1998 +0200
    56.2 +++ b/src/HOL/ex/BT.ML	Fri Jul 24 13:19:38 1998 +0200
    56.3 @@ -11,48 +11,48 @@
    56.4  (** BT simplification **)
    56.5  
    56.6  Goal "n_leaves(reflect(t)) = n_leaves(t)";
    56.7 -by (bt.induct_tac "t" 1);
    56.8 +by (induct_tac "t" 1);
    56.9  by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_commute])));
   56.10  qed "n_leaves_reflect";
   56.11  
   56.12  Goal "n_nodes(reflect(t)) = n_nodes(t)";
   56.13 -by (bt.induct_tac "t" 1);
   56.14 +by (induct_tac "t" 1);
   56.15  by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_commute])));
   56.16  qed "n_nodes_reflect";
   56.17  
   56.18  (*The famous relationship between the numbers of leaves and nodes*)
   56.19  Goal "n_leaves(t) = Suc(n_nodes(t))";
   56.20 -by (bt.induct_tac "t" 1);
   56.21 +by (induct_tac "t" 1);
   56.22  by (ALLGOALS Asm_simp_tac);
   56.23  qed "n_leaves_nodes";
   56.24  
   56.25  Goal "reflect(reflect(t))=t";
   56.26 -by (bt.induct_tac "t" 1);
   56.27 +by (induct_tac "t" 1);
   56.28  by (ALLGOALS Asm_simp_tac);
   56.29  qed "reflect_reflect_ident";
   56.30  
   56.31  Goal "bt_map f (reflect t) = reflect (bt_map f t)";
   56.32 -by (bt.induct_tac "t" 1);
   56.33 +by (induct_tac "t" 1);
   56.34  by (ALLGOALS Asm_simp_tac);
   56.35  qed "bt_map_reflect";
   56.36  
   56.37  Goal "inorder (bt_map f t) = map f (inorder t)";
   56.38 -by (bt.induct_tac "t" 1);
   56.39 +by (induct_tac "t" 1);
   56.40  by (ALLGOALS Asm_simp_tac);
   56.41  qed "inorder_bt_map";
   56.42  
   56.43  Goal "preorder (reflect t) = rev (postorder t)";
   56.44 -by (bt.induct_tac "t" 1);
   56.45 +by (induct_tac "t" 1);
   56.46  by (ALLGOALS Asm_simp_tac);
   56.47  qed "preorder_reflect";
   56.48  
   56.49  Goal "inorder (reflect t) = rev (inorder t)";
   56.50 -by (bt.induct_tac "t" 1);
   56.51 +by (induct_tac "t" 1);
   56.52  by (ALLGOALS Asm_simp_tac);
   56.53  qed "inorder_reflect";
   56.54  
   56.55  Goal "postorder (reflect t) = rev (preorder t)";
   56.56 -by (bt.induct_tac "t" 1);
   56.57 +by (induct_tac "t" 1);
   56.58  by (ALLGOALS Asm_simp_tac);
   56.59  qed "postorder_reflect";
   56.60  
    57.1 --- a/src/HOL/ex/BT.thy	Fri Jul 24 13:03:20 1998 +0200
    57.2 +++ b/src/HOL/ex/BT.thy	Fri Jul 24 13:19:38 1998 +0200
    57.3 @@ -19,31 +19,31 @@
    57.4      inorder     :: 'a bt => 'a list
    57.5      postorder   :: 'a bt => 'a list
    57.6  
    57.7 -primrec n_nodes bt
    57.8 +primrec
    57.9    "n_nodes (Lf) = 0"
   57.10    "n_nodes (Br a t1 t2) = Suc(n_nodes t1 + n_nodes t2)"
   57.11  
   57.12 -primrec n_leaves bt
   57.13 +primrec
   57.14    "n_leaves (Lf) = Suc 0"
   57.15    "n_leaves (Br a t1 t2) = n_leaves t1 + n_leaves t2"
   57.16  
   57.17 -primrec reflect bt
   57.18 +primrec
   57.19    "reflect (Lf) = Lf"
   57.20    "reflect (Br a t1 t2) = Br a (reflect t2) (reflect t1)"
   57.21  
   57.22 -primrec bt_map bt
   57.23 +primrec
   57.24    "bt_map f Lf = Lf"
   57.25    "bt_map f (Br a t1 t2) = Br (f a) (bt_map f t1) (bt_map f t2)"
   57.26  
   57.27 -primrec preorder bt
   57.28 +primrec
   57.29    "preorder (Lf) = []"
   57.30    "preorder (Br a t1 t2) = [a] @ (preorder t1) @ (preorder t2)"
   57.31  
   57.32 -primrec inorder bt
   57.33 +primrec
   57.34    "inorder (Lf) = []"
   57.35    "inorder (Br a t1 t2) = (inorder t1) @ [a] @ (inorder t2)"
   57.36  
   57.37 -primrec postorder bt
   57.38 +primrec
   57.39    "postorder (Lf) = []"
   57.40    "postorder (Br a t1 t2) = (postorder t1) @ (postorder t2) @ [a]"
   57.41  
    58.1 --- a/src/HOL/ex/InSort.ML	Fri Jul 24 13:03:20 1998 +0200
    58.2 +++ b/src/HOL/ex/InSort.ML	Fri Jul 24 13:19:38 1998 +0200
    58.3 @@ -7,13 +7,13 @@
    58.4  *)
    58.5  
    58.6  Goal "!y. mset(ins f x xs) y = mset (x#xs) y";
    58.7 -by (list.induct_tac "xs" 1);
    58.8 +by (induct_tac "xs" 1);
    58.9  by (ALLGOALS Asm_simp_tac);
   58.10  qed "mset_ins";
   58.11  Addsimps [mset_ins];
   58.12  
   58.13  Goal "!x. mset(insort f xs) x = mset xs x";
   58.14 -by (list.induct_tac "xs" 1);
   58.15 +by (induct_tac "xs" 1);
   58.16  by (ALLGOALS Asm_simp_tac);
   58.17  qed "insort_permutes";
   58.18  
   58.19 @@ -25,7 +25,7 @@
   58.20  
   58.21  val prems = goalw InSort.thy [total_def,transf_def]
   58.22    "[| total(f); transf(f) |] ==>  sorted f (ins f x xs) = sorted f xs";
   58.23 -by (list.induct_tac "xs" 1);
   58.24 +by (induct_tac "xs" 1);
   58.25  by (ALLGOALS Asm_simp_tac);
   58.26  by (cut_facts_tac prems 1);
   58.27  by (Fast_tac 1);
   58.28 @@ -33,6 +33,6 @@
   58.29  Addsimps [sorted_ins];
   58.30  
   58.31  Goal "[| total(f); transf(f) |] ==>  sorted f (insort f xs)";
   58.32 -by (list.induct_tac "xs" 1);
   58.33 +by (induct_tac "xs" 1);
   58.34  by (ALLGOALS Asm_simp_tac);
   58.35  qed "sorted_insort";
    59.1 --- a/src/HOL/ex/InSort.thy	Fri Jul 24 13:03:20 1998 +0200
    59.2 +++ b/src/HOL/ex/InSort.thy	Fri Jul 24 13:19:38 1998 +0200
    59.3 @@ -12,10 +12,10 @@
    59.4    ins :: [['a,'a]=>bool, 'a, 'a list] => 'a list
    59.5    insort :: [['a,'a]=>bool, 'a list] => 'a list
    59.6  
    59.7 -primrec ins List.list
    59.8 +primrec
    59.9    "ins f x [] = [x]"
   59.10    "ins f x (y#ys) = (if f x y then (x#y#ys) else y#(ins f x ys))"
   59.11 -primrec insort List.list
   59.12 +primrec
   59.13    "insort f [] = []"
   59.14    "insort f (x#xs) = ins f x (insort f xs)"
   59.15  end
    60.1 --- a/src/HOL/ex/NatSum.thy	Fri Jul 24 13:03:20 1998 +0200
    60.2 +++ b/src/HOL/ex/NatSum.thy	Fri Jul 24 13:19:38 1998 +0200
    60.3 @@ -8,7 +8,7 @@
    60.4  
    60.5  NatSum = Arith +
    60.6  consts sum     :: [nat=>nat, nat] => nat
    60.7 -primrec "sum" nat 
    60.8 +primrec 
    60.9    "sum f 0 = 0"
   60.10    "sum f (Suc n) = f(n) + sum f n"
   60.11  
    61.1 --- a/src/HOL/ex/Primes.thy	Fri Jul 24 13:03:20 1998 +0200
    61.2 +++ b/src/HOL/ex/Primes.thy	Fri Jul 24 13:19:38 1998 +0200
    61.3 @@ -11,7 +11,7 @@
    61.4  	Isabelle prove those conditions.
    61.5  *)
    61.6  
    61.7 -Primes = Divides + WF_Rel +
    61.8 +Primes = Divides + Recdef + Datatype +
    61.9  consts
   61.10    is_gcd  :: [nat,nat,nat]=>bool          (*gcd as a relation*)
   61.11    gcd     :: "nat*nat=>nat"               (*Euclid's algorithm *)
    62.1 --- a/src/HOL/ex/Primrec.thy	Fri Jul 24 13:03:20 1998 +0200
    62.2 +++ b/src/HOL/ex/Primrec.thy	Fri Jul 24 13:19:38 1998 +0200
    62.3 @@ -25,12 +25,12 @@
    62.4      "ack (Suc m, Suc n) = ack (m, ack (Suc m, n))"
    62.5  
    62.6  consts  list_add :: nat list => nat
    62.7 -primrec list_add list
    62.8 +primrec
    62.9    "list_add []     = 0"
   62.10    "list_add (m#ms) = m + list_add ms"
   62.11  
   62.12  consts  zeroHd  :: nat list => nat
   62.13 -primrec zeroHd list
   62.14 +primrec
   62.15    "zeroHd []     = 0"
   62.16    "zeroHd (m#ms) = m"
   62.17  
    63.1 --- a/src/HOL/ex/Qsort.ML	Fri Jul 24 13:03:20 1998 +0200
    63.2 +++ b/src/HOL/ex/Qsort.ML	Fri Jul 24 13:19:38 1998 +0200
    63.3 @@ -36,7 +36,7 @@
    63.4  
    63.5  goal List.thy
    63.6    "(!x:set[x:xs. P(x)].Q(x)) = (!x:set xs. P(x)-->Q(x))";
    63.7 -by (list.induct_tac "xs" 1);
    63.8 +by (induct_tac "xs" 1);
    63.9  by (ALLGOALS Asm_simp_tac);
   63.10  qed"Ball_set_filter";
   63.11  Addsimps [Ball_set_filter];
   63.12 @@ -44,7 +44,7 @@
   63.13  Goal
   63.14   "sorted le (xs@ys) = (sorted le xs & sorted le ys & \
   63.15  \                     (!x:set xs. !y:set ys. le x y))";
   63.16 -by (list.induct_tac "xs" 1);
   63.17 +by (induct_tac "xs" 1);
   63.18  by (ALLGOALS Asm_simp_tac);
   63.19  qed "sorted_append";
   63.20  Addsimps [sorted_append];
    64.1 --- a/src/HOL/ex/Sorting.ML	Fri Jul 24 13:03:20 1998 +0200
    64.2 +++ b/src/HOL/ex/Sorting.ML	Fri Jul 24 13:19:38 1998 +0200
    64.3 @@ -7,20 +7,20 @@
    64.4  *)
    64.5  
    64.6  Goal "!x. mset (xs@ys) x = mset xs x + mset ys x";
    64.7 -by (list.induct_tac "xs" 1);
    64.8 +by (induct_tac "xs" 1);
    64.9  by (ALLGOALS Asm_simp_tac);
   64.10  qed "mset_append";
   64.11  
   64.12  Goal "!x. mset [x:xs. ~p(x)] x + mset [x:xs. p(x)] x = \
   64.13  \                     mset xs x";
   64.14 -by (list.induct_tac "xs" 1);
   64.15 +by (induct_tac "xs" 1);
   64.16  by (ALLGOALS Asm_simp_tac);
   64.17  qed "mset_compl_add";
   64.18  
   64.19  Addsimps [mset_append, mset_compl_add];
   64.20  
   64.21  Goal "set xs = {x. mset xs x ~= 0}";
   64.22 -by (list.induct_tac "xs" 1);
   64.23 +by (induct_tac "xs" 1);
   64.24  by (ALLGOALS Asm_simp_tac);
   64.25  by (Fast_tac 1);
   64.26  qed "set_via_mset";
   64.27 @@ -29,8 +29,8 @@
   64.28  
   64.29  val prems = goalw Sorting.thy [transf_def]
   64.30    "transf(le) ==> sorted1 le xs = sorted le xs";
   64.31 -by (list.induct_tac "xs" 1);
   64.32 -by (ALLGOALS(asm_simp_tac (simpset() addsplits [split_list_case])));
   64.33 +by (induct_tac "xs" 1);
   64.34 +by (ALLGOALS(asm_simp_tac (simpset() addsplits [list.split])));
   64.35  by (cut_facts_tac prems 1);
   64.36  by (Fast_tac 1);
   64.37  qed "sorted1_is_sorted";
    65.1 --- a/src/HOL/ex/Sorting.thy	Fri Jul 24 13:03:20 1998 +0200
    65.2 +++ b/src/HOL/ex/Sorting.thy	Fri Jul 24 13:19:38 1998 +0200
    65.3 @@ -14,16 +14,16 @@
    65.4    total  :: (['a,'a] => bool) => bool
    65.5    transf :: (['a,'a] => bool) => bool
    65.6  
    65.7 -primrec sorted1 list
    65.8 +primrec
    65.9    "sorted1 le [] = True"
   65.10    "sorted1 le (x#xs) = ((case xs of [] => True | y#ys => le x y) &
   65.11                          sorted1 le xs)"
   65.12  
   65.13 -primrec sorted list
   65.14 +primrec
   65.15    "sorted le [] = True"
   65.16    "sorted le (x#xs) = ((!y:set xs. le x y) & sorted le xs)"
   65.17  
   65.18 -primrec mset list
   65.19 +primrec
   65.20    "mset [] y = 0"
   65.21    "mset (x#xs) y = (if x=y then Suc(mset xs y) else mset xs y)"
   65.22