simplified induction;
authorwenzelm
Sun Nov 12 14:49:37 2000 +0100 (2000-11-12)
changeset 10458df4e182c0fcd
parent 10457 dd669bda2b0c
child 10459 df3cd3e76046
simplified induction;
src/HOL/Isar_examples/NestedDatatype.thy
     1.1 --- a/src/HOL/Isar_examples/NestedDatatype.thy	Sun Nov 12 14:48:47 2000 +0100
     1.2 +++ b/src/HOL/Isar_examples/NestedDatatype.thy	Sun Nov 12 14:49:37 2000 +0100
     1.3 @@ -83,9 +83,7 @@
     1.4    show "?P (Var a)" by (simp add: o_def)
     1.5  next
     1.6    case App
     1.7 -  have "?this --> ?P (App b ts)"
     1.8 -    by (induct ts) simp_all
     1.9 -  thus "..." ..
    1.10 +  show "?P (App b ts)" by (insert App, induct ts) simp_all
    1.11  qed
    1.12  
    1.13  end