diff -r 2775062fd3a9 -r 2f4684e2ea95 doc-src/IsarAdvanced/Codegen/codegen_process.ps
--- a/doc-src/IsarAdvanced/Codegen/codegen_process.ps	Mon Mar 02 16:58:39 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,586 +0,0 @@
-%!PS-Adobe-2.0
-%%Creator: dot version 2.2 (Mon Sep 12 23:33:36 UTC 2005)
-%%For: (haftmann) Florian Haftmann
-%%Title: _anonymous_0
-%%Pages: (atend)
-%%BoundingBox: 35 35 451 291
-%%EndComments
-save
-%%BeginProlog
-/DotDict 200 dict def
-DotDict begin
-
-/setupLatin1 {
-mark
-/EncodingVector 256 array def
- EncodingVector 0
-
-ISOLatin1Encoding 0 255 getinterval putinterval
-
-EncodingVector
-  dup 306 /AE
-  dup 301 /Aacute
-  dup 302 /Acircumflex
-  dup 304 /Adieresis
-  dup 300 /Agrave
-  dup 305 /Aring
-  dup 303 /Atilde
-  dup 307 /Ccedilla
-  dup 311 /Eacute
-  dup 312 /Ecircumflex
-  dup 313 /Edieresis
-  dup 310 /Egrave
-  dup 315 /Iacute
-  dup 316 /Icircumflex
-  dup 317 /Idieresis
-  dup 314 /Igrave
-  dup 334 /Udieresis
-  dup 335 /Yacute
-  dup 376 /thorn
-  dup 337 /germandbls
-  dup 341 /aacute
-  dup 342 /acircumflex
-  dup 344 /adieresis
-  dup 346 /ae
-  dup 340 /agrave
-  dup 345 /aring
-  dup 347 /ccedilla
-  dup 351 /eacute
-  dup 352 /ecircumflex
-  dup 353 /edieresis
-  dup 350 /egrave
-  dup 355 /iacute
-  dup 356 /icircumflex
-  dup 357 /idieresis
-  dup 354 /igrave
-  dup 360 /dcroat
-  dup 361 /ntilde
-  dup 363 /oacute
-  dup 364 /ocircumflex
-  dup 366 /odieresis
-  dup 362 /ograve
-  dup 365 /otilde
-  dup 370 /oslash
-  dup 372 /uacute
-  dup 373 /ucircumflex
-  dup 374 /udieresis
-  dup 371 /ugrave
-  dup 375 /yacute
-  dup 377 /ydieresis  
-
-% Set up ISO Latin 1 character encoding
-/starnetISO {
-        dup dup findfont dup length dict begin
-        { 1 index /FID ne { def }{ pop pop } ifelse
-        } forall
-        /Encoding EncodingVector def
-        currentdict end definefont
-} def
-/Times-Roman starnetISO def
-/Times-Italic starnetISO def
-/Times-Bold starnetISO def
-/Times-BoldItalic starnetISO def
-/Helvetica starnetISO def
-/Helvetica-Oblique starnetISO def
-/Helvetica-Bold starnetISO def
-/Helvetica-BoldOblique starnetISO def
-/Courier starnetISO def
-/Courier-Oblique starnetISO def
-/Courier-Bold starnetISO def
-/Courier-BoldOblique starnetISO def
-cleartomark
-} bind def
-
-%%BeginResource: procset graphviz 0 0
-/coord-font-family /Times-Roman def
-/default-font-family /Times-Roman def
-/coordfont coord-font-family findfont 8 scalefont def
-
-/InvScaleFactor 1.0 def
-/set_scale {
-	dup 1 exch div /InvScaleFactor exch def
-	dup scale
-} bind def
-
-% styles
-/solid { [] 0 setdash } bind def
-/dashed { [9 InvScaleFactor mul dup ] 0 setdash } bind def
-/dotted { [1 InvScaleFactor mul 6 InvScaleFactor mul] 0 setdash } bind def
-/invis {/fill {newpath} def /stroke {newpath} def /show {pop newpath} def} bind def
-/bold { 2 setlinewidth } bind def
-/filled { } bind def
-/unfilled { } bind def
-/rounded { } bind def
-/diagonals { } bind def
-
-% hooks for setting color 
-/nodecolor { sethsbcolor } bind def
-/edgecolor { sethsbcolor } bind def
-/graphcolor { sethsbcolor } bind def
-/nopcolor {pop pop pop} bind def
-
-/beginpage {	% i j npages
-	/npages exch def
-	/j exch def
-	/i exch def
-	/str 10 string def
-	npages 1 gt {
-		gsave
-			coordfont setfont
-			0 0 moveto
-			(\() show i str cvs show (,) show j str cvs show (\)) show
-		grestore
-	} if
-} bind def
-
-/set_font {
-	findfont exch
-	scalefont setfont
-} def
-
-% draw aligned label in bounding box aligned to current point
-/alignedtext {			% width adj text
-	/text exch def
-	/adj exch def
-	/width exch def
-	gsave
-		width 0 gt {
-			text stringwidth pop adj mul 0 rmoveto
-		} if
-		[] 0 setdash
-		text show
-	grestore
-} def
-
-/boxprim {				% xcorner ycorner xsize ysize
-		4 2 roll
-		moveto
-		2 copy
-		exch 0 rlineto
-		0 exch rlineto
-		pop neg 0 rlineto
-		closepath
-} bind def
-
-/ellipse_path {
-	/ry exch def
-	/rx exch def
-	/y exch def
-	/x exch def
-	matrix currentmatrix
-	newpath
-	x y translate
-	rx ry scale
-	0 0 1 0 360 arc
-	setmatrix
-} bind def
-
-/endpage { showpage } bind def
-/showpage { } def
-
-/layercolorseq
-	[	% layer color sequence - darkest to lightest
-		[0 0 0]
-		[.2 .8 .8]
-		[.4 .8 .8]
-		[.6 .8 .8]
-		[.8 .8 .8]
-	]
-def
-
-/layerlen layercolorseq length def
-
-/setlayer {/maxlayer exch def /curlayer exch def
-	layercolorseq curlayer 1 sub layerlen mod get
-	aload pop sethsbcolor
-	/nodecolor {nopcolor} def
-	/edgecolor {nopcolor} def
-	/graphcolor {nopcolor} def
-} bind def
-
-/onlayer { curlayer ne {invis} if } def
-
-/onlayers {
-	/myupper exch def
-	/mylower exch def
-	curlayer mylower lt
-	curlayer myupper gt
-	or
-	{invis} if
-} def
-
-/curlayer 0 def
-
-%%EndResource
-%%EndProlog
-%%BeginSetup
-14 default-font-family set_font
-1 setmiterlimit
-% /arrowlength 10 def
-% /arrowwidth 5 def
-
-% make sure pdfmark is harmless for PS-interpreters other than Distiller
-/pdfmark where {pop} {userdict /pdfmark /cleartomark load put} ifelse
-% make '<<' and '>>' safe on PS Level 1 devices
-/languagelevel where {pop languagelevel}{1} ifelse
-2 lt {
-    userdict (<<) cvn ([) cvn load put
-    userdict (>>) cvn ([) cvn load put
-} if
-
-%%EndSetup
-%%Page: 1 1
-%%PageBoundingBox: 36 36 451 291
-%%PageOrientation: Portrait
-gsave
-35 35 416 256 boxprim clip newpath
-36 36 translate
-0 0 1 beginpage
-0 0 translate 0 rotate
-[ /CropBox [36 36 451 291] /PAGES pdfmark
-0.000 0.000 0.000 graphcolor
-14.00 /Times-Roman set_font
-
-%	theory
-gsave 10 dict begin
-newpath 93 254 moveto
-1 254 lineto
-1 214 lineto
-93 214 lineto
-closepath
-stroke
-gsave 10 dict begin
-8 237 moveto
-(Isabelle/HOL)
-[4.56 5.52 6.24 6.96 6.24 3.84 3.84 6.24 3.84 10.08 10.08 8.64]
-xshow
-16 221 moveto
-(Isar theory)
-[4.56 5.52 6.24 4.56 3.6 4.08 6.96 6.24 6.96 4.8 6.96]
-xshow
-end grestore
-end grestore
-
-%	selection
-gsave 10 dict begin
-183 234 38 18 ellipse_path
-stroke
-gsave 10 dict begin
-158 229 moveto
-(selection)
-[5.52 6.24 3.84 6.24 6.24 3.84 3.84 6.96 6.96]
-xshow
-end grestore
-end grestore
-
-%	theory -> selection
-newpath 94 234 moveto
-107 234 121 234 135 234 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 135 238 moveto
-145 234 lineto
-135 231 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 135 238 moveto
-145 234 lineto
-135 231 lineto
-closepath
-stroke
-end grestore
-
-%	sml
-gsave 10 dict begin
-newpath 74 144 moveto
-20 144 lineto
-20 108 lineto
-74 108 lineto
-closepath
-stroke
-gsave 10 dict begin
-32 121 moveto
-(SML)
-[7.68 12.48 8.64]
-xshow
-end grestore
-end grestore
-
-%	other
-gsave 10 dict begin
-gsave 10 dict begin
-41 67 moveto
-(...)
-[3.6 3.6 3.6]
-xshow
-end grestore
-end grestore
-
-%	haskell
-gsave 10 dict begin
-newpath 77 36 moveto
-17 36 lineto
-17 0 lineto
-77 0 lineto
-closepath
-stroke
-gsave 10 dict begin
-25 13 moveto
-(Haskell)
-[10.08 6.24 5.52 6.72 6.24 3.84 3.84]
-xshow
-end grestore
-end grestore
-
-%	preprocessing
-gsave 10 dict begin
-183 180 52 18 ellipse_path
-stroke
-gsave 10 dict begin
-143 175 moveto
-(preprocessing)
-[6.96 4.56 6.24 6.96 4.56 6.96 6.24 6.24 5.52 5.52 3.84 6.96 6.96]
-xshow
-end grestore
-end grestore
-
-%	selection -> preprocessing
-newpath 183 216 moveto
-183 213 183 211 183 208 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 187 208 moveto
-183 198 lineto
-180 208 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 187 208 moveto
-183 198 lineto
-180 208 lineto
-closepath
-stroke
-end grestore
-
-%	def_eqn
-gsave 10 dict begin
-newpath 403 198 moveto
-283 198 lineto
-283 162 lineto
-403 162 lineto
-closepath
-stroke
-gsave 10 dict begin
-291 175 moveto
-(defining equations)
-[6.96 6.24 4.8 3.84 6.96 3.84 6.96 6.96 3.6 6.24 6.72 6.96 6.24 3.84 3.84 6.96 6.96 5.52]
-xshow
-end grestore
-end grestore
-
-%	preprocessing -> def_eqn
-newpath 236 180 moveto
-248 180 260 180 273 180 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 273 184 moveto
-283 180 lineto
-273 177 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 273 184 moveto
-283 180 lineto
-273 177 lineto
-closepath
-stroke
-end grestore
-
-%	serialization
-gsave 10 dict begin
-183 72 47 18 ellipse_path
-stroke
-gsave 10 dict begin
-148 67 moveto
-(serialization)
-[5.52 6.24 4.8 3.84 6.24 3.84 3.84 6.24 6.24 3.84 3.84 6.96 6.96]
-xshow
-end grestore
-end grestore
-
-%	serialization -> sml
-newpath 150 85 moveto
-129 93 104 103 83 111 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 82 108 moveto
-74 115 lineto
-85 114 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 82 108 moveto
-74 115 lineto
-85 114 lineto
-closepath
-stroke
-end grestore
-
-%	serialization -> other
-gsave 10 dict begin
-dotted
-newpath 135 72 moveto
-119 72 100 72 84 72 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 84 69 moveto
-74 72 lineto
-84 76 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 84 69 moveto
-74 72 lineto
-84 76 lineto
-closepath
-stroke
-end grestore
-end grestore
-
-%	serialization -> haskell
-newpath 150 59 moveto
-131 51 107 42 86 34 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 88 31 moveto
-77 30 lineto
-85 37 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 88 31 moveto
-77 30 lineto
-85 37 lineto
-closepath
-stroke
-end grestore
-
-%	translation
-gsave 10 dict begin
-343 126 43 18 ellipse_path
-stroke
-gsave 10 dict begin
-313 121 moveto
-(translation)
-[3.84 4.56 6.24 6.96 5.52 3.84 6.24 3.84 3.84 6.96 6.96]
-xshow
-end grestore
-end grestore
-
-%	def_eqn -> translation
-newpath 343 162 moveto
-343 159 343 157 343 154 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 347 154 moveto
-343 144 lineto
-340 154 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 347 154 moveto
-343 144 lineto
-340 154 lineto
-closepath
-stroke
-end grestore
-
-%	iml
-gsave 10 dict begin
-newpath 413 90 moveto
-273 90 lineto
-273 54 lineto
-413 54 lineto
-closepath
-stroke
-gsave 10 dict begin
-280 67 moveto
-(intermediate language)
-[3.84 6.96 3.84 6.24 4.8 10.8 6.24 6.96 3.84 6.24 3.84 6.24 3.6 3.84 6.24 6.96 6.96 6.96 6.24 6.72 6.24]
-xshow
-end grestore
-end grestore
-
-%	translation -> iml
-newpath 343 108 moveto
-343 105 343 103 343 100 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 347 100 moveto
-343 90 lineto
-340 100 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 347 100 moveto
-343 90 lineto
-340 100 lineto
-closepath
-stroke
-end grestore
-
-%	iml -> serialization
-newpath 272 72 moveto
-262 72 251 72 241 72 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 241 69 moveto
-231 72 lineto
-241 76 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 241 69 moveto
-231 72 lineto
-241 76 lineto
-closepath
-stroke
-end grestore
-endpage
-showpage
-grestore
-%%PageTrailer
-%%EndPage: 1
-%%Trailer
-%%Pages: 1
-end
-restore
-%%EOF