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.
replaced id by idt;
authorwenzelm
Mon, 04 Oct 1993 15:44:29 +0100
changeset 21 b5f8677e24e7
parent 20 e6fb60365db9
child 22 41dc6b189412
replaced id by idt; added parse rule for ->; removed ndependent_tr;
src/Cube/Cube.thy file | annotate | diff | comparison | revisions
src/Cube/cube.thy file | annotate | diff | comparison | revisions 
--- a/src/Cube/Cube.thy	Mon Oct 04 15:38:02 1993 +0100
+++ b/src/Cube/Cube.thy	Mon Oct 04 15:44:29 1993 +0100
@@ -25,8 +25,8 @@
   star          :: "term"                               ("*")
   box           :: "term"                               ("[]")
   "^"           :: "[term, term] => term"               (infixl 20)
-  Lam           :: "[id, term, term] => term"           ("(3Lam _:_./ _)" [0, 0, 0] 10)
-  Pi            :: "[id, term, term] => term"           ("(3Pi _:_./ _)" [0, 0] 10)
+  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)
 
@@ -34,6 +34,7 @@
   (prop) "x:X"  == (prop) "|- x:X"
   "Lam x:A. B"  == "Abs(A, %x. B)"
   "Pi x:A. B"   => "Prod(A, %x. B)"
+  "A -> B"      => "Prod(A, _K(B))"
 
 rules
   s_b           "*: []"
@@ -55,6 +56,5 @@
 
 ML
 
-val parse_translation = [("op ->", ndependent_tr "Prod")];
 val print_translation = [("Prod", dependent_tr' ("Pi", "op ->"))];
 
--- a/src/Cube/cube.thy	Mon Oct 04 15:38:02 1993 +0100
+++ b/src/Cube/cube.thy	Mon Oct 04 15:44:29 1993 +0100
@@ -25,8 +25,8 @@
   star          :: "term"                               ("*")
   box           :: "term"                               ("[]")
   "^"           :: "[term, term] => term"               (infixl 20)
-  Lam           :: "[id, term, term] => term"           ("(3Lam _:_./ _)" [0, 0, 0] 10)
-  Pi            :: "[id, term, term] => term"           ("(3Pi _:_./ _)" [0, 0] 10)
+  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)
 
@@ -34,6 +34,7 @@
   (prop) "x:X"  == (prop) "|- x:X"
   "Lam x:A. B"  == "Abs(A, %x. B)"
   "Pi x:A. B"   => "Prod(A, %x. B)"
+  "A -> B"      => "Prod(A, _K(B))"
 
 rules
   s_b           "*: []"
@@ -55,6 +56,5 @@
 
 ML
 
-val parse_translation = [("op ->", ndependent_tr "Prod")];
 val print_translation = [("Prod", dependent_tr' ("Pi", "op ->"))];
isabelle