src/HOL/Induct/LList.ML
changeset 8442 96023903c2df
parent 8423 3c19160b6432
child 8703 816d8f6513be
     1.1 --- a/src/HOL/Induct/LList.ML	Mon Mar 13 15:42:19 2000 +0100
     1.2 +++ b/src/HOL/Induct/LList.ML	Mon Mar 13 16:23:34 2000 +0100
     1.3 @@ -76,7 +76,7 @@
     1.4      "LList_corec a f <= \
     1.5  \    (case f a of None => NIL | Some(z,w) => CONS z (LList_corec w f))";
     1.6  by (rtac UN_least 1);
     1.7 -by (cases_tac "k" 1);
     1.8 +by (case_tac "k" 1);
     1.9  by (ALLGOALS Asm_simp_tac);
    1.10  by (REPEAT (resolve_tac [allI, impI, subset_refl RS CONS_mono, 
    1.11  			 UNIV_I RS UN_upper] 1));
    1.12 @@ -132,10 +132,10 @@
    1.13  by (safe_tac (claset() delrules [equalityI]));
    1.14  by (etac LListD.elim 1);
    1.15  by (safe_tac (claset() delrules [equalityI]));
    1.16 -by (cases_tac "n" 1);
    1.17 +by (case_tac "n" 1);
    1.18  by (Asm_simp_tac 1);
    1.19  by (rename_tac "n'" 1);
    1.20 -by (cases_tac "n'" 1);
    1.21 +by (case_tac "n'" 1);
    1.22  by (asm_simp_tac (simpset() addsimps [CONS_def]) 1);
    1.23  by (asm_simp_tac (simpset() addsimps [CONS_def, less_Suc_eq]) 1);
    1.24  qed "LListD_implies_ntrunc_equality";
    1.25 @@ -295,9 +295,9 @@
    1.26  by (stac prem2 1);
    1.27  by (Simp_tac 1);
    1.28  by (strip_tac 1);
    1.29 -by (cases_tac "n" 1);
    1.30 +by (case_tac "n" 1);
    1.31  by (rename_tac "m" 2);
    1.32 -by (cases_tac "m" 2);
    1.33 +by (case_tac "m" 2);
    1.34  by (ALLGOALS (asm_simp_tac (simpset() addsimps [less_Suc_eq])));
    1.35  result();
    1.36  
    1.37 @@ -598,7 +598,7 @@
    1.38      "llist_corec a f =  \
    1.39  \    (case f a of None => LNil | Some(z,w) => LCons z (llist_corec w f))";
    1.40  by (stac LList_corec 1);
    1.41 -by (cases_tac "f a" 1);
    1.42 +by (case_tac "f a" 1);
    1.43  by (asm_simp_tac (simpset() addsimps [LList_corec_type2]) 1);
    1.44  by (force_tac (claset(), simpset() addsimps [LList_corec_type2]) 1);
    1.45  qed "llist_corec";