# HG changeset patch
# User wenzelm
# Date 885394225 -3600
# Node ID 3588b8f9613ff4775b039b61d6febb0930d995a5
# Parent  6d9be46ea566580ecd07863f894b17a8d6b0a7df
added symbols syntax;

diff -r 6d9be46ea566 -r 3588b8f9613f src/Cube/Base.thy
--- a/src/Cube/Base.thy	Tue Jan 20 18:26:26 1998 +0100
+++ b/src/Cube/Base.thy	Wed Jan 21 15:50:25 1998 +0100
@@ -38,6 +38,14 @@
   "Pi x:A. B"   => "Prod(A, %x. B)"
   "A -> B"      => "Prod(A, _K(B))"
 
+syntax (symbols)
+  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)
+  "op ->"       :: "[term, term] => term"               (infixr "\\<rightarrow>" 10)
+
+
 rules
   s_b           "*: []"