src/HOL/Isar_examples/NestedDatatype.thy
changeset 23373 ead82c82da9e
parent 18460 9a1458cb2956
     1.1 --- a/src/HOL/Isar_examples/NestedDatatype.thy	Wed Jun 13 16:43:02 2007 +0200
     1.2 +++ b/src/HOL/Isar_examples/NestedDatatype.thy	Wed Jun 13 18:30:11 2007 +0200
     1.3 @@ -44,12 +44,14 @@
     1.4      fix a show "?P (Var a)" by simp
     1.5    next
     1.6      fix b ts assume "?Q ts"
     1.7 -    thus "?P (App b ts)" by (simp add: o_def)
     1.8 +    then show "?P (App b ts)"
     1.9 +      by (simp only: subst.simps)
    1.10    next
    1.11      show "?Q []" by simp
    1.12    next
    1.13      fix t ts
    1.14 -    assume "?P t" "?Q ts" thus "?Q (t # ts)" by simp
    1.15 +    assume "?P t" "?Q ts" then show "?Q (t # ts)"
    1.16 +      by (simp only: subst.simps)
    1.17    qed
    1.18  qed
    1.19  
    1.20 @@ -64,12 +66,12 @@
    1.21    fix a show "P (Var a)" by (rule var)
    1.22  next
    1.23    fix b t ts assume "list_all P ts"
    1.24 -  thus "P (App b ts)" by (rule app)
    1.25 +  then show "P (App b ts)" by (rule app)
    1.26  next
    1.27    show "list_all P []" by simp
    1.28  next
    1.29    fix t ts assume "P t" "list_all P ts"
    1.30 -  thus "list_all P (t # ts)" by simp
    1.31 +  then show "list_all P (t # ts)" by simp
    1.32  qed
    1.33  
    1.34  lemma
    1.35 @@ -79,7 +81,7 @@
    1.36    show ?case by (simp add: o_def)
    1.37  next
    1.38    case (App b ts)
    1.39 -  thus ?case by (induct ts) simp_all
    1.40 +  then show ?case by (induct ts) simp_all
    1.41  qed
    1.42  
    1.43  end