# HG changeset patch
# User wenzelm
# Date 876122760 -7200
# Node ID 989ef5e9d543c4927e06fbcc288189016ddf0d5a
# Parent  6ee707a73248772661c2a9561c36c2ec35db05f0
syntactic constants;

diff -r 6ee707a73248 -r 989ef5e9d543 src/Cube/Cube.thy
--- a/src/Cube/Cube.thy	Fri Oct 03 10:32:50 1997 +0200
+++ b/src/Cube/Cube.thy	Mon Oct 06 09:26:00 1997 +0200
@@ -17,18 +17,20 @@
 consts
   Abs, Prod     :: "[term, term => term] => term"
   Trueprop      :: "[context, typing] => prop"          ("(_/ |- _)")
-  Trueprop1     :: "typing => prop"                     ("(_)")
   MT_context    :: "context"                            ("")
-  ""            :: "id => context"                      ("_ ")
-  ""            :: "var => context"                     ("_ ")
   Context       :: "[typing, context] => context"       ("_ _")
   star          :: "term"                               ("*")
   box           :: "term"                               ("[]")
   "^"           :: "[term, term] => term"               (infixl 20)
+  "->"          :: "[term, term] => term"               (infixr 10)
+  Has_type      :: "[term, term] => typing"             ("(_:/ _)" [0, 0] 5)
+
+syntax
+  Trueprop1     :: "typing => prop"                     ("(_)")
+  ""            :: "id => context"                      ("_ ")
+  ""            :: "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)
-  Has_type      :: "[term, term] => typing"             ("(_:/ _)" [0, 0] 5)
 
 translations
   (prop) "x:X"  == (prop) "|- x:X"