replaced id by idt;
authorwenzelm
Mon Oct 04 15:49:49 1993 +0100 (1993-10-04)
changeset 231cd377c2f7c6
parent 22 41dc6b189412
child 24 f3d4ff75d9f2
replaced id by idt;
added parse rules for --> and *;
removed ndependent_tr;
src/CTT/CTT.thy
src/CTT/ctt.thy
     1.1 --- a/src/CTT/CTT.thy	Mon Oct 04 15:44:54 1993 +0100
     1.2 +++ b/src/CTT/CTT.thy	Mon Oct 04 15:49:49 1993 +0100
     1.3 @@ -40,8 +40,8 @@
     1.4    Eqelem    :: "[i,i,t]=>prop"      ("(3_ =/ _ :/ _)" [10,10,10] 5)
     1.5    Reduce    :: "[i,i]=>prop"        ("Reduce[_,_]")
     1.6    (*Types*)
     1.7 -  "@PROD"   :: "[id,t,t]=>t"        ("(3PROD _:_./ _)" 10)
     1.8 -  "@SUM"    :: "[id,t,t]=>t"        ("(3SUM _:_./ _)" 10)
     1.9 +  "@PROD"   :: "[idt,t,t]=>t"       ("(3PROD _:_./ _)" 10)
    1.10 +  "@SUM"    :: "[idt,t,t]=>t"       ("(3SUM _:_./ _)" 10)
    1.11    "+"       :: "[t,t]=>t"           (infixr 40)
    1.12    (*Invisible infixes!*)
    1.13    "@-->"    :: "[t,t]=>t"           ("(_ -->/ _)" [31,30] 30)
    1.14 @@ -56,7 +56,9 @@
    1.15  
    1.16  translations
    1.17    "PROD x:A. B" => "Prod(A, %x. B)"
    1.18 +  "A --> B"     => "Prod(A, _K(B))"
    1.19    "SUM x:A. B"  => "Sum(A, %x. B)"
    1.20 +  "A * B"       => "Sum(A, _K(B))"
    1.21  
    1.22  rules
    1.23  
    1.24 @@ -244,9 +246,6 @@
    1.25  
    1.26  ML
    1.27  
    1.28 -val parse_translation =
    1.29 -  [("@-->", ndependent_tr "Prod"), ("@*", ndependent_tr "Sum")];
    1.30 -
    1.31  val print_translation =
    1.32    [("Prod", dependent_tr' ("@PROD", "@-->")),
    1.33     ("Sum", dependent_tr' ("@SUM", "@*"))];
     2.1 --- a/src/CTT/ctt.thy	Mon Oct 04 15:44:54 1993 +0100
     2.2 +++ b/src/CTT/ctt.thy	Mon Oct 04 15:49:49 1993 +0100
     2.3 @@ -40,8 +40,8 @@
     2.4    Eqelem    :: "[i,i,t]=>prop"      ("(3_ =/ _ :/ _)" [10,10,10] 5)
     2.5    Reduce    :: "[i,i]=>prop"        ("Reduce[_,_]")
     2.6    (*Types*)
     2.7 -  "@PROD"   :: "[id,t,t]=>t"        ("(3PROD _:_./ _)" 10)
     2.8 -  "@SUM"    :: "[id,t,t]=>t"        ("(3SUM _:_./ _)" 10)
     2.9 +  "@PROD"   :: "[idt,t,t]=>t"       ("(3PROD _:_./ _)" 10)
    2.10 +  "@SUM"    :: "[idt,t,t]=>t"       ("(3SUM _:_./ _)" 10)
    2.11    "+"       :: "[t,t]=>t"           (infixr 40)
    2.12    (*Invisible infixes!*)
    2.13    "@-->"    :: "[t,t]=>t"           ("(_ -->/ _)" [31,30] 30)
    2.14 @@ -56,7 +56,9 @@
    2.15  
    2.16  translations
    2.17    "PROD x:A. B" => "Prod(A, %x. B)"
    2.18 +  "A --> B"     => "Prod(A, _K(B))"
    2.19    "SUM x:A. B"  => "Sum(A, %x. B)"
    2.20 +  "A * B"       => "Sum(A, _K(B))"
    2.21  
    2.22  rules
    2.23  
    2.24 @@ -244,9 +246,6 @@
    2.25  
    2.26  ML
    2.27  
    2.28 -val parse_translation =
    2.29 -  [("@-->", ndependent_tr "Prod"), ("@*", ndependent_tr "Sum")];
    2.30 -
    2.31  val print_translation =
    2.32    [("Prod", dependent_tr' ("@PROD", "@-->")),
    2.33     ("Sum", dependent_tr' ("@SUM", "@*"))];