# HG changeset patch
# User haftmann
# Date 1197446407 -3600
# Node ID 7793d6423d01bed534910938c22b84393a233fc8
# Parent  779c79c36c5e37f850cfe5accf86c0dc1a35101a
adjusted

diff -r 779c79c36c5e -r 7793d6423d01 doc-src/IsarImplementation/Thy/ML.thy
--- a/doc-src/IsarImplementation/Thy/ML.thy	Tue Dec 11 10:23:14 2007 +0100
+++ b/doc-src/IsarImplementation/Thy/ML.thy	Wed Dec 12 09:00:07 2007 +0100
@@ -320,7 +320,7 @@
     @{ML "Sign.declare_const: Markup.property list -> bstring * typ * mixfix
        -> theory -> term * theory"}
 
-    @{ML "Thm.add_def: bool -> bstring * term -> theory -> thm * theory"}
+    @{ML "Thm.add_def: bool -> bool -> bstring * term -> theory -> thm * theory"}
   \end{quotation}
 
   Written with naive application, an addition of constant
@@ -328,7 +328,7 @@
   a corresponding definition @{term "bar \<equiv> \<lambda>x. x"} would look like:
 
   \begin{quotation}
-   @{ML "(fn (t, thy) => Thm.add_def false
+   @{ML "(fn (t, thy) => Thm.add_def false false
   (\"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})) thy)
     (Sign.declare_const []
       (\"bar\", @{typ \"foo => foo\"}, NoSyn) thy)"}
@@ -346,7 +346,7 @@
 @{ML "thy
 |> Sign.declare_const [] (\"bar\", @{typ \"foo => foo\"}, NoSyn)
 |> (fn (t, thy) => thy
-|> Thm.add_def false
+|> Thm.add_def false false
      (\"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})))"}
   \end{quotation}
 *}
@@ -368,7 +368,7 @@
   \begin{quotation}
 @{ML "thy
 |> Sign.declare_const [] (\"bar\", @{typ \"foo => foo\"}, NoSyn)
-|-> (fn t => Thm.add_def false
+|-> (fn t => Thm.add_def false false
       (\"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})))
 "}
   \end{quotation}
@@ -378,7 +378,7 @@
 @{ML "thy
 |> Sign.declare_const [] (\"bar\", @{typ \"foo => foo\"}, NoSyn)
 |>> (fn t => Logic.mk_equals (t, @{term \"%x. x\"}))
-|-> (fn def => Thm.add_def false (\"bar_def\", def))
+|-> (fn def => Thm.add_def false false (\"bar_def\", def))
 "}
   \end{quotation}
 
@@ -388,7 +388,7 @@
 @{ML "thy
 |> Sign.declare_const [] (\"bar\", @{typ \"foo => foo\"}, NoSyn)
 ||> Sign.add_path \"foobar\"
-|-> (fn t => Thm.add_def false
+|-> (fn t => Thm.add_def false false
       (\"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})))
 ||> Sign.restore_naming thy
 "}
@@ -399,7 +399,7 @@
 @{ML "thy
 |> Sign.declare_const [] (\"bar\", @{typ \"foo => foo\"}, NoSyn)
 ||>> Sign.declare_const [] (\"foobar\", @{typ \"foo => foo\"}, NoSyn)
-|-> (fn (t1, t2) => Thm.add_def false
+|-> (fn (t1, t2) => Thm.add_def false false
       (\"bar_def\", Logic.mk_equals (t1, t2)))
 "}
   \end{quotation}
@@ -444,7 +444,7 @@
        (const, @{typ \"foo => foo\"}, NoSyn)) consts
   |>> map (fn t => Logic.mk_equals (t, @{term \"%x. x\"}))
   |-> (fn defs => fold_map (fn def =>
-       Thm.add_def false (\"\", def)) defs)
+       Thm.add_def false false (\"\", def)) defs)
 end
 "}
   \end{quotation}
diff -r 779c79c36c5e -r 7793d6423d01 doc-src/IsarImplementation/Thy/document/ML.tex
--- a/doc-src/IsarImplementation/Thy/document/ML.tex	Tue Dec 11 10:23:14 2007 +0100
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex	Wed Dec 12 09:00:07 2007 +0100
@@ -376,7 +376,7 @@
     \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
@@ -384,7 +384,7 @@
   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)|
@@ -403,7 +403,7 @@
 \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}%
@@ -440,7 +440,7 @@
   \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}
@@ -450,7 +450,7 @@
 \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}
 
@@ -460,7 +460,7 @@
 \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%
 
@@ -471,7 +471,7 @@
 \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}%
@@ -531,7 +531,7 @@
 \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}%