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.
"->" made syntax;
authorwenzelm
Mon, 06 Oct 1997 19:16:57 +0200
changeset 3796 60c788035e54
parent 3795 e687069e7257
child 3797 05e47c7cc6fd
"->" made syntax;
src/Cube/Cube.thy file | annotate | diff | comparison | revisions 
--- 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"
isabelle