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.
new 'THEN' syntax;
authorwenzelm
Wed, 04 Oct 2000 22:21:10 +0200
changeset 10155 6263a4a60e38
parent 10154 05d6ccb2f536
child 10156 9d4d5852eb47
new 'THEN' syntax;
src/HOL/Lambda/Type.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Lambda/Type.thy	Wed Oct 04 21:06:01 2000 +0200
+++ b/src/HOL/Lambda/Type.thy	Wed Oct 04 22:21:10 2000 +0200
@@ -454,7 +454,7 @@
    apply simp
   apply (rule subst_type_IT)
   apply (rule lists.Nil
-    [THEN 2 lists.Cons [THEN IT.Var], unfolded foldl_Nil [THEN eq_reflection]
+    [THEN [2] lists.Cons [THEN IT.Var], unfolded foldl_Nil [THEN eq_reflection]
       foldl_Cons [THEN eq_reflection]])
       apply (erule lift_IT)
      apply (rule typing.App)
isabelle