# HG changeset patch
# User hoelzl
# Date 1278487614 -7200
# Node ID 243ea7885e055a9ec7464cfce8801135bf84794b
# Parent  2bf3a2cb5e58244297353d97c9b1e2edbb382726
tuned

diff -r 2bf3a2cb5e58 -r 243ea7885e05 src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Wed Jul 07 08:25:23 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Wed Jul 07 09:26:54 2010 +0200
@@ -3315,8 +3315,6 @@
 apply simp
 done
 
-print_antiquotations
-
 subsection "Instantiate @{typ real} and @{typ complex} as typeclass @{text ordered_euclidean_space}."
 
 instantiation real :: real_basis_with_inner