Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
syntactic constants;
authorwenzelm
Mon, 06 Oct 1997 09:26:00 +0200
changeset 3773 989ef5e9d543
parent 3772 6ee707a73248
child 3774 b1bfd394b60a
syntactic constants;
src/Cube/Cube.thy file | annotate | diff | comparison | revisions 
--- 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"
isabelle