diff -r ab23925c64d6 -r c5039bee2602 doc-src/IsarAdvanced/Codegen/codegen_process.ps
--- a/doc-src/IsarAdvanced/Codegen/codegen_process.ps	Thu Mar 29 14:21:47 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/codegen_process.ps	Fri Mar 30 16:18:59 2007 +0200
@@ -1,5 +1,5 @@
 %!PS-Adobe-2.0
-%%Creator: dot version 2.2 (Tue Mar 22 18:02:44 UTC 2005)
+%%Creator: dot version 2.2 (Mon Sep 12 23:33:36 UTC 2005)
 %%For: (haftmann) Florian Haftmann
 %%Title: _anonymous_0
 %%Pages: (atend)
@@ -369,39 +369,39 @@
 stroke
 end grestore
 
-%	code_thm
+%	def_eqn
 gsave 10 dict begin
-newpath 392 198 moveto
-294 198 lineto
-294 162 lineto
-392 162 lineto
+newpath 403 198 moveto
+283 198 lineto
+283 162 lineto
+403 162 lineto
 closepath
 stroke
 gsave 10 dict begin
-302 175 moveto
-(code theorems)
-[6.24 6.96 6.96 6.24 3.6 4.08 6.96 6.24 6.96 4.56 6.24 10.8 5.52]
+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 -> code_thm
+%	preprocessing -> def_eqn
 newpath 236 180 moveto
-252 180 268 180 284 180 curveto
+248 180 260 180 273 180 curveto
 stroke
 gsave 10 dict begin
 solid
 1 setlinewidth
 0.000 0.000 0.000 edgecolor
-newpath 284 184 moveto
-294 180 lineto
-284 177 lineto
+newpath 273 184 moveto
+283 180 lineto
+273 177 lineto
 closepath
 fill
 0.000 0.000 0.000 edgecolor
-newpath 284 184 moveto
-294 180 lineto
-284 177 lineto
+newpath 273 184 moveto
+283 180 lineto
+273 177 lineto
 closepath
 stroke
 end grestore
@@ -484,19 +484,19 @@
 stroke
 end grestore
 
-%	extraction
+%	translation
 gsave 10 dict begin
-343 126 41 18 ellipse_path
+343 126 43 18 ellipse_path
 stroke
 gsave 10 dict begin
-315 121 moveto
-(extraction)
-[5.76 6.96 3.84 4.56 6.24 6.24 3.84 3.84 6.96 6.96]
+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
 
-%	code_thm -> extraction
+%	def_eqn -> translation
 newpath 343 162 moveto
 343 159 343 157 343 154 curveto
 stroke
@@ -533,7 +533,7 @@
 end grestore
 end grestore
 
-%	extraction -> iml
+%	translation -> iml
 newpath 343 108 moveto
 343 105 343 103 343 100 curveto
 stroke