# HG changeset patch
# User haftmann
# Date 1281521089 -7200
# Node ID 7813e44db886895ea62dfa803515a3e7f677f939
# Parent  6daf896bca5ea53870c5070b27d406a6a54f29d0# Parent  fb8fd73827d41d067c6c06c1e48198519e54d6c3
merged

diff -r fb8fd73827d4 -r 7813e44db886 doc-src/Classes/Thy/Classes.thy
--- a/doc-src/Classes/Thy/Classes.thy	Wed Aug 11 08:59:41 2010 +0200
+++ b/doc-src/Classes/Thy/Classes.thy	Wed Aug 11 12:04:49 2010 +0200
@@ -611,13 +611,12 @@
 text {*
   \noindent This maps to Haskell as follows:
 *}
-
+(*<*)code_include %invisible Haskell "Natural" -(*>*)
 text %quote {*@{code_stmts example (Haskell)}*}
 
 text {*
   \noindent The code in SML has explicit dictionary passing:
 *}
-
 text %quote {*@{code_stmts example (SML)}*}
 
 subsection {* Inspecting the type class universe *}
diff -r fb8fd73827d4 -r 7813e44db886 doc-src/Classes/Thy/Setup.thy
--- a/doc-src/Classes/Thy/Setup.thy	Wed Aug 11 08:59:41 2010 +0200
+++ b/doc-src/Classes/Thy/Setup.thy	Wed Aug 11 12:04:49 2010 +0200
@@ -1,8 +1,8 @@
 theory Setup
 imports Main Code_Integer
 uses
-  "../../antiquote_setup"
-  "../../more_antiquote"
+  "../../antiquote_setup.ML"
+  "../../more_antiquote.ML"
 begin
 
 setup {* Code_Target.set_default_code_width 74 *}
diff -r fb8fd73827d4 -r 7813e44db886 doc-src/Classes/Thy/document/Classes.tex
--- a/doc-src/Classes/Thy/document/Classes.tex	Wed Aug 11 08:59:41 2010 +0200
+++ b/doc-src/Classes/Thy/document/Classes.tex	Wed Aug 11 12:04:49 2010 +0200
@@ -1132,6 +1132,19 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
+\isadeliminvisible
+%
+\endisadeliminvisible
+%
+\isataginvisible
+%
+\endisataginvisible
+{\isafoldinvisible}%
+%
+\isadeliminvisible
+%
+\endisadeliminvisible
+%
 \isadelimquote
 %
 \endisadelimquote
diff -r fb8fd73827d4 -r 7813e44db886 doc-src/Main/Docs/Main_Doc.thy
--- a/doc-src/Main/Docs/Main_Doc.thy	Wed Aug 11 08:59:41 2010 +0200
+++ b/doc-src/Main/Docs/Main_Doc.thy	Wed Aug 11 12:04:49 2010 +0200
@@ -109,7 +109,7 @@
 @{const Set.empty} & @{term_type_only "Set.empty" "'a set"}\\
 @{const Set.insert} & @{term_type_only insert "'a\<Rightarrow>'a set\<Rightarrow>'a set"}\\
 @{const Collect} & @{term_type_only Collect "('a\<Rightarrow>bool)\<Rightarrow>'a set"}\\
-@{const "op :"} & @{term_type_only "op :" "'a\<Rightarrow>'a set\<Rightarrow>bool"} & (\texttt{:})\\
+@{const Set.member} & @{term_type_only Set.member "'a\<Rightarrow>'a set\<Rightarrow>bool"} & (\texttt{:})\\
 @{const Set.union} & @{term_type_only Set.union "'a set\<Rightarrow>'a set \<Rightarrow> 'a set"} & (\texttt{Un})\\
 @{const Set.inter} & @{term_type_only Set.inter "'a set\<Rightarrow>'a set \<Rightarrow> 'a set"} & (\texttt{Int})\\
 @{const UNION} & @{term_type_only UNION "'a set\<Rightarrow>('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"}\\
diff -r fb8fd73827d4 -r 7813e44db886 doc-src/TutorialI/Fun/ROOT.ML
--- a/doc-src/TutorialI/Fun/ROOT.ML	Wed Aug 11 08:59:41 2010 +0200
+++ b/doc-src/TutorialI/Fun/ROOT.ML	Wed Aug 11 12:04:49 2010 +0200
@@ -1,2 +1,2 @@
-use "../settings";
+use "../settings.ML";
 use_thy "fun0";
diff -r fb8fd73827d4 -r 7813e44db886 doc-src/TutorialI/Types/Axioms.thy
--- a/doc-src/TutorialI/Types/Axioms.thy	Wed Aug 11 08:59:41 2010 +0200
+++ b/doc-src/TutorialI/Types/Axioms.thy	Wed Aug 11 12:04:49 2010 +0200
@@ -59,7 +59,7 @@
 text {* \noindent Again, the interesting things enter the stage with
 parametric types: *}
 
-instantiation * :: (semigroup, semigroup) semigroup
+instantiation prod :: (semigroup, semigroup) semigroup
 begin
 
 instance proof
@@ -112,7 +112,7 @@
 This covers products as well:
 *}
 
-instantiation * :: (monoidl, monoidl) monoidl
+instantiation prod :: (monoidl, monoidl) monoidl
 begin
 
 definition
diff -r fb8fd73827d4 -r 7813e44db886 doc-src/TutorialI/Types/Overloading.thy
--- a/doc-src/TutorialI/Types/Overloading.thy	Wed Aug 11 08:59:41 2010 +0200
+++ b/doc-src/TutorialI/Types/Overloading.thy	Wed Aug 11 12:04:49 2010 +0200
@@ -55,10 +55,10 @@
 text {* \noindent From now on, terms like @{term "Suc (m \<oplus> 2)"} are
 legal. *}
 
-instantiation "*" :: (plus, plus) plus
+instantiation prod :: (plus, plus) plus
 begin
 
-text {* \noindent Here we instantiate the product type @{type "*"} to
+text {* \noindent Here we instantiate the product type @{type prod} to
 class @{class [source] plus}, given that its type arguments are of
 class @{class [source] plus}: *}
 
diff -r fb8fd73827d4 -r 7813e44db886 doc-src/TutorialI/Types/document/Axioms.tex
--- a/doc-src/TutorialI/Types/document/Axioms.tex	Wed Aug 11 08:59:41 2010 +0200
+++ b/doc-src/TutorialI/Types/document/Axioms.tex	Wed Aug 11 12:04:49 2010 +0200
@@ -123,7 +123,7 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{instantiation}\isamarkupfalse%
-\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}semigroup{\isacharcomma}\ semigroup{\isacharparenright}\ semigroup\isanewline
+\ prod\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}semigroup{\isacharcomma}\ semigroup{\isacharparenright}\ semigroup\isanewline
 \isakeyword{begin}\isanewline
 \isanewline
 \isacommand{instance}\isamarkupfalse%
@@ -226,7 +226,7 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{instantiation}\isamarkupfalse%
-\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}monoidl{\isacharcomma}\ monoidl{\isacharparenright}\ monoidl\isanewline
+\ prod\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}monoidl{\isacharcomma}\ monoidl{\isacharparenright}\ monoidl\isanewline
 \isakeyword{begin}\isanewline
 \isanewline
 \isacommand{definition}\isamarkupfalse%
diff -r fb8fd73827d4 -r 7813e44db886 doc-src/TutorialI/Types/document/Overloading.tex
--- a/doc-src/TutorialI/Types/document/Overloading.tex	Wed Aug 11 08:59:41 2010 +0200
+++ b/doc-src/TutorialI/Types/document/Overloading.tex	Wed Aug 11 12:04:49 2010 +0200
@@ -99,10 +99,10 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{instantiation}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isacharasterisk}{\isachardoublequoteclose}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}plus{\isacharcomma}\ plus{\isacharparenright}\ plus\isanewline
+\ prod\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}plus{\isacharcomma}\ plus{\isacharparenright}\ plus\isanewline
 \isakeyword{begin}%
 \begin{isamarkuptext}%
-\noindent Here we instantiate the product type \isa{{\isacharasterisk}} to
+\noindent Here we instantiate the product type \isa{prod} to
 class \isa{plus}, given that its type arguments are of
 class \isa{plus}:%
 \end{isamarkuptext}%