1.1 --- a/src/Cube/Cube.thy	Mon Oct 04 15:38:02 1993 +0100
     1.2 +++ b/src/Cube/Cube.thy	Mon Oct 04 15:44:29 1993 +0100
     1.3 @@ -25,8 +25,8 @@
     1.4    star          :: "term"                               ("*")
     1.5    box           :: "term"                               ("[]")
     1.6    "^"           :: "[term, term] => term"               (infixl 20)
     1.7 -  Lam           :: "[id, term, term] => term"           ("(3Lam _:_./ _)" [0, 0, 0] 10)
     1.8 -  Pi            :: "[id, term, term] => term"           ("(3Pi _:_./ _)" [0, 0] 10)
     1.9 +  Lam           :: "[idt, term, term] => term"          ("(3Lam _:_./ _)" [0, 0, 0] 10)
    1.10 +  Pi            :: "[idt, term, term] => term"          ("(3Pi _:_./ _)" [0, 0] 10)
    1.11    "->"          :: "[term, term] => term"               (infixr 10)
    1.12    Has_type      :: "[term, term] => typing"             ("(_:/ _)" [0, 0] 5)
    1.13  
    1.14 @@ -34,6 +34,7 @@
    1.15    (prop) "x:X"  == (prop) "|- x:X"
    1.16    "Lam x:A. B"  == "Abs(A, %x. B)"
    1.17    "Pi x:A. B"   => "Prod(A, %x. B)"
    1.18 +  "A -> B"      => "Prod(A, _K(B))"
    1.19  
    1.20  rules
    1.21    s_b           "*: []"
    1.22 @@ -55,6 +56,5 @@
    1.23  
    1.24  ML
    1.25  
    1.26 -val parse_translation = [("op ->", ndependent_tr "Prod")];
    1.27  val print_translation = [("Prod", dependent_tr' ("Pi", "op ->"))];
    1.28  

     2.1 --- a/src/Cube/cube.thy	Mon Oct 04 15:38:02 1993 +0100
     2.2 +++ b/src/Cube/cube.thy	Mon Oct 04 15:44:29 1993 +0100
     2.3 @@ -25,8 +25,8 @@
     2.4    star          :: "term"                               ("*")
     2.5    box           :: "term"                               ("[]")
     2.6    "^"           :: "[term, term] => term"               (infixl 20)
     2.7 -  Lam           :: "[id, term, term] => term"           ("(3Lam _:_./ _)" [0, 0, 0] 10)
     2.8 -  Pi            :: "[id, term, term] => term"           ("(3Pi _:_./ _)" [0, 0] 10)
     2.9 +  Lam           :: "[idt, term, term] => term"          ("(3Lam _:_./ _)" [0, 0, 0] 10)
    2.10 +  Pi            :: "[idt, term, term] => term"          ("(3Pi _:_./ _)" [0, 0] 10)
    2.11    "->"          :: "[term, term] => term"               (infixr 10)
    2.12    Has_type      :: "[term, term] => typing"             ("(_:/ _)" [0, 0] 5)
    2.13  
    2.14 @@ -34,6 +34,7 @@
    2.15    (prop) "x:X"  == (prop) "|- x:X"
    2.16    "Lam x:A. B"  == "Abs(A, %x. B)"
    2.17    "Pi x:A. B"   => "Prod(A, %x. B)"
    2.18 +  "A -> B"      => "Prod(A, _K(B))"
    2.19  
    2.20  rules
    2.21    s_b           "*: []"
    2.22 @@ -55,6 +56,5 @@
    2.23  
    2.24  ML
    2.25  
    2.26 -val parse_translation = [("op ->", ndependent_tr "Prod")];
    2.27  val print_translation = [("Prod", dependent_tr' ("Pi", "op ->"))];
    2.28