src/HOL/Isar_examples/NestedDatatype.thy
changeset 11809 c9ffdd63dd93
parent 10458 df4e182c0fcd
child 16417 9bc16273c2d4
     1.1 --- a/src/HOL/Isar_examples/NestedDatatype.thy	Tue Oct 16 17:56:12 2001 +0200
     1.2 +++ b/src/HOL/Isar_examples/NestedDatatype.thy	Tue Oct 16 17:58:13 2001 +0200
     1.3 @@ -30,7 +30,7 @@
     1.4        subst_term f1 (subst_term f2 t) &
     1.5      subst_term_list (subst_term f1 o f2) ts =
     1.6        subst_term_list f1 (subst_term_list f2 ts)"
     1.7 -  by (induct t and ts rule: term.induct) simp_all
     1.8 +  by (induct t and ts) simp_all
     1.9  
    1.10  lemma "subst_term (subst_term f1 o f2) t =
    1.11    subst_term f1 (subst_term f2 t)"
    1.12 @@ -62,7 +62,7 @@
    1.13    assume var: "!!a. P (Var a)"
    1.14    assume app: "!!b ts. list_all P ts ==> P (App b ts)"
    1.15    show ?thesis
    1.16 -  proof (induct P t)
    1.17 +  proof (induct t)
    1.18      fix a show "P (Var a)" by (rule var)
    1.19    next
    1.20      fix b t ts assume "list_all P ts"
    1.21 @@ -78,12 +78,12 @@
    1.22  lemma
    1.23    "subst_term (subst_term f1 o f2) t = subst_term f1 (subst_term f2 t)"
    1.24    (is "?P t")
    1.25 -proof (induct (open) ?P t rule: term_induct')
    1.26 -  case Var
    1.27 +proof (induct t rule: term_induct')
    1.28 +  case (Var a)
    1.29    show "?P (Var a)" by (simp add: o_def)
    1.30  next
    1.31 -  case App
    1.32 -  show "?P (App b ts)" by (insert App, induct ts) simp_all
    1.33 +  case (App b ts)
    1.34 +  thus "?P (App b ts)" by (induct ts) simp_all
    1.35  qed
    1.36  
    1.37  end