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/Lambda/Type.thy
changeset 15236 f289e8ba2bb3
parent 14565 c6dc17aab88a
child 16417 9bc16273c2d4 
--- a/src/HOL/Lambda/Type.thy	Mon Oct 11 07:39:19 2004 +0200
+++ b/src/HOL/Lambda/Type.thy	Mon Oct 11 07:42:22 2004 +0200
@@ -121,7 +121,7 @@
   apply (case_tac Ts)
   apply simp+
   apply (case_tac Ts)
-  apply (case_tac "list @ [t]")
+  apply (case_tac "ts @ [t]")
   apply simp+
   done
 
@@ -185,7 +185,7 @@
   apply simp
   apply (erule_tac x = "t \<degree> a" in allE)
   apply (erule_tac x = T in allE)
-  apply (erule_tac x = lista in allE)
+  apply (erule_tac x = list in allE)
   apply (erule impE)
    apply (erule conjE)
    apply (erule typing.App)
isabelle