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:49:49 +0100
changeset 23 1cd377c2f7c6
parent 22 41dc6b189412
child 24 f3d4ff75d9f2
replaced id by idt; added parse rules for --> and *; removed ndependent_tr;
src/CTT/CTT.thy file | annotate | diff | comparison | revisions
src/CTT/ctt.thy file | annotate | diff | comparison | revisions 
--- a/src/CTT/CTT.thy	Mon Oct 04 15:44:54 1993 +0100
+++ b/src/CTT/CTT.thy	Mon Oct 04 15:49:49 1993 +0100
@@ -40,8 +40,8 @@
   Eqelem    :: "[i,i,t]=>prop"      ("(3_ =/ _ :/ _)" [10,10,10] 5)
   Reduce    :: "[i,i]=>prop"        ("Reduce[_,_]")
   (*Types*)
-  "@PROD"   :: "[id,t,t]=>t"        ("(3PROD _:_./ _)" 10)
-  "@SUM"    :: "[id,t,t]=>t"        ("(3SUM _:_./ _)" 10)
+  "@PROD"   :: "[idt,t,t]=>t"       ("(3PROD _:_./ _)" 10)
+  "@SUM"    :: "[idt,t,t]=>t"       ("(3SUM _:_./ _)" 10)
   "+"       :: "[t,t]=>t"           (infixr 40)
   (*Invisible infixes!*)
   "@-->"    :: "[t,t]=>t"           ("(_ -->/ _)" [31,30] 30)
@@ -56,7 +56,9 @@
 
 translations
   "PROD x:A. B" => "Prod(A, %x. B)"
+  "A --> B"     => "Prod(A, _K(B))"
   "SUM x:A. B"  => "Sum(A, %x. B)"
+  "A * B"       => "Sum(A, _K(B))"
 
 rules
 
@@ -244,9 +246,6 @@
 
 ML
 
-val parse_translation =
-  [("@-->", ndependent_tr "Prod"), ("@*", ndependent_tr "Sum")];
-
 val print_translation =
   [("Prod", dependent_tr' ("@PROD", "@-->")),
    ("Sum", dependent_tr' ("@SUM", "@*"))];
--- a/src/CTT/ctt.thy	Mon Oct 04 15:44:54 1993 +0100
+++ b/src/CTT/ctt.thy	Mon Oct 04 15:49:49 1993 +0100
@@ -40,8 +40,8 @@
   Eqelem    :: "[i,i,t]=>prop"      ("(3_ =/ _ :/ _)" [10,10,10] 5)
   Reduce    :: "[i,i]=>prop"        ("Reduce[_,_]")
   (*Types*)
-  "@PROD"   :: "[id,t,t]=>t"        ("(3PROD _:_./ _)" 10)
-  "@SUM"    :: "[id,t,t]=>t"        ("(3SUM _:_./ _)" 10)
+  "@PROD"   :: "[idt,t,t]=>t"       ("(3PROD _:_./ _)" 10)
+  "@SUM"    :: "[idt,t,t]=>t"       ("(3SUM _:_./ _)" 10)
   "+"       :: "[t,t]=>t"           (infixr 40)
   (*Invisible infixes!*)
   "@-->"    :: "[t,t]=>t"           ("(_ -->/ _)" [31,30] 30)
@@ -56,7 +56,9 @@
 
 translations
   "PROD x:A. B" => "Prod(A, %x. B)"
+  "A --> B"     => "Prod(A, _K(B))"
   "SUM x:A. B"  => "Sum(A, %x. B)"
+  "A * B"       => "Sum(A, _K(B))"
 
 rules
 
@@ -244,9 +246,6 @@
 
 ML
 
-val parse_translation =
-  [("@-->", ndependent_tr "Prod"), ("@*", ndependent_tr "Sum")];
-
 val print_translation =
   [("Prod", dependent_tr' ("@PROD", "@-->")),
    ("Sum", dependent_tr' ("@SUM", "@*"))];
isabelle