# 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"