# HG changeset patch
# User haftmann
# Date 1232115256 -3600
# Node ID 363f17dee9cad7cf9c34d80dbbbafc3f01e71393
# Parent  25472dc71a4b897cdb63d578ac8f64929bceec30
adapted to changes in class package

diff -r 25472dc71a4b -r 363f17dee9ca doc-src/IsarAdvanced/Classes/Thy/Classes.thy
--- 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
diff -r 25472dc71a4b -r 363f17dee9ca doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex
--- 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
diff -r 25472dc71a4b -r 363f17dee9ca src/FOL/ex/LocaleTest.thy
--- 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