added parse rules for -> and *;
authorwenzelm
Mon Oct 04 15:44:54 1993 +0100 (1993-10-04)
changeset 2241dc6b189412
parent 21 b5f8677e24e7
child 23 1cd377c2f7c6
added parse rules for -> and *;
removed ndependent_tr;
src/CCL/Type.thy
src/CCL/type.thy
     1.1 --- a/src/CCL/Type.thy	Mon Oct 04 15:44:29 1993 +0100
     1.2 +++ b/src/CCL/Type.thy	Mon Oct 04 15:44:54 1993 +0100
     1.3 @@ -35,7 +35,9 @@
     1.4  
     1.5  translations
     1.6    "PROD x:A. B" => "Pi(A, %x. B)"
     1.7 +  "A -> B"      => "Pi(A, _K(B))"
     1.8    "SUM x:A. B"  => "Sigma(A, %x. B)"
     1.9 +  "A * B"       => "Sigma(A, _K(B))"
    1.10    "{x: A. B}"   == "Subtype(A, %x. B)"
    1.11  
    1.12  rules
    1.13 @@ -63,10 +65,6 @@
    1.14  
    1.15  ML
    1.16  
    1.17 -val parse_translation =
    1.18 -  [("@->", ndependent_tr "Pi"),
    1.19 -   ("@*", ndependent_tr "Sigma")];
    1.20 -
    1.21  val print_translation =
    1.22    [("Pi", dependent_tr' ("@Pi", "@->")),
    1.23     ("Sigma", dependent_tr' ("@Sigma", "@*"))];
     2.1 --- a/src/CCL/type.thy	Mon Oct 04 15:44:29 1993 +0100
     2.2 +++ b/src/CCL/type.thy	Mon Oct 04 15:44:54 1993 +0100
     2.3 @@ -35,7 +35,9 @@
     2.4  
     2.5  translations
     2.6    "PROD x:A. B" => "Pi(A, %x. B)"
     2.7 +  "A -> B"      => "Pi(A, _K(B))"
     2.8    "SUM x:A. B"  => "Sigma(A, %x. B)"
     2.9 +  "A * B"       => "Sigma(A, _K(B))"
    2.10    "{x: A. B}"   == "Subtype(A, %x. B)"
    2.11  
    2.12  rules
    2.13 @@ -63,10 +65,6 @@
    2.14  
    2.15  ML
    2.16  
    2.17 -val parse_translation =
    2.18 -  [("@->", ndependent_tr "Pi"),
    2.19 -   ("@*", ndependent_tr "Sigma")];
    2.20 -
    2.21  val print_translation =
    2.22    [("Pi", dependent_tr' ("@Pi", "@->")),
    2.23     ("Sigma", dependent_tr' ("@Sigma", "@*"))];