(continued)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/arbitrary.ML	Mon Nov 06 16:28:30 2006 +0100
@@ -0,0 +1,14 @@
+structure ROOT = 
+struct
+
+structure Codegen = 
+struct
+
+val arbitrary_option : 'a option = NONE;
+
+fun dummy_option [] = arbitrary_option
+  | dummy_option (x :: xs) = SOME x;
+
+end; (*struct Codegen*)
+
+end; (*struct ROOT*)

--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/bool3.ML	Mon Nov 06 16:28:29 2006 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool3.ML	Mon Nov 06 16:28:30 2006 +0100
@@ -9,24 +9,23 @@
 
 end; (*struct HOL*)
 
-structure IntDef = 
+structure Nat = 
 struct
 
-datatype nat = Zero_nat | Succ_nat of nat;
+datatype nat = Zero_nat | Suc of nat;
 
-fun less_nat Zero_nat (Succ_nat n) = true
+fun less_nat Zero_nat (Suc n) = true
   | less_nat n Zero_nat = false
-  | less_nat (Succ_nat m) (Succ_nat n) = less_nat m n;
+  | less_nat (Suc m) (Suc n) = less_nat m n;
 
 fun less_eq_nat m n = HOL.nota (less_nat n m);
 
-end; (*struct IntDef*)
+end; (*struct Nat*)
 
 structure Codegen = 
 struct
 
-fun in_interval (k, l) n =
-  IntDef.less_eq_nat k n andalso IntDef.less_eq_nat n l;
+fun in_interval (k, l) n = Nat.less_eq_nat k n andalso Nat.less_eq_nat n l;
 
 end; (*struct Codegen*)
 

--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML	Mon Nov 06 16:28:29 2006 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML	Mon Nov 06 16:28:30 2006 +0100
@@ -1,28 +1,28 @@
 structure ROOT = 
 struct
 
-structure IntDef = 
+structure Nat = 
 struct
 
-datatype nat = Zero_nat | Succ_nat of nat;
+datatype nat = Zero_nat | Suc of nat;
 
-end; (*struct IntDef*)
+end; (*struct Nat*)
 
 structure Codegen = 
 struct
 
 type 'a null = {null_ : 'a};
