# HG changeset patch
# User wenzelm
# Date 876158217 -7200
# Node ID 60c788035e54d4e583e3208e169250adba60cf74
# Parent  e687069e7257b6b7174be29d835816742c98d57b
"->" made syntax;

diff -r e687069e7257 -r 60c788035e54 src/Cube/Cube.thy
--- 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"