guillemot syntax;

--- a/src/HOL/ex/Multiquote.thy	Wed Oct 17 20:25:19 2001 +0200
+++ b/src/HOL/ex/Multiquote.thy	Wed Oct 17 20:25:51 2001 +0200
@@ -14,7 +14,7 @@
 *}
 
 syntax
-  "_quote" :: "'b => ('a => 'b)"	     (".'(_')." [0] 1000)
+  "_quote" :: "'b => ('a => 'b)"	     ("\<guillemotleft>_\<guillemotright>" [0] 1000)
   "_antiquote" :: "('a => 'b) => 'b"         ("\<acute>_" [1000] 1000)
 
 parse_translation {*
@@ -36,15 +36,15 @@
 *}
 
 text {* basic examples *}
-term ".(a + b + c)."
-term ".(a + b + c + \<acute>x + \<acute>y + 1)."
-term ".(\<acute>(f w) + \<acute>x)."
-term ".(f \<acute>x \<acute>y z)."
+term "\<guillemotleft>a + b + c\<guillemotright>"
+term "\<guillemotleft>a + b + c + \<acute>x + \<acute>y + 1\<guillemotright>"
+term "\<guillemotleft>\<acute>(f w) + \<acute>x\<guillemotright>"
+term "\<guillemotleft>f \<acute>x \<acute>y z\<guillemotright>"
 
 text {* advanced examples *}
-term ".(.(\<acute>\<acute>x + \<acute>y).)."
-term ".(.(\<acute>\<acute>x + \<acute>y). \<circ> \<acute>f)."
-term ".(\<acute>(f \<circ> \<acute>g))."
-term ".(.( \<acute>\<acute>(f \<circ> \<acute>g) ).)."
+term "\<guillemotleft>\<guillemotleft>\<acute>\<acute>x + \<acute>y\<guillemotright>\<guillemotright>"
+term "\<guillemotleft>\<guillemotleft>\<acute>\<acute>x + \<acute>y\<guillemotright> o \<acute>f\<guillemotright>"
+term "\<guillemotleft>\<acute>(f o \<acute>g)\<guillemotright>"
+term "\<guillemotleft>\<guillemotleft>\<acute>\<acute>(f o \<acute>g)\<guillemotright>\<guillemotright>"
 
 end

--- a/src/HOL/ex/document/root.tex	Wed Oct 17 20:25:19 2001 +0200
+++ b/src/HOL/ex/document/root.tex	Wed Oct 17 20:25:51 2001 +0200
@@ -3,6 +3,7 @@
 
 \documentclass[11pt,a4paper]{article}
 \usepackage{isabelle,isabellesym,pdfsetup}
+\usepackage[english]{babel}
 
 \urlstyle{rm}
 \isabellestyle{it}