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/Cube/Cube.thy
changeset 3796 60c788035e54
parent 3773 989ef5e9d543
child 4583 6d9be46ea566 
--- a/src/Cube/Cube.thy	Mon Oct 06 19:15:22 1997 +0200
+++ b/src/Cube/Cube.thy	Mon Oct 06 19:16:57 1997 +0200
@@ -1,4 +1,4 @@
-(*  Title:      Cube/cube.thy
+(*  Title:      Cube/Cube.thy
     ID:         $Id$
     Author:     Tobias Nipkow
     Copyright   1993  University of Cambridge
@@ -22,7 +22,6 @@
   star          :: "term"                               ("*")
   box           :: "term"                               ("[]")
   "^"           :: "[term, term] => term"               (infixl 20)
-  "->"          :: "[term, term] => term"               (infixr 10)
   Has_type      :: "[term, term] => typing"             ("(_:/ _)" [0, 0] 5)
 
 syntax
@@ -31,6 +30,7 @@
   ""            :: "var => context"                     ("_ ")
   Lam           :: "[idt, term, term] => term"          ("(3Lam _:_./ _)" [0, 0, 0] 10)
   Pi            :: "[idt, term, term] => term"          ("(3Pi _:_./ _)" [0, 0] 10)
+  "->"          :: "[term, term] => term"               (infixr 10)
 
 translations
   (prop) "x:X"  == (prop) "|- x:X"
isabelle