--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy Wed Feb 21 12:57:49 2018 +0000
+++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy Thu Feb 22 18:01:08 2018 +0100
@@ -20,9 +20,19 @@
declare vec_lambda_inject [simplified, simp]
+bundle vec_syntax begin
notation
vec_nth (infixl "$" 90) and
vec_lambda (binder "\<chi>" 10)
+end
+
+bundle no_vec_syntax begin
+no_notation
+ vec_nth (infixl "$" 90) and
+ vec_lambda (binder "\<chi>" 10)
+end
+
+unbundle vec_syntax
(*
Translate "'b ^ 'n" into "'b ^ ('n :: finite)". When 'n has already more than