src/HOL/Isar_examples/NestedDatatype.thy
changeset 9659 b9cf6801f3da
parent 8717 20c42415c07d
child 10007 64bf7da1994a
     1.1 --- a/src/HOL/Isar_examples/NestedDatatype.thy	Sat Aug 19 12:44:20 2000 +0200
     1.2 +++ b/src/HOL/Isar_examples/NestedDatatype.thy	Sat Aug 19 12:44:39 2000 +0200
     1.3 @@ -32,7 +32,8 @@
     1.4        subst_term_list f1 (subst_term_list f2 ts)";
     1.5    by (induct t and ts rule: term.induct) simp_all;
     1.6  
     1.7 -lemma "subst_term (subst_term f1 o f2) t = subst_term f1 (subst_term f2 t)";
     1.8 +lemma "subst_term (subst_term f1 o f2) t =
     1.9 +  subst_term f1 (subst_term f2 t)";
    1.10  proof -;
    1.11    let "?P t" = ?thesis;
    1.12    let ?Q = "\\<lambda>ts. subst_term_list (subst_term f1 o f2) ts =
    1.13 @@ -55,7 +56,8 @@
    1.14  subsection {* Alternative induction *};
    1.15  
    1.16  theorem term_induct' [case_names Var App]:
    1.17 - "(!!a. P (Var a)) ==> (!!b ts. list_all P ts ==> P (App b ts)) ==> P t";
    1.18 +  "(!!a. P (Var a)) ==>
    1.19 +   (!!b ts. list_all P ts ==> P (App b ts)) ==> P t";
    1.20  proof -;
    1.21    assume var: "!!a. P (Var a)";
    1.22    assume app: "!!b ts. list_all P ts ==> P (App b ts)";
    1.23 @@ -76,7 +78,7 @@
    1.24  lemma
    1.25    "subst_term (subst_term f1 o f2) t = subst_term f1 (subst_term f2 t)"
    1.26    (is "?P t");
    1.27 -proof (induct ?P t rule: term_induct');
    1.28 +proof (induct (open) ?P t rule: term_induct');
    1.29    case Var;
    1.30    show "?P (Var a)"; by (simp add: o_def);
    1.31  next;