-fun Null (A_:'a null) = #null_ A_;
+fun null (A_:'a null) = #null_ A_;
 
 fun head (A_1_:'a_1 null) (y :: xs) = y
-  | head (A_1_:'a_1 null) [] = Null A_1_;
+  | head (A_1_:'a_1 null) [] = null A_1_;
 
 val null_option : 'b option = NONE;
 
 fun null_optiona () = {null_ = null_option} : ('b option) null
 
-val dummy : IntDef.nat option =
-  head (null_optiona ()) [SOME (IntDef.Succ_nat IntDef.Zero_nat), NONE];
+val dummy : Nat.nat option =
+  head (null_optiona ()) [SOME (Nat.Suc Nat.Zero_nat), NONE];
 
 end; (*struct Codegen*)
 

--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML	Mon Nov 06 16:28:29 2006 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML	Mon Nov 06 16:28:30 2006 +0100
@@ -5,14 +5,14 @@
 struct
 
 type 'a eq = {eq_ : 'a -> 'a -> bool};
-fun Eq (A_:'a eq) = #eq_ A_;
+fun eq (A_:'a eq) = #eq_ A_;
 
 end; (*struct Code_Generator*)
 
 structure HOL = 
 struct
 
-fun op_eq (A_:'a Code_Generator.eq) a b = Code_Generator.Eq A_ a b;
+fun op_eq (A_:'a Code_Generator.eq) a b = Code_Generator.eq A_ a b;
 
 end; (*struct HOL*)
 

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/dirty_set.ML	Mon Nov 06 16:28:30 2006 +0100
@@ -0,0 +1,22 @@
+structure ROOT = 
+struct
+
+structure Nat = 
+struct
+
+datatype nat = Zero_nat | Suc of nat;
+
+end; (*struct Nat*)
+
+structure Codegen = 
+struct
+
+val dummy_set : Nat.nat -> Nat.nat list = Nat.Suc :: [];
+
+val foobar_set : Nat.nat list =
+  Nat.Zero_nat ::
+    (Nat.Suc Nat.Zero_nat :: (Nat.Suc (Nat.Suc Nat.Zero_nat) :: []));
+
+end; (*struct Codegen*)
+
+end; (*struct ROOT*)

--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/fac.ML	Mon Nov 06 16:28:29 2006 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/fac.ML	Mon Nov 06 16:28:30 2006 +0100
@@ -1,24 +1,24 @@
 structure ROOT = 
 struct
 
-structure IntDef = 
+structure Nat = 
 struct
 
-datatype nat = Zero_nat | Succ_nat of nat;
+datatype nat = Zero_nat | Suc of nat;
 
-fun plus_nat (Succ_nat m) n = plus_nat m (Succ_nat n)
+fun plus_nat (Suc m) n = plus_nat m (Suc n)
   | plus_nat Zero_nat y = y;
 
-fun times_nat (Succ_nat m) n = plus_nat n (times_nat m n)
+fun times_nat (Suc m) n = plus_nat n (times_nat m n)
   | times_nat Zero_nat n = Zero_nat;
 
-end; (*struct IntDef*)
+end; (*struct Nat*)
 
 structure Codegen = 
 struct
 
-fun fac (IntDef.Succ_nat n) = IntDef.times_nat (IntDef.Succ_nat n) (fac n)
-  | fac IntDef.Zero_nat = IntDef.Succ_nat IntDef.Zero_nat;
+fun fac (Nat.Suc n) = Nat.times_nat (Nat.Suc n) (fac n)
+  | fac Nat.Zero_nat = Nat.Suc Nat.Zero_nat;
 
 end; (*struct Codegen*)
 

--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML	Mon Nov 06 16:28:29 2006 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML	Mon Nov 06 16:28:30 2006 +0100
@@ -1,25 +1,25 @@
 structure ROOT = 
 struct
 
-structure IntDef = 
+structure Nat = 
 struct
 
-datatype nat = Zero_nat | Succ_nat of nat;
+datatype nat = Zero_nat | Suc of nat;
 
-fun plus_nat (Succ_nat m) n = plus_nat m (Succ_nat n)
+fun plus_nat (Suc m) n = plus_nat m (Suc n)
   | plus_nat Zero_nat y = y;
 
-fun times_nat (Succ_nat m) n = plus_nat n (times_nat m n)
+fun times_nat (Suc m) n = plus_nat n (times_nat m n)
   | times_nat Zero_nat n = Zero_nat;
 
-end; (*struct IntDef*)
+end; (*struct Nat*)
 
 structure Codegen = 
 struct
 
 fun fac n =
-  (case n of IntDef.Zero_nat => IntDef.Succ_nat IntDef.Zero_nat
-     | IntDef.Succ_nat ma => IntDef.times_nat n (fac ma));
+  (case n of Nat.Zero_nat => Nat.Suc Nat.Zero_nat
+     | Nat.Suc ma => Nat.times_nat n (fac ma));
 
 end; (*struct Codegen*)
 

--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML	Mon Nov 06 16:28:29 2006 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML	Mon Nov 06 16:28:30 2006 +0100
@@ -5,7 +5,7 @@
 struct
 
 type 'a eq = {eq_ : 'a -> 'a -> bool};
-fun Eq (A_:'a eq) = #eq_ A_;
+fun eq (A_:'a eq) = #eq_ A_;
 
 end; (*struct Code_Generator*)
 
@@ -13,38 +13,37 @@
 struct
 
 fun eq_prod (A_:'a Code_Generator.eq) (B_:'b Code_Generator.eq) (x1, y1)
-  (x2, y2) = Code_Generator.Eq A_ x1 x2 andalso Code_Generator.Eq B_ y1 y2;
+  (x2, y2) = Code_Generator.eq A_ x1 x2 andalso Code_Generator.eq B_ y1 y2;
 
 end; (*struct Product_Type*)
 
 structure Orderings = 
 struct
 
-type 'a ord =
-  {Code_Generator__eq : 'a Code_Generator.eq, less_eq_ : 'a -> 'a -> bool,
-    less_ : 'a -> 'a -> bool};
-fun Less_eq (A_:'a ord) = #less_eq_ A_;
-fun Less (A_:'a ord) = #less_ A_;
+type 'a ord = {less_eq_ : 'a -> 'a -> bool, less_ : 'a -> 'a -> bool};
+fun less_eq (A_:'a ord) = #less_eq_ A_;
+fun less (A_:'a ord) = #less_ A_;
 
 end; (*struct Orderings*)
 
 structure Codegen = 
 struct
 
-fun less_prod (B_:'b Orderings.ord) (C_:'c Orderings.ord) p1 p2 =
+fun less_prod (B_:'b Code_Generator.eq * 'b Orderings.ord)
+  (C_:'c Code_Generator.eq * 'c Orderings.ord) p1 p2 =
   let
     val (x1a, y1a) = p1;
     val (x2a, y2a) = p2;
   in
-    Orderings.Less B_ x1a x2a orelse
-      Code_Generator.Eq (#Code_Generator__eq B_) x1a x2a andalso
-        Orderings.Less C_ y1a y2a
+    Orderings.less (#2 B_) x1a x2a orelse
+      Code_Generator.eq (#1 B_) x1a x2a andalso
+        Orderings.less (#2 C_) y1a y2a
   end;
 
-fun less_eq_prod (B_:'b Orderings.ord) (C_:'c Orderings.ord) p1 p2 =
-  less_prod B_ C_ p1 p2 orelse
-    Product_Type.eq_prod (#Code_Generator__eq B_) (#Code_Generator__eq C_)
-      p1 p2;
+fun less_eq_prod (B_:'b Code_Generator.eq * 'b Orderings.ord)
+  (C_:'c Code_Generator.eq * 'c Orderings.ord) p1 p2 =
+  less_prod ((#1 B_), (#2 B_)) ((#1 C_), (#2 C_)) p1 p2 orelse
+    Product_Type.eq_prod (#1 B_) (#1 C_) p1 p2;
 
 end; (*struct Codegen*)
 

--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML	Mon Nov 06 16:28:29 2006 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML	Mon Nov 06 16:28:30 2006 +0100
@@ -1,31 +1,31 @@
 structure ROOT = 
 struct
 
-structure IntDef = 
+structure Nat = 
 struct
 
-datatype nat = Zero_nat | Succ_nat of nat;
+datatype nat = Zero_nat | Suc of nat;
 
-fun less_nat Zero_nat (Succ_nat n) = true
+fun less_nat Zero_nat (Suc n) = true
   | less_nat n Zero_nat = false
-  | less_nat (Succ_nat m) (Succ_nat n) = less_nat m n;
+  | less_nat (Suc m) (Suc n) = less_nat m n;
 
-fun minus_nat (Succ_nat m) (Succ_nat n) = minus_nat m n
+fun minus_nat (Suc m) (Suc n) = minus_nat m n
   | minus_nat Zero_nat n = Zero_nat
   | minus_nat y Zero_nat = y;
 
-end; (*struct IntDef*)
+end; (*struct Nat*)
 
 structure Codegen = 
 struct
 
 fun pick ((k, v) :: xs) n =
-  (if IntDef.less_nat n k then v else pick xs (IntDef.minus_nat n k))
+  (if Nat.less_nat n k then v else pick xs (Nat.minus_nat n k))
   | pick (x :: xs) n =
     let
       val (ka, va) = x;
     in
-      (if IntDef.less_nat n ka then va else pick xs (IntDef.minus_nat n ka))
+      (if Nat.less_nat n ka then va else pick xs (Nat.minus_nat n ka))
     end;
 
 end; (*struct Codegen*)

--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/pick2.ML	Mon Nov 06 16:28:29 2006 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/pick2.ML	Mon Nov 06 16:28:30 2006 +0100
@@ -1,26 +1,26 @@
 structure ROOT = 
 struct
 
-structure IntDef = 
+structure Nat = 
 struct
 
-datatype nat = Zero_nat | Succ_nat of nat;
+datatype nat = Zero_nat | Suc of nat;
 
-fun less_nat Zero_nat (Succ_nat n) = true
+fun less_nat Zero_nat (Suc n) = true
   | less_nat n Zero_nat = false
-  | less_nat (Succ_nat m) (Succ_nat n) = less_nat m n;
+  | less_nat (Suc m) (Suc n) = less_nat m n;
 
-fun minus_nat (Succ_nat m) (Succ_nat n) = minus_nat m n
+fun minus_nat (Suc m) (Suc n) = minus_nat m n
   | minus_nat Zero_nat n = Zero_nat
   | minus_nat y Zero_nat = y;
 
-end; (*struct IntDef*)
+end; (*struct Nat*)
 
 structure Codegen = 
 struct
 
 fun pick ((k, v) :: xs) n =
-  (if IntDef.less_nat n k then v else pick xs (IntDef.minus_nat n k));
+  (if Nat.less_nat n k then v else pick xs (Nat.minus_nat n k));
 
 end; (*struct Codegen*)
 

--- a/doc-src/IsarAdvanced/Codegen/codegen.tex	Mon Nov 06 16:28:29 2006 +0100
+++ b/doc-src/IsarAdvanced/Codegen/codegen.tex	Mon Nov 06 16:28:30 2006 +0100
@@ -40,6 +40,8 @@
 \newcommand{\isasymCODERESERVED}{\cmd{code\_reserved}}
 \newcommand{\isasymCODEMODULENAME}{\cmd{code\_modulename}}
 \newcommand{\isasymCODEMODULEPROLOG}{\cmd{code\_moduleprolog}}
+\newcommand{\isasymCODEAXIOMS}{\cmd{code\_axioms}}
+\newcommand{\isasymCODEABSTYPE}{\cmd{code\_abstype}}
 \newcommand{\isasymPRINTCODETHMS}{\cmd{print\_codethms}}
 \newcommand{\isasymFUN}{\cmd{fun}}
 \newcommand{\isasymFUNCTION}{\cmd{function}}

--- a/doc-src/IsarAdvanced/Codegen/codegen_process.eps	Mon Nov 06 16:28:29 2006 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,582 +0,0 @@
-%!PS-Adobe-2.0
-%%Creator: dot version 2.2 (Tue Mar 22 18:02:44 UTC 2005)
-%%For: (haftmann) Florian Haftmann
-%%Title: _anonymous_0
-%%Pages: (atend)
-%%BoundingBox: 35 35 241 577
-%%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 241 577
-%%PageOrientation: Portrait
-gsave
-35 35 206 542 boxprim clip newpath
-36 36 translate
-0 0 1 beginpage
-0 0 translate 0 rotate
-[ /CropBox [36 36 241 577] /PAGES pdfmark
-0.000 0.000 0.000 graphcolor
-14.00 /Times-Roman set_font
-
-%	theory
-gsave 10 dict begin
-newpath 126 540 moveto
-72 540 lineto
-72 504 lineto
-126 504 lineto
-closepath
-stroke
-gsave 10 dict begin
-80 517 moveto
-(theory)
-[4.08 6.96 6.24 6.96 4.8 6.96]
-xshow
-end grestore
-end grestore
-
-%	selection
-gsave 10 dict begin
-99 450 38 18 ellipse_path
-stroke
-gsave 10 dict begin
-74 445 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 99 504 moveto
-99 496 99 487 99 478 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 103 478 moveto
-99 468 lineto
-96 478 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 103 478 moveto
-99 468 lineto
-96 478 lineto
-closepath
-stroke
-end grestore
-
-%	preprocessing
-gsave 10 dict begin
-99 378 52 18 ellipse_path
-stroke
-gsave 10 dict begin
-59 373 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 99 432 moveto
-99 424 99 415 99 406 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 103 406 moveto
-99 396 lineto
-96 406 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 103 406 moveto
-99 396 lineto
-96 406 lineto
-closepath
-stroke
-end grestore
-
-%	code_thm
-gsave 10 dict begin
-newpath 148 324 moveto
-50 324 lineto
-50 288 lineto
-148 288 lineto
-closepath
-stroke
-gsave 10 dict begin
-58 301 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]
-xshow
-end grestore
-end grestore
-
-%	preprocessing -> code_thm
-newpath 99 360 moveto
-99 352 99 343 99 334 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 103 334 moveto
-99 324 lineto
-96 334 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 103 334 moveto
-99 324 lineto
-96 334 lineto
-closepath
-stroke
-end grestore
-
-%	extraction
-gsave 10 dict begin
-99 234 41 18 ellipse_path
-stroke
-gsave 10 dict begin
-71 229 moveto
-(extraction)
-[5.76 6.96 3.84 4.56 6.24 6.24 3.84 3.84 6.96 6.96]
-xshow
-end grestore
-end grestore
-
-%	code_thm -> extraction
-newpath 99 288 moveto
-99 280 99 271 99 262 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 103 262 moveto
-99 252 lineto
-96 262 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 103 262 moveto
-99 252 lineto
-96 262 lineto
-closepath
-stroke
-end grestore
-
-%	iml
-gsave 10 dict begin
-newpath 169 180 moveto
-29 180 lineto
-29 144 lineto
-169 144 lineto
-closepath
-stroke
-gsave 10 dict begin
-36 157 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
-
-%	extraction -> iml
-newpath 99 216 moveto
-99 208 99 199 99 190 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 103 190 moveto
-99 180 lineto
-96 190 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 103 190 moveto
-99 180 lineto
-96 190 lineto
-closepath
-stroke
-end grestore
-
-%	serialization
-gsave 10 dict begin
-99 90 47 18 ellipse_path
-stroke
-gsave 10 dict begin
-64 85 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
-
-%	iml -> serialization
-newpath 99 144 moveto
-99 136 99 127 99 118 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 103 118 moveto
-99 108 lineto
-96 118 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 103 118 moveto
-99 108 lineto
-96 118 lineto
-closepath
-stroke
-end grestore
-
-%	sml
-gsave 10 dict begin
-newpath 54 36 moveto
-0 36 lineto
-0 0 lineto
-54 0 lineto
-closepath
-stroke
-gsave 10 dict begin
-12 13 moveto
-(SML)
-[7.68 12.48 8.64]
-xshow
-end grestore
-end grestore
-
-%	serialization -> sml
-newpath 82 73 moveto
-73 64 62 53 52 43 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 55 41 moveto
-45 36 lineto
-50 46 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 55 41 moveto
-45 36 lineto
-50 46 lineto
-closepath
-stroke
-end grestore
-
-%	other
-gsave 10 dict begin
-gsave 10 dict begin
-93 13 moveto
-(...)
-[3.6 3.6 3.6]
-xshow
-end grestore
-end grestore
-
-%	serialization -> other
-gsave 10 dict begin
-dotted
-newpath 99 72 moveto
-99 64 99 55 99 46 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 103 46 moveto
-99 36 lineto
-96 46 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 103 46 moveto
-99 36 lineto
-96 46 lineto
-closepath
-stroke
-end grestore
-end grestore
-
-%	haskell
-gsave 10 dict begin
-newpath 204 36 moveto
-144 36 lineto
-144 0 lineto
-204 0 lineto
-closepath
-stroke
-gsave 10 dict begin
-152 13 moveto
-(Haskell)
-[10.08 6.24 5.52 6.72 6.24 3.84 3.84]
-xshow
-end grestore
-end grestore
-
-%	serialization -> haskell
-newpath 117 73 moveto
-127 64 138 53 148 43 curveto
-stroke
-gsave 10 dict begin
-solid
-1 setlinewidth
-0.000 0.000 0.000 edgecolor
-newpath 150 46 moveto
-155 36 lineto
-145 41 lineto
-closepath
-fill
-0.000 0.000 0.000 edgecolor
-newpath 150 46 moveto
-155 36 lineto
-145 41 lineto
-closepath
-stroke
-end grestore
-endpage
-showpage
-grestore
-%%PageTrailer
-%%EndPage: 1
-%%Trailer
-%%Pages: 1
-end
-restore
-%%EOF

Binary file doc-src/IsarAdvanced/Codegen/codegen_process.pdf has changed