# HG changeset patch
# User wenzelm
# Date 974036977 -3600
# Node ID df4e182c0fcd1190fbe4b2cb19e2a1334ae0ce14
# Parent  dd669bda2b0c8f356e4afa21d73f3756fa8e2fd6
simplified induction;

diff -r dd669bda2b0c -r df4e182c0fcd src/HOL/Isar_examples/NestedDatatype.thy
--- a/src/HOL/Isar_examples/NestedDatatype.thy	Sun Nov 12 14:48:47 2000 +0100
+++ b/src/HOL/Isar_examples/NestedDatatype.thy	Sun Nov 12 14:49:37 2000 +0100
@@ -83,9 +83,7 @@
   show "?P (Var a)" by (simp add: o_def)
 next
   case App
-  have "?this --> ?P (App b ts)"
-    by (induct ts) simp_all
-  thus "..." ..
+  show "?P (App b ts)" by (insert App, induct ts) simp_all
 qed
 
 end