# HG changeset patch
# User wenzelm
# Date 1003343151 -7200
# Node ID 5a3fcd84e55ef3b16f04d6aef5d9e9b5dfcca5fa
# Parent  122834177ec1a329010f8adfdd5ffdf5bab28eed
guillemot syntax;

diff -r 122834177ec1 -r 5a3fcd84e55e src/HOL/ex/Multiquote.thy
--- 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
diff -r 122834177ec1 -r 5a3fcd84e55e src/HOL/ex/document/root.tex
--- 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}