--- 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