# HG changeset patch
# User wenzelm
# Date 1085167115 -7200
# Node ID 556d9cc7371170bacd978987513257ee44880607
# Parent  c52060b69a8cfcf9f0ffc0a75dfa274322712626
adapted syntax to cope with lack of non-logical types;

diff -r c52060b69a8c -r 556d9cc73711 src/Cube/Base.thy
--- a/src/Cube/Base.thy	Fri May 21 21:18:14 2004 +0200
+++ b/src/Cube/Base.thy	Fri May 21 21:18:35 2004 +0200
@@ -9,25 +9,33 @@
 Base = Pure +
 
 types
-  term  context  typing
-
+  term
 arities
   term :: logic
 
+types
+  context  typing
+nonterminals
+  context_ typing_
+
 consts
   Abs, Prod     :: "[term, term => term] => term"
-  Trueprop      :: "[context, typing] => prop"          ("(_/ |- _)")
-  MT_context    :: "context"                            ("")
-  Context       :: "[typing, context] => context"       ("_ _")
+  Trueprop      :: "[context, typing] => prop"
+  MT_context    :: "context"
+  Context       :: "[typing, context] => context"
   star          :: "term"                               ("*")
   box           :: "term"                               ("[]")
   "^"           :: "[term, term] => term"               (infixl 20)
-  Has_type      :: "[term, term] => typing"             ("(_:/ _)" [0, 0] 5)
+  Has_type      :: "[term, term] => typing"
 
 syntax
-  Trueprop1     :: "typing => prop"                     ("(_)")
-  ""            :: "id => context"                      ("_ ")
-  ""            :: "var => context"                     ("_ ")
+  Trueprop      :: "[context_, typing_] => prop"        ("(_/ |- _)")
+  Trueprop1     :: "typing_ => prop"                    ("(_)")
+  ""            :: "id => context_"                     ("_")
+  ""            :: "var => context_"                    ("_")
+  MT_context    :: "context_"                           ("")
+  Context       :: "[typing_, context_] => context_"    ("_ _")
+  Has_type      :: "[term, term] => typing_"            ("(_:/ _)" [0, 0] 5)
   Lam           :: "[idt, term, term] => term"          ("(3Lam _:_./ _)" [0, 0, 0] 10)
   Pi            :: "[idt, term, term] => term"          ("(3Pi _:_./ _)" [0, 0] 10)
   "->"          :: "[term, term] => term"               (infixr 10)
@@ -39,7 +47,7 @@
   "A -> B"      => "Prod(A, _K(B))"
 
 syntax (xsymbols)
-  Trueprop      :: "[context, typing] => prop"          ("(_/ \\<turnstile> _)")
+  Trueprop      :: "[context_, typing_] => prop"        ("(_/ \\<turnstile> _)")
   box           :: "term"                               ("\\<box>")
   Lam           :: "[idt, term, term] => term"          ("(3\\<Lambda>_:_./ _)" [0, 0, 0] 10)
   Pi            :: "[idt, term, term] => term"          ("(3\\<Pi>_:_./ _)" [0, 0] 10)