Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Isar_examples/W_correct.thy
changeset 11987 bf31b35949ce
parent 11809 c9ffdd63dd93 
--- a/src/HOL/Isar_examples/W_correct.thy	Tue Oct 30 17:33:56 2001 +0100
+++ b/src/HOL/Isar_examples/W_correct.thy	Tue Oct 30 17:37:25 2001 +0100
@@ -46,8 +46,8 @@
 proof -
   assume "a |- e :: t"
   thus ?thesis (is "?P a e t")
-  proof (induct (open) a e t)
-    case Var
+  proof induct
+    case (Var a n)
     hence "n < length (map ($ s) a)" by simp
     hence "map ($ s) a |- Var n :: map ($ s) a ! n"
       by (rule has_type.Var)
@@ -57,7 +57,7 @@
       by (simp only: app_subst_list)
     finally show "?P a (Var n) (a ! n)" .
   next
-    case Abs
+    case (Abs a e t1 t2)
     hence "$ s t1 # map ($ s) a |- e :: $ s t2"
       by (simp add: app_subst_list)
     hence "map ($ s) a |- Abs e :: $ s t1 -> $ s t2"
@@ -66,7 +66,7 @@
       by (simp add: app_subst_list)
   next
     case App
-    thus "?P a (App e1 e2) t1" by (simp add: has_type.App)
+    thus ?case by (simp add: has_type.App)
   qed
 qed
isabelle