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.
more explicit infixl (see initial 1edf0f223c6e);
authorwenzelm
Wed, 28 Feb 2018 16:30:25 +0100
changeset 67732 39d80006fc29
parent 67731 184c293f0a33
child 67734 7b0b0a02b303
more explicit infixl (see initial 1edf0f223c6e); clarified name;
src/HOL/Analysis/Finite_Cartesian_Product.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy	Wed Feb 28 13:37:33 2018 +0100
+++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy	Wed Feb 28 16:30:25 2018 +0100
@@ -39,7 +39,7 @@
     \<^item> \<open>'a^'b\<close> becomes \<open>('a, 'b::finite) vec\<close>
     \<^item> \<open>'a^'b::_\<close> becomes \<open>('a, 'b) vec\<close> without extra sort-constraint
 \<close>
-syntax "_finite_vec" :: "type \<Rightarrow> type \<Rightarrow> type" ("(_ ^/ _)" [15, 16] 15)
+syntax "_vec_type" :: "type \<Rightarrow> type \<Rightarrow> type" (infixl "^" 15)
 parse_translation \<open>
   let
     fun vec t u = Syntax.const @{type_syntax vec} $ t $ u;
@@ -52,7 +52,7 @@
           else vec t u
       | _ => vec t u)
   in
-    [(@{syntax_const "_finite_vec"}, K finite_vec_tr)]
+    [(@{syntax_const "_vec_type"}, K finite_vec_tr)]
   end
 \<close>
isabelle