Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
simplified induction;
authorwenzelm
Sun, 12 Nov 2000 14:49:37 +0100
changeset 10458 df4e182c0fcd
parent 10457 dd669bda2b0c
child 10459 df3cd3e76046
simplified induction;
src/HOL/Isar_examples/NestedDatatype.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle