--- a/doc-src/IsarAdvanced/Classes/Thy/Classes.thy Fri Jan 16 14:59:06 2009 +0100
+++ b/doc-src/IsarAdvanced/Classes/Thy/Classes.thy Fri Jan 16 15:14:16 2009 +0100
@@ -368,14 +368,14 @@
text {*
\noindent The connection to the type system is done by means
of a primitive axclass
-*}
+*} setup %invisible {* Sign.add_path "foo" *}
axclass %quote idem < type
- idem: "f (f x) = f x"
+ idem: "f (f x) = f x" setup %invisible {* Sign.parent_path *}
text {* \noindent together with a corresponding interpretation: *}
-interpretation %quote idem_class': (* FIXME proper prefix? *)
+interpretation %quote idem_class:
idem "f \<Colon> (\<alpha>\<Colon>idem) \<Rightarrow> \<alpha>"
proof qed (rule idem)
@@ -459,7 +459,7 @@
of monoids for lists:
*}
-class_interpretation %quote list_monoid: monoid [append "[]"]
+interpretation %quote list_monoid!: monoid append "[]"
proof qed auto
text {*
@@ -474,10 +474,10 @@
"replicate 0 _ = []"
| "replicate (Suc n) xs = xs @ replicate n xs"
-class_interpretation %quote list_monoid: monoid [append "[]"] where
+interpretation %quote list_monoid!: monoid append "[]" where
"monoid.pow_nat append [] = replicate"
proof -
- class_interpret monoid [append "[]"] ..
+ interpret monoid append "[]" ..
show "monoid.pow_nat append [] = replicate"
proof
fix n
--- a/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex Fri Jan 16 14:59:06 2009 +0100
+++ b/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex Fri Jan 16 15:14:16 2009 +0100
@@ -655,7 +655,23 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
+\isadeliminvisible
+\ %
+\endisadeliminvisible
+%
+\isataginvisible
+\isacommand{setup}\isamarkupfalse%
+\ {\isacharverbatimopen}\ Sign{\isachardot}add{\isacharunderscore}path\ {\isachardoublequote}foo{\isachardoublequote}\ {\isacharverbatimclose}%
+\endisataginvisible
+{\isafoldinvisible}%
+%
+\isadeliminvisible
+%
+\endisadeliminvisible
+\isanewline
+%
\isadelimquote
+\isanewline
%
\endisadelimquote
%
@@ -670,6 +686,20 @@
%
\endisadelimquote
%
+\isadeliminvisible
+\ %
+\endisadeliminvisible
+%
+\isataginvisible
+\isacommand{setup}\isamarkupfalse%
+\ {\isacharverbatimopen}\ Sign{\isachardot}parent{\isacharunderscore}path\ {\isacharverbatimclose}%
+\endisataginvisible
+{\isafoldinvisible}%
+%
+\isadeliminvisible
+%
+\endisadeliminvisible
+%
\begin{isamarkuptext}%
\noindent together with a corresponding interpretation:%
\end{isamarkuptext}%
@@ -681,7 +711,7 @@
%
\isatagquote
\isacommand{interpretation}\isamarkupfalse%
-\ idem{\isacharunderscore}class{\isacharprime}{\isacharcolon}\ \ \ \ \isanewline
+\ idem{\isacharunderscore}class{\isacharcolon}\isanewline
\ \ idem\ {\isachardoublequoteopen}f\ {\isasymColon}\ {\isacharparenleft}{\isasymalpha}{\isasymColon}idem{\isacharparenright}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\isanewline
\isacommand{proof}\isamarkupfalse%
\ \isacommand{qed}\isamarkupfalse%
@@ -843,8 +873,8 @@
\endisadelimquote
%
\isatagquote
-\isacommand{class{\isacharunderscore}interpretation}\isamarkupfalse%
-\ list{\isacharunderscore}monoid{\isacharcolon}\ monoid\ {\isacharbrackleft}append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
+\isacommand{interpretation}\isamarkupfalse%
+\ list{\isacharunderscore}monoid{\isacharbang}{\isacharcolon}\ monoid\ append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ \isacommand{qed}\isamarkupfalse%
\ auto%
@@ -874,13 +904,13 @@
\ \ {\isachardoublequoteopen}replicate\ {\isadigit{0}}\ {\isacharunderscore}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
\ \ {\isacharbar}\ {\isachardoublequoteopen}replicate\ {\isacharparenleft}Suc\ n{\isacharparenright}\ xs\ {\isacharequal}\ xs\ {\isacharat}\ replicate\ n\ xs{\isachardoublequoteclose}\isanewline
\isanewline
-\isacommand{class{\isacharunderscore}interpretation}\isamarkupfalse%
-\ list{\isacharunderscore}monoid{\isacharcolon}\ monoid\ {\isacharbrackleft}append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\ \isakeyword{where}\isanewline
+\isacommand{interpretation}\isamarkupfalse%
+\ list{\isacharunderscore}monoid{\isacharbang}{\isacharcolon}\ monoid\ append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ append\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ replicate{\isachardoublequoteclose}\isanewline
\isacommand{proof}\isamarkupfalse%
\ {\isacharminus}\isanewline
-\ \ \isacommand{class{\isacharunderscore}interpret}\isamarkupfalse%
-\ monoid\ {\isacharbrackleft}append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\ \ \isacommand{interpret}\isamarkupfalse%
+\ monoid\ append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ append\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ replicate{\isachardoublequoteclose}\isanewline
--- a/src/FOL/ex/LocaleTest.thy Fri Jan 16 14:59:06 2009 +0100
+++ b/src/FOL/ex/LocaleTest.thy Fri Jan 16 15:14:16 2009 +0100
@@ -8,9 +8,6 @@
imports FOL
begin
-ML_val {* set Toplevel.debug *}
-
-
typedecl int arities int :: "term"
consts plus :: "int => int => int" (infixl "+" 60)
zero :: int ("0")
@@ -483,6 +480,4 @@
thm local_free.lone [where ?zero = 0]
qed
-ML_val {* reset Toplevel.debug *}
-
end