doc-src/IsarImplementation/Thy/document/ML.tex

 
   \begin{quotation}
     \verb|Sign.declare_const: Markup.property list -> bstring * typ * mixfix|\isasep\isanewline%
 \verb|       -> theory -> term * theory|
 
-    \verb|Thm.add_def: bool -> bstring * term -> theory -> thm * theory|
+    \verb|Thm.add_def: bool -> bool -> bstring * term -> theory -> thm * theory|
   \end{quotation}
 
   Written with naive application, an addition of constant
   \isa{bar} with type \isa{foo\ {\isasymRightarrow}\ foo} and
   a corresponding definition \isa{bar\ {\isasymequiv}\ {\isasymlambda}x{\isachardot}\ x} would look like:
 
   \begin{quotation}
-   \verb|(fn (t, thy) => Thm.add_def false|\isasep\isanewline%
+   \verb|(fn (t, thy) => Thm.add_def false false|\isasep\isanewline%
 \verb|  ("bar_def", Logic.mk_equals (t, @{term "%x. x"})) thy)|\isasep\isanewline%
 \verb|    (Sign.declare_const []|\isasep\isanewline%
 \verb|      ("bar", @{typ "foo => foo"}, NoSyn) thy)|
   \end{quotation}
 

   for more convenient notation, most notably reverse application:
   \begin{quotation}
 \verb|thy|\isasep\isanewline%
 \verb||\verb,|,\verb|> Sign.declare_const [] ("bar", @{typ "foo => foo"}, NoSyn)|\isasep\isanewline%
 \verb||\verb,|,\verb|> (fn (t, thy) => thy|\isasep\isanewline%
-\verb||\verb,|,\verb|> Thm.add_def false|\isasep\isanewline%
+\verb||\verb,|,\verb|> Thm.add_def false false|\isasep\isanewline%
 \verb|     ("bar_def", Logic.mk_equals (t, @{term "%x. x"})))|
   \end{quotation}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %

   set of combinators is at hand, most notably \verb|op |\verb,|,\verb|->|
   which allows curried access to side results:
   \begin{quotation}
 \verb|thy|\isasep\isanewline%
 \verb||\verb,|,\verb|> Sign.declare_const [] ("bar", @{typ "foo => foo"}, NoSyn)|\isasep\isanewline%
-\verb||\verb,|,\verb|-> (fn t => Thm.add_def false|\isasep\isanewline%
+\verb||\verb,|,\verb|-> (fn t => Thm.add_def false false|\isasep\isanewline%
 \verb|      ("bar_def", Logic.mk_equals (t, @{term "%x. x"})))|\isasep\isanewline%
 
   \end{quotation}
 
   \noindent \verb|op |\verb,|,\verb|>>| allows for processing side results on their own:
   \begin{quotation}
 \verb|thy|\isasep\isanewline%
 \verb||\verb,|,\verb|> Sign.declare_const [] ("bar", @{typ "foo => foo"}, NoSyn)|\isasep\isanewline%
 \verb||\verb,|,\verb|>> (fn t => Logic.mk_equals (t, @{term "%x. x"}))|\isasep\isanewline%
-\verb||\verb,|,\verb|-> (fn def => Thm.add_def false ("bar_def", def))|\isasep\isanewline%
+\verb||\verb,|,\verb|-> (fn def => Thm.add_def false false ("bar_def", def))|\isasep\isanewline%
 
   \end{quotation}
 
   \noindent Orthogonally, \verb|op |\verb,|,\verb||\verb,|,\verb|>| applies a transformation
   in the presence of side results which are left unchanged:
   \begin{quotation}
 \verb|thy|\isasep\isanewline%
 \verb||\verb,|,\verb|> Sign.declare_const [] ("bar", @{typ "foo => foo"}, NoSyn)|\isasep\isanewline%
 \verb||\verb,|,\verb||\verb,|,\verb|> Sign.add_path "foobar"|\isasep\isanewline%
-\verb||\verb,|,\verb|-> (fn t => Thm.add_def false|\isasep\isanewline%
+\verb||\verb,|,\verb|-> (fn t => Thm.add_def false false|\isasep\isanewline%
 \verb|      ("bar_def", Logic.mk_equals (t, @{term "%x. x"})))|\isasep\isanewline%
 \verb||\verb,|,\verb||\verb,|,\verb|> Sign.restore_naming thy|\isasep\isanewline%
 
   \end{quotation}
 
   \noindent \indexml{op ||$>$$>$}\verb|op |\verb,|,\verb||\verb,|,\verb|>>| accumulates side results:
   \begin{quotation}
 \verb|thy|\isasep\isanewline%
 \verb||\verb,|,\verb|> Sign.declare_const [] ("bar", @{typ "foo => foo"}, NoSyn)|\isasep\isanewline%
 \verb||\verb,|,\verb||\verb,|,\verb|>> Sign.declare_const [] ("foobar", @{typ "foo => foo"}, NoSyn)|\isasep\isanewline%
-\verb||\verb,|,\verb|-> (fn (t1, t2) => Thm.add_def false|\isasep\isanewline%
+\verb||\verb,|,\verb|-> (fn (t1, t2) => Thm.add_def false false|\isasep\isanewline%
 \verb|      ("bar_def", Logic.mk_equals (t1, t2)))|\isasep\isanewline%
 
   \end{quotation}%
 \end{isamarkuptext}%
 \isamarkuptrue%

 \verb|  thy|\isasep\isanewline%
 \verb|  |\verb,|,\verb|> fold_map (fn const => Sign.declare_const []|\isasep\isanewline%
 \verb|       (const, @{typ "foo => foo"}, NoSyn)) consts|\isasep\isanewline%
 \verb|  |\verb,|,\verb|>> map (fn t => Logic.mk_equals (t, @{term "%x. x"}))|\isasep\isanewline%
 \verb|  |\verb,|,\verb|-> (fn defs => fold_map (fn def =>|\isasep\isanewline%
-\verb|       Thm.add_def false ("", def)) defs)|\isasep\isanewline%
+\verb|       Thm.add_def false false ("", def)) defs)|\isasep\isanewline%
 \verb|end|\isasep\isanewline%
 
   \end{quotation}%
 \end{isamarkuptext}%
 \isamarkuptrue%