updated generated files;

--- a/doc-src/Classes/Thy/document/Classes.tex	Sun Apr 22 22:01:45 2012 +0200
+++ b/doc-src/Classes/Thy/document/Classes.tex	Sun Apr 22 22:02:52 2012 +0200
@@ -1134,11 +1134,40 @@
 \isanewline
 data\ Nat\ {\isaliteral{3D}{\isacharequal}}\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{7C}{\isacharbar}}\ Suc\ Nat{\isaliteral{3B}{\isacharsemicolon}}\isanewline
 \isanewline
-nat{\isaliteral{5F}{\isacharunderscore}}aux\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ Integer\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ Nat\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ Nat{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-nat{\isaliteral{5F}{\isacharunderscore}}aux\ i\ n\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ i\ {\isaliteral{3C}{\isacharless}}{\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}\ then\ n\ else\ nat{\isaliteral{5F}{\isacharunderscore}}aux\ {\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+data\ Numa\ {\isaliteral{3D}{\isacharequal}}\ One\ {\isaliteral{7C}{\isacharbar}}\ Bit{\isadigit{0}}\ Numa\ {\isaliteral{7C}{\isacharbar}}\ Bit{\isadigit{1}}\ Numa{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+\isanewline
+plus{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ Nat\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ Nat\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ Nat{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+plus{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{28}{\isacharparenleft}}Suc\ m{\isaliteral{29}{\isacharparenright}}\ n\ {\isaliteral{3D}{\isacharequal}}\ plus{\isaliteral{5F}{\isacharunderscore}}nat\ m\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+plus{\isaliteral{5F}{\isacharunderscore}}nat\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\ n\ {\isaliteral{3D}{\isacharequal}}\ n{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+\isanewline
+abs{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ Integer\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ Integer{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+abs{\isaliteral{5F}{\isacharunderscore}}int\ i\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ i\ {\isaliteral{3C}{\isacharless}}\ {\isadigit{0}}\ then\ negate\ i\ else\ i{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+\isanewline
+sgn{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ Integer\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ Integer{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+sgn{\isaliteral{5F}{\isacharunderscore}}int\ i\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ i\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}\ then\ {\isadigit{0}}\ else\ {\isaliteral{28}{\isacharparenleft}}if\ {\isadigit{0}}\ {\isaliteral{3C}{\isacharless}}\ i\ then\ {\isadigit{1}}\ else\ negate\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+\isanewline
+apsnd\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ forall\ a\ b\ c{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{28}{\isacharparenleft}}c{\isaliteral{2C}{\isacharcomma}}\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{28}{\isacharparenleft}}c{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+apsnd\ f\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ f\ y{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+\isanewline
+divmod{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ Integer\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ Integer\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{28}{\isacharparenleft}}Integer{\isaliteral{2C}{\isacharcomma}}\ Integer{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+divmod{\isaliteral{5F}{\isacharunderscore}}int\ k\ l\ {\isaliteral{3D}{\isacharequal}}\isanewline
+\ \ {\isaliteral{28}{\isacharparenleft}}if\ k\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}\ then\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline
+\ \ \ \ else\ {\isaliteral{28}{\isacharparenleft}}if\ l\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}\ then\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{2C}{\isacharcomma}}\ k{\isaliteral{29}{\isacharparenright}}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ else\ apsnd\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C}{\isacharbackslash}}\ a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ sgn{\isaliteral{5F}{\isacharunderscore}}int\ l\ {\isaliteral{2A}{\isacharasterisk}}\ a{\isaliteral{29}{\isacharparenright}}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}if\ sgn{\isaliteral{5F}{\isacharunderscore}}int\ k\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ sgn{\isaliteral{5F}{\isacharunderscore}}int\ l\ then\ divMod\ {\isaliteral{28}{\isacharparenleft}}abs\ k{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}abs\ l{\isaliteral{29}{\isacharparenright}}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ else\ let\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}r{\isaliteral{2C}{\isacharcomma}}\ s{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ divMod\ {\isaliteral{28}{\isacharparenleft}}abs\ k{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}abs\ l{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{7D}{\isacharbraceright}}\ in\ {\isaliteral{28}{\isacharparenleft}}if\ s\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}\ then\ {\isaliteral{28}{\isacharparenleft}}negate\ r{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ else\ {\isaliteral{28}{\isacharparenleft}}negate\ r\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ abs{\isaliteral{5F}{\isacharunderscore}}int\ l\ {\isaliteral{2D}{\isacharminus}}\ s{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
 \isanewline
 nat\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ Integer\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ Nat{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-nat\ i\ {\isaliteral{3D}{\isacharequal}}\ nat{\isaliteral{5F}{\isacharunderscore}}aux\ i\ Zero{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+nat\ k\ {\isaliteral{3D}{\isacharequal}}\isanewline
+\ \ {\isaliteral{28}{\isacharparenleft}}if\ k\ {\isaliteral{3C}{\isacharless}}{\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}\ then\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\isanewline
+\ \ \ \ else\ let\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}l{\isaliteral{2C}{\isacharcomma}}\ j{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ divmod{\isaliteral{5F}{\isacharunderscore}}int\ k\ {\isadigit{2}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ n\ {\isaliteral{3D}{\isacharequal}}\ nat\ l{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ la\ {\isaliteral{3D}{\isacharequal}}\ plus{\isaliteral{5F}{\isacharunderscore}}nat\ n\ n{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+\ \ \ \ \ \ \ \ \ {\isaliteral{7D}{\isacharbraceright}}\ in\ {\isaliteral{28}{\isacharparenleft}}if\ j\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}\ then\ la\ else\ Suc\ la{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
 \isanewline
 class\ Semigroup\ a\ where\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
 \ \ mult\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ a{\isaliteral{3B}{\isacharsemicolon}}\isanewline
@@ -1216,7 +1245,12 @@
 \begin{isamarkuptext}%
 structure\ Example\ {\isaliteral{3A}{\isacharcolon}}\ sig\isanewline
 \ \ datatype\ nat\ {\isaliteral{3D}{\isacharequal}}\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{7C}{\isacharbar}}\ Suc\ of\ nat\isanewline
-\ \ val\ nat{\isaliteral{5F}{\isacharunderscore}}aux\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ nat\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ nat\isanewline
+\ \ datatype\ num\ {\isaliteral{3D}{\isacharequal}}\ One\ {\isaliteral{7C}{\isacharbar}}\ Bit{\isadigit{0}}\ of\ num\ {\isaliteral{7C}{\isacharbar}}\ Bit{\isadigit{1}}\ of\ num\isanewline
+\ \ val\ plus{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{3A}{\isacharcolon}}\ nat\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ nat\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ nat\isanewline
+\ \ val\ abs{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ IntInf{\isaliteral{2E}{\isachardot}}int\isanewline
+\ \ val\ sgn{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ IntInf{\isaliteral{2E}{\isachardot}}int\isanewline
+\ \ val\ apsnd\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}c\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}c\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{27}{\isacharprime}}b\isanewline
+\ \ val\ divmod{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ {\isaliteral{2A}{\isacharasterisk}}\ IntInf{\isaliteral{2E}{\isachardot}}int\isanewline
 \ \ val\ nat\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ nat\isanewline
 \ \ type\ {\isaliteral{27}{\isacharprime}}a\ semigroup\isanewline
 \ \ val\ mult\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ semigroup\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\isanewline
@@ -1242,11 +1276,45 @@
 \isanewline
 datatype\ nat\ {\isaliteral{3D}{\isacharequal}}\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{7C}{\isacharbar}}\ Suc\ of\ nat{\isaliteral{3B}{\isacharsemicolon}}\isanewline
 \isanewline
-fun\ nat{\isaliteral{5F}{\isacharunderscore}}aux\ i\ n\ {\isaliteral{3D}{\isacharequal}}\isanewline
-\ \ {\isaliteral{28}{\isacharparenleft}}if\ IntInf{\isaliteral{2E}{\isachardot}}{\isaliteral{3C}{\isacharless}}{\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}i{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ then\ n\isanewline
-\ \ \ \ else\ nat{\isaliteral{5F}{\isacharunderscore}}aux\ {\isaliteral{28}{\isacharparenleft}}IntInf{\isaliteral{2E}{\isachardot}}{\isaliteral{2D}{\isacharminus}}\ {\isaliteral{28}{\isacharparenleft}}i{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+datatype\ num\ {\isaliteral{3D}{\isacharequal}}\ One\ {\isaliteral{7C}{\isacharbar}}\ Bit{\isadigit{0}}\ of\ num\ {\isaliteral{7C}{\isacharbar}}\ Bit{\isadigit{1}}\ of\ num{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+\isanewline
+fun\ plus{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{28}{\isacharparenleft}}Suc\ m{\isaliteral{29}{\isacharparenright}}\ n\ {\isaliteral{3D}{\isacharequal}}\ plus{\isaliteral{5F}{\isacharunderscore}}nat\ m\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\isanewline
+\ \ {\isaliteral{7C}{\isacharbar}}\ plus{\isaliteral{5F}{\isacharunderscore}}nat\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\ n\ {\isaliteral{3D}{\isacharequal}}\ n{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+\isanewline
+fun\ abs{\isaliteral{5F}{\isacharunderscore}}int\ i\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ IntInf{\isaliteral{2E}{\isachardot}}{\isaliteral{3C}{\isacharless}}\ {\isaliteral{28}{\isacharparenleft}}i{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ then\ IntInf{\isaliteral{2E}{\isachardot}}{\isaliteral{7E}{\isachartilde}}\ i\ else\ i{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+\isanewline
+fun\ sgn{\isaliteral{5F}{\isacharunderscore}}int\ i\ {\isaliteral{3D}{\isacharequal}}\isanewline
+\ \ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ then\ {\isadigit{0}}\isanewline
+\ \ \ \ else\ {\isaliteral{28}{\isacharparenleft}}if\ IntInf{\isaliteral{2E}{\isachardot}}{\isaliteral{3C}{\isacharless}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{2C}{\isacharcomma}}\ i{\isaliteral{29}{\isacharparenright}}\ then\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int{\isaliteral{29}{\isacharparenright}}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ else\ IntInf{\isaliteral{2E}{\isachardot}}{\isaliteral{7E}{\isachartilde}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+\isanewline
+fun\ apsnd\ f\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ f\ y{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
 \isanewline
-fun\ nat\ i\ {\isaliteral{3D}{\isacharequal}}\ nat{\isaliteral{5F}{\isacharunderscore}}aux\ i\ Zero{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+fun\ divmod{\isaliteral{5F}{\isacharunderscore}}int\ k\ l\ {\isaliteral{3D}{\isacharequal}}\isanewline
+\ \ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}k\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ then\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline
+\ \ \ \ else\ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}l\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ then\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{2C}{\isacharcomma}}\ k{\isaliteral{29}{\isacharparenright}}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ else\ apsnd\ {\isaliteral{28}{\isacharparenleft}}fn\ a\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ IntInf{\isaliteral{2E}{\isachardot}}{\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}sgn{\isaliteral{5F}{\isacharunderscore}}int\ l{\isaliteral{2C}{\isacharcomma}}\ a{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}sgn{\isaliteral{5F}{\isacharunderscore}}int\ k{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}sgn{\isaliteral{5F}{\isacharunderscore}}int\ l{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ then\ IntInf{\isaliteral{2E}{\isachardot}}divMod\ {\isaliteral{28}{\isacharparenleft}}IntInf{\isaliteral{2E}{\isachardot}}abs\ k{\isaliteral{2C}{\isacharcomma}}\ IntInf{\isaliteral{2E}{\isachardot}}abs\ l{\isaliteral{29}{\isacharparenright}}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ else\ let\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ val\ {\isaliteral{28}{\isacharparenleft}}r{\isaliteral{2C}{\isacharcomma}}\ s{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ IntInf{\isaliteral{2E}{\isachardot}}divMod\ {\isaliteral{28}{\isacharparenleft}}IntInf{\isaliteral{2E}{\isachardot}}abs\ k{\isaliteral{2C}{\isacharcomma}}\ IntInf{\isaliteral{2E}{\isachardot}}abs\ l{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ in\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}s\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ then\ {\isaliteral{28}{\isacharparenleft}}IntInf{\isaliteral{2E}{\isachardot}}{\isaliteral{7E}{\isachartilde}}\ r{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ else\ {\isaliteral{28}{\isacharparenleft}}IntInf{\isaliteral{2E}{\isachardot}}{\isaliteral{2D}{\isacharminus}}\ {\isaliteral{28}{\isacharparenleft}}IntInf{\isaliteral{2E}{\isachardot}}{\isaliteral{7E}{\isachartilde}}\isanewline
+\ \ \ \ \ \ \ \ \ \ r{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ IntInf{\isaliteral{2E}{\isachardot}}{\isaliteral{2D}{\isacharminus}}\ {\isaliteral{28}{\isacharparenleft}}abs{\isaliteral{5F}{\isacharunderscore}}int\ l{\isaliteral{2C}{\isacharcomma}}\ s{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ end{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+\isanewline
+fun\ nat\ k\ {\isaliteral{3D}{\isacharequal}}\isanewline
+\ \ {\isaliteral{28}{\isacharparenleft}}if\ IntInf{\isaliteral{2E}{\isachardot}}{\isaliteral{3C}{\isacharless}}{\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}k{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ then\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\isanewline
+\ \ \ \ else\ let\isanewline
+\ \ \ \ \ \ \ \ \ \ \ val\ {\isaliteral{28}{\isacharparenleft}}l{\isaliteral{2C}{\isacharcomma}}\ j{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ divmod{\isaliteral{5F}{\isacharunderscore}}int\ k\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{2}}\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ val\ n\ {\isaliteral{3D}{\isacharequal}}\ nat\ l{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ val\ la\ {\isaliteral{3D}{\isacharequal}}\ plus{\isaliteral{5F}{\isacharunderscore}}nat\ n\ n{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+\ \ \ \ \ \ \ \ \ in\isanewline
+\ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}j\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ then\ la\ else\ Suc\ la{\isaliteral{29}{\isacharparenright}}\isanewline
+\ \ \ \ \ \ \ \ \ end{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
 \isanewline
 type\ {\isaliteral{27}{\isacharprime}}a\ semigroup\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}mult\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
 val\ mult\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{23}{\isacharhash}}mult\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ semigroup\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{3B}{\isacharsemicolon}}\isanewline
@@ -1267,13 +1335,12 @@
 \ \ \ \ mult\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}semigroup{\isaliteral{5F}{\isacharunderscore}}monoidl\ o\ monoidl{\isaliteral{5F}{\isacharunderscore}}monoid{\isaliteral{29}{\isacharparenright}}\ A{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ x\ {\isaliteral{28}{\isacharparenleft}}pow{\isaliteral{5F}{\isacharunderscore}}nat\ A{\isaliteral{5F}{\isacharunderscore}}\ n\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
 \isanewline
 fun\ pow{\isaliteral{5F}{\isacharunderscore}}int\ A{\isaliteral{5F}{\isacharunderscore}}\ k\ x\ {\isaliteral{3D}{\isacharequal}}\isanewline
-\ \ {\isaliteral{28}{\isacharparenleft}}if\ IntInf{\isaliteral{2E}{\isachardot}}{\isaliteral{3C}{\isacharless}}{\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ k{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ \ \ then\ pow{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{28}{\isacharparenleft}}monoid{\isaliteral{5F}{\isacharunderscore}}group\ A{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}nat\ k{\isaliteral{29}{\isacharparenright}}\ x\isanewline
+\ \ {\isaliteral{28}{\isacharparenleft}}if\ IntInf{\isaliteral{2E}{\isachardot}}{\isaliteral{3C}{\isacharless}}{\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{2C}{\isacharcomma}}\ k{\isaliteral{29}{\isacharparenright}}\ then\ pow{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{28}{\isacharparenleft}}monoid{\isaliteral{5F}{\isacharunderscore}}group\ A{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}nat\ k{\isaliteral{29}{\isacharparenright}}\ x\isanewline
 \ \ \ \ else\ inverse\ A{\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{28}{\isacharparenleft}}pow{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{28}{\isacharparenleft}}monoid{\isaliteral{5F}{\isacharunderscore}}group\ A{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}nat\ {\isaliteral{28}{\isacharparenleft}}IntInf{\isaliteral{2E}{\isachardot}}{\isaliteral{7E}{\isachartilde}}\ k{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
 \isanewline
 fun\ mult{\isaliteral{5F}{\isacharunderscore}}int\ i\ j\ {\isaliteral{3D}{\isacharequal}}\ IntInf{\isaliteral{2E}{\isachardot}}{\isaliteral{2B}{\isacharplus}}\ {\isaliteral{28}{\isacharparenleft}}i{\isaliteral{2C}{\isacharcomma}}\ j{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
 \isanewline
-val\ neutral{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+val\ neutral{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
 \isanewline
 val\ semigroup{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}mult\ {\isaliteral{3D}{\isacharequal}}\ mult{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ semigroup{\isaliteral{3B}{\isacharsemicolon}}\isanewline
 \isanewline
@@ -1333,10 +1400,51 @@
 final\ case\ object\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\ extends\ nat\isanewline
 final\ case\ class\ Suc{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{3A}{\isacharcolon}}\ nat{\isaliteral{29}{\isacharparenright}}\ extends\ nat\isanewline
 \isanewline
-def\ nat{\isaliteral{5F}{\isacharunderscore}}aux{\isaliteral{28}{\isacharparenleft}}i{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{2C}{\isacharcomma}}\ n{\isaliteral{3A}{\isacharcolon}}\ nat{\isaliteral{29}{\isacharparenright}}{\isaliteral{3A}{\isacharcolon}}\ nat\ {\isaliteral{3D}{\isacharequal}}\isanewline
-\ \ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{3C}{\isacharless}}{\isaliteral{3D}{\isacharequal}}\ BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ n\ else\ nat{\isaliteral{5F}{\isacharunderscore}}aux{\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{2D}{\isacharminus}}\ BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ Suc{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline
+abstract\ sealed\ class\ num\isanewline
+final\ case\ object\ One\ extends\ num\isanewline
+final\ case\ class\ Bit{\isadigit{0}}{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{3A}{\isacharcolon}}\ num{\isaliteral{29}{\isacharparenright}}\ extends\ num\isanewline
+final\ case\ class\ Bit{\isadigit{1}}{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{3A}{\isacharcolon}}\ num{\isaliteral{29}{\isacharparenright}}\ extends\ num\isanewline
+\isanewline
+def\ plus{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{28}{\isacharparenleft}}x{\isadigit{0}}{\isaliteral{3A}{\isacharcolon}}\ nat{\isaliteral{2C}{\isacharcomma}}\ n{\isaliteral{3A}{\isacharcolon}}\ nat{\isaliteral{29}{\isacharparenright}}{\isaliteral{3A}{\isacharcolon}}\ nat\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}x{\isadigit{0}}{\isaliteral{2C}{\isacharcomma}}\ n{\isaliteral{29}{\isacharparenright}}\ match\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
+\ \ case\ {\isaliteral{28}{\isacharparenleft}}Suc{\isaliteral{28}{\isacharparenleft}}m{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ plus{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{28}{\isacharparenleft}}m{\isaliteral{2C}{\isacharcomma}}\ Suc{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline
+\ \ case\ {\isaliteral{28}{\isacharparenleft}}Zero{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{2C}{\isacharcomma}}\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ n\isanewline
+{\isaliteral{7D}{\isacharbraceright}}\isanewline
+\isanewline
+def\ abs{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{28}{\isacharparenleft}}i{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{29}{\isacharparenright}}{\isaliteral{3A}{\isacharcolon}}\ BigInt\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{3C}{\isacharless}}\ BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2D}{\isacharminus}}\ i{\isaliteral{29}{\isacharparenright}}\ else\ i{\isaliteral{29}{\isacharparenright}}\isanewline
+\isanewline
+def\ sgn{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{28}{\isacharparenleft}}i{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{29}{\isacharparenright}}{\isaliteral{3A}{\isacharcolon}}\ BigInt\ {\isaliteral{3D}{\isacharequal}}\isanewline
+\ \ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline
+\ \ \ \ else\ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{28}{\isacharparenleft}}BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3C}{\isacharless}}\ i{\isaliteral{29}{\isacharparenright}}\ BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ else\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2D}{\isacharminus}}\ BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline
+\isanewline
+def\ apsnd{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{2C}{\isacharcomma}}\ B{\isaliteral{2C}{\isacharcomma}}\ C{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{28}{\isacharparenleft}}f{\isaliteral{3A}{\isacharcolon}}\ A\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ B{\isaliteral{2C}{\isacharcomma}}\ x{\isadigit{1}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}C{\isaliteral{2C}{\isacharcomma}}\ A{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}C{\isaliteral{2C}{\isacharcomma}}\ B{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}f{\isaliteral{2C}{\isacharcomma}}\ x{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ match\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
+\ \ case\ {\isaliteral{28}{\isacharparenleft}}f{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ y{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ f{\isaliteral{28}{\isacharparenleft}}y{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline
+{\isaliteral{7D}{\isacharbraceright}}\isanewline
 \isanewline
-def\ nat{\isaliteral{28}{\isacharparenleft}}i{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{29}{\isacharparenright}}{\isaliteral{3A}{\isacharcolon}}\ nat\ {\isaliteral{3D}{\isacharequal}}\ nat{\isaliteral{5F}{\isacharunderscore}}aux{\isaliteral{28}{\isacharparenleft}}i{\isaliteral{2C}{\isacharcomma}}\ Zero{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{29}{\isacharparenright}}\isanewline
+def\ divmod{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{28}{\isacharparenleft}}k{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{2C}{\isacharcomma}}\ l{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{29}{\isacharparenright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}BigInt{\isaliteral{2C}{\isacharcomma}}\ BigInt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline
+\ \ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{28}{\isacharparenleft}}k\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline
+\ \ \ \ else\ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{28}{\isacharparenleft}}l\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ k{\isaliteral{29}{\isacharparenright}}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ else\ apsnd{\isaliteral{5B}{\isacharbrackleft}}BigInt{\isaliteral{2C}{\isacharcomma}}\ BigInt{\isaliteral{2C}{\isacharcomma}}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ BigInt{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ sgn{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{28}{\isacharparenleft}}l{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A}{\isacharasterisk}}\ a{\isaliteral{2C}{\isacharcomma}}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{28}{\isacharparenleft}}sgn{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{28}{\isacharparenleft}}k{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ sgn{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{28}{\isacharparenleft}}l{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}k{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{28}{\isacharparenleft}}l{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ if\ {\isaliteral{28}{\isacharparenleft}}l\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ k{\isaliteral{29}{\isacharparenright}}\ else\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}k{\isaliteral{2E}{\isachardot}}abs\ {\isaliteral{2F}{\isacharslash}}{\isaliteral{25}{\isacharpercent}}\ l{\isaliteral{2E}{\isachardot}}abs{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2E}{\isachardot}}apply{\isaliteral{28}{\isacharparenleft}}k{\isaliteral{29}{\isacharparenright}}{\isaliteral{2E}{\isachardot}}apply{\isaliteral{28}{\isacharparenleft}}l{\isaliteral{29}{\isacharparenright}}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ else\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
+\ \ \ \ val\ {\isaliteral{28}{\isacharparenleft}}r{\isaliteral{2C}{\isacharcomma}}\ s{\isaliteral{29}{\isacharparenright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}BigInt{\isaliteral{2C}{\isacharcomma}}\ BigInt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline
+\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}k{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{28}{\isacharparenleft}}l{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ if\ {\isaliteral{28}{\isacharparenleft}}l\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ k{\isaliteral{29}{\isacharparenright}}\ else\isanewline
+\ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}k{\isaliteral{2E}{\isachardot}}abs\ {\isaliteral{2F}{\isacharslash}}{\isaliteral{25}{\isacharpercent}}\ l{\isaliteral{2E}{\isachardot}}abs{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2E}{\isachardot}}apply{\isaliteral{28}{\isacharparenleft}}k{\isaliteral{29}{\isacharparenright}}{\isaliteral{2E}{\isachardot}}apply{\isaliteral{28}{\isacharparenleft}}l{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+\ \ \ \ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{28}{\isacharparenleft}}s\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2D}{\isacharminus}}\ r{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline
+\ \ \ \ \ \ else\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{2D}{\isacharminus}}\ r{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2D}{\isacharminus}}\ BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ abs{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{28}{\isacharparenleft}}l{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2D}{\isacharminus}}\ s{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline
+\ \ {\isaliteral{7D}{\isacharbraceright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline
+\isanewline
+def\ nat{\isaliteral{28}{\isacharparenleft}}k{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{29}{\isacharparenright}}{\isaliteral{3A}{\isacharcolon}}\ nat\ {\isaliteral{3D}{\isacharequal}}\isanewline
+\ \ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{28}{\isacharparenleft}}k\ {\isaliteral{3C}{\isacharless}}{\isaliteral{3D}{\isacharequal}}\ BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\isanewline
+\ \ \ \ else\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ val\ {\isaliteral{28}{\isacharparenleft}}l{\isaliteral{2C}{\isacharcomma}}\ j{\isaliteral{29}{\isacharparenright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}BigInt{\isaliteral{2C}{\isacharcomma}}\ BigInt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ divmod{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{28}{\isacharparenleft}}k{\isaliteral{2C}{\isacharcomma}}\ BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ val\ n{\isaliteral{3A}{\isacharcolon}}\ nat\ {\isaliteral{3D}{\isacharequal}}\ nat{\isaliteral{28}{\isacharparenleft}}l{\isaliteral{29}{\isacharparenright}}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ val\ la{\isaliteral{3A}{\isacharcolon}}\ nat\ {\isaliteral{3D}{\isacharequal}}\ plus{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{2C}{\isacharcomma}}\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+\ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{28}{\isacharparenleft}}j\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ la\ else\ Suc{\isaliteral{28}{\isacharparenleft}}la{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline
+\ \ \ \ \ \ \ \ \ {\isaliteral{7D}{\isacharbraceright}}{\isaliteral{29}{\isacharparenright}}\isanewline
 \isanewline
 trait\ semigroup{\isaliteral{5B}{\isacharbrackleft}}A{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
 \ \ val\ {\isaliteral{60}{\isacharbackquote}}Example{\isaliteral{2E}{\isachardot}}mult{\isaliteral{60}{\isacharbackquote}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}A{\isaliteral{2C}{\isacharcomma}}\ A{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ A\isanewline

--- a/doc-src/System/Thy/document/Basics.tex	Sun Apr 22 22:01:45 2012 +0200
+++ b/doc-src/System/Thy/document/Basics.tex	Sun Apr 22 22:02:52 2012 +0200
@@ -167,10 +167,11 @@
 
   \begin{description}
 
-  \item[\indexdef{}{setting}{USER\_HOME}\hypertarget{setting.USER-HOME}{\hyperlink{setting.USER-HOME}{\mbox{\isa{\isatt{USER{\isaliteral{5F}{\isacharunderscore}}HOME}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}] Is the cross-platform
-  user home directory.  On Unix systems this is usually the same as
-  \hyperlink{setting.HOME}{\mbox{\isa{\isatt{HOME}}}}, but on Windows it is the regular home directory of
-  the, not the one of within the Cygwin root file-system.
+  \item[\indexdef{}{setting}{USER\_HOME}\hypertarget{setting.USER-HOME}{\hyperlink{setting.USER-HOME}{\mbox{\isa{\isatt{USER{\isaliteral{5F}{\isacharunderscore}}HOME}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}] Is the
+  cross-platform user home directory.  On Unix systems this is usually
+  the same as \hyperlink{setting.HOME}{\mbox{\isa{\isatt{HOME}}}}, but on Windows it is the regular home
+  directory of the user, not the one of within the Cygwin root
+  file-system.
 
  \item[\indexdef{}{setting}{ISABELLE\_HOME}\hypertarget{setting.ISABELLE-HOME}{\hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}] is the location of the
   top-level Isabelle distribution directory. This is automatically