guillemot syntax;
authorwenzelm
Wed Oct 17 20:25:51 2001 +0200 (2001-10-17)
changeset 118235a3fcd84e55e
parent 11822 122834177ec1
child 11824 f4c1882dde2c
guillemot syntax;
src/HOL/ex/Multiquote.thy
src/HOL/ex/document/root.tex
     1.1 --- a/src/HOL/ex/Multiquote.thy	Wed Oct 17 20:25:19 2001 +0200
     1.2 +++ b/src/HOL/ex/Multiquote.thy	Wed Oct 17 20:25:51 2001 +0200
     1.3 @@ -14,7 +14,7 @@
     1.4  *}
     1.5  
     1.6  syntax
     1.7 -  "_quote" :: "'b => ('a => 'b)"	     (".'(_')." [0] 1000)
     1.8 +  "_quote" :: "'b => ('a => 'b)"	     ("\<guillemotleft>_\<guillemotright>" [0] 1000)
     1.9    "_antiquote" :: "('a => 'b) => 'b"         ("\<acute>_" [1000] 1000)
    1.10  
    1.11  parse_translation {*
    1.12 @@ -36,15 +36,15 @@
    1.13  *}
    1.14  
    1.15  text {* basic examples *}
    1.16 -term ".(a + b + c)."
    1.17 -term ".(a + b + c + \<acute>x + \<acute>y + 1)."
    1.18 -term ".(\<acute>(f w) + \<acute>x)."
    1.19 -term ".(f \<acute>x \<acute>y z)."
    1.20 +term "\<guillemotleft>a + b + c\<guillemotright>"
    1.21 +term "\<guillemotleft>a + b + c + \<acute>x + \<acute>y + 1\<guillemotright>"
    1.22 +term "\<guillemotleft>\<acute>(f w) + \<acute>x\<guillemotright>"
    1.23 +term "\<guillemotleft>f \<acute>x \<acute>y z\<guillemotright>"
    1.24  
    1.25  text {* advanced examples *}
    1.26 -term ".(.(\<acute>\<acute>x + \<acute>y).)."
    1.27 -term ".(.(\<acute>\<acute>x + \<acute>y). \<circ> \<acute>f)."
    1.28 -term ".(\<acute>(f \<circ> \<acute>g))."
    1.29 -term ".(.( \<acute>\<acute>(f \<circ> \<acute>g) ).)."
    1.30 +term "\<guillemotleft>\<guillemotleft>\<acute>\<acute>x + \<acute>y\<guillemotright>\<guillemotright>"
    1.31 +term "\<guillemotleft>\<guillemotleft>\<acute>\<acute>x + \<acute>y\<guillemotright> o \<acute>f\<guillemotright>"
    1.32 +term "\<guillemotleft>\<acute>(f o \<acute>g)\<guillemotright>"
    1.33 +term "\<guillemotleft>\<guillemotleft>\<acute>\<acute>(f o \<acute>g)\<guillemotright>\<guillemotright>"
    1.34  
    1.35  end
     2.1 --- a/src/HOL/ex/document/root.tex	Wed Oct 17 20:25:19 2001 +0200
     2.2 +++ b/src/HOL/ex/document/root.tex	Wed Oct 17 20:25:51 2001 +0200
     2.3 @@ -3,6 +3,7 @@
     2.4  
     2.5  \documentclass[11pt,a4paper]{article}
     2.6  \usepackage{isabelle,isabellesym,pdfsetup}
     2.7 +\usepackage[english]{babel}
     2.8  
     2.9  \urlstyle{rm}
    2.10  \isabellestyle{it}