Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
binding replaces bstring
authorhaftmann
Thu, 22 Jan 2009 09:04:45 +0100
changeset 29612 4f68e0f8f4fd
parent 29611 9891e3646809
child 29613 595d91e50510
binding replaces bstring
doc-src/IsarImplementation/Thy/ML.thy file | annotate | diff | comparison | revisions
doc-src/IsarImplementation/Thy/document/ML.tex file | annotate | diff | comparison | revisions 
--- a/doc-src/IsarImplementation/Thy/ML.thy	Wed Jan 21 23:42:37 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/ML.thy	Thu Jan 22 09:04:45 2009 +0100
@@ -319,7 +319,7 @@
   \smallskip\begin{mldecls}
   @{ML "Sign.declare_const: Properties.T -> (binding * typ) * mixfix
   -> theory -> term * theory"} \\
-  @{ML "Thm.add_def: bool -> bool -> bstring * term -> theory -> thm * theory"}
+  @{ML "Thm.add_def: bool -> bool -> binding * term -> theory -> thm * theory"}
   \end{mldecls}
 
   \noindent Written with naive application, an addition of constant
@@ -328,7 +328,7 @@
 
   \smallskip\begin{mldecls}
   @{ML "(fn (t, thy) => Thm.add_def false false
-  (\"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})) thy)
+  (Binding.name \"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})) thy)
     (Sign.declare_const []
       ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn) thy)"}
   \end{mldecls}
@@ -347,7 +347,7 @@
 |> Sign.declare_const [] ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
 |> (fn (t, thy) => thy
 |> Thm.add_def false false
-     (\"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})))"}
+     (Binding.name \"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})))"}
   \end{mldecls}
 *}
 
@@ -370,7 +370,7 @@
 @{ML "thy
 |> Sign.declare_const [] ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
 |-> (fn t => Thm.add_def false false
-      (\"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})))
+      (Binding.name \"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})))
 "}
   \end{mldecls}
 
@@ -380,7 +380,7 @@
 @{ML "thy
 |> Sign.declare_const [] ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
 |>> (fn t => Logic.mk_equals (t, @{term \"%x. x\"}))
-|-> (fn def => Thm.add_def false false (\"bar_def\", def))
+|-> (fn def => Thm.add_def false false (Binding.name \"bar_def\", def))
 "}
   \end{mldecls}
 
@@ -392,7 +392,7 @@
 |> Sign.declare_const [] ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
 ||> Sign.add_path \"foobar\"
 |-> (fn t => Thm.add_def false false
-      (\"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})))
+      (Binding.name \"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})))
 ||> Sign.restore_naming thy
 "}
   \end{mldecls}
@@ -404,7 +404,7 @@
 |> Sign.declare_const [] ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
 ||>> Sign.declare_const [] ((Binding.name \"foobar\", @{typ \"foo => foo\"}), NoSyn)
 |-> (fn (t1, t2) => Thm.add_def false false
-      (\"bar_def\", Logic.mk_equals (t1, t2)))
+      (Binding.name \"bar_def\", Logic.mk_equals (t1, t2)))
 "}
   \end{mldecls}
 *}
@@ -451,7 +451,7 @@
        ((Binding.name 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 false (\"\", def)) defs)
+       Thm.add_def false false (Binding.empty, def)) defs)
 end"}
   \end{mldecls}
 *}
--- a/doc-src/IsarImplementation/Thy/document/ML.tex	Wed Jan 21 23:42:37 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex	Thu Jan 22 09:04:45 2009 +0100
@@ -368,7 +368,7 @@
   \smallskip\begin{mldecls}
   \verb|Sign.declare_const: Properties.T -> (binding * typ) * mixfix|\isasep\isanewline%
 \verb|  -> theory -> term * theory| \\
-  \verb|Thm.add_def: bool -> bool -> bstring * term -> theory -> thm * theory|
+  \verb|Thm.add_def: bool -> bool -> binding * term -> theory -> thm * theory|
   \end{mldecls}
 
   \noindent Written with naive application, an addition of constant
@@ -377,7 +377,7 @@
 
   \smallskip\begin{mldecls}
   \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|  (Binding.name "bar_def", Logic.mk_equals (t, @{term "%x. x"})) thy)|\isasep\isanewline%
 \verb|    (Sign.declare_const []|\isasep\isanewline%
 \verb|      ((Binding.name "bar", @{typ "foo => foo"}), NoSyn) thy)|
   \end{mldecls}
@@ -397,7 +397,7 @@
 \verb||\verb,|,\verb|> Sign.declare_const [] ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
 \verb||\verb,|,\verb|> (fn (t, thy) => thy|\isasep\isanewline%
 \verb||\verb,|,\verb|> Thm.add_def false false|\isasep\isanewline%
-\verb|     ("bar_def", Logic.mk_equals (t, @{term "%x. x"})))|
+\verb|     (Binding.name "bar_def", Logic.mk_equals (t, @{term "%x. x"})))|
   \end{mldecls}%
 \end{isamarkuptext}%
 \isamarkuptrue%
@@ -435,7 +435,7 @@
 \verb|thy|\isasep\isanewline%
 \verb||\verb,|,\verb|> Sign.declare_const [] ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\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|      (Binding.name "bar_def", Logic.mk_equals (t, @{term "%x. x"})))|\isasep\isanewline%
 
   \end{mldecls}
 
@@ -445,7 +445,7 @@
 \verb|thy|\isasep\isanewline%
 \verb||\verb,|,\verb|> Sign.declare_const [] ((Binding.name "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 false ("bar_def", def))|\isasep\isanewline%
+\verb||\verb,|,\verb|-> (fn def => Thm.add_def false false (Binding.name "bar_def", def))|\isasep\isanewline%
 
   \end{mldecls}
 
@@ -457,7 +457,7 @@
 \verb||\verb,|,\verb|> Sign.declare_const [] ((Binding.name "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 false|\isasep\isanewline%
-\verb|      ("bar_def", Logic.mk_equals (t, @{term "%x. x"})))|\isasep\isanewline%
+\verb|      (Binding.name "bar_def", Logic.mk_equals (t, @{term "%x. x"})))|\isasep\isanewline%
 \verb||\verb,|,\verb||\verb,|,\verb|> Sign.restore_naming thy|\isasep\isanewline%
 
   \end{mldecls}
@@ -469,7 +469,7 @@
 \verb||\verb,|,\verb|> Sign.declare_const [] ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
 \verb||\verb,|,\verb||\verb,|,\verb|>> Sign.declare_const [] ((Binding.name "foobar", @{typ "foo => foo"}), NoSyn)|\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%
+\verb|      (Binding.name "bar_def", Logic.mk_equals (t1, t2)))|\isasep\isanewline%
 
   \end{mldecls}%
 \end{isamarkuptext}%
@@ -531,7 +531,7 @@
 \verb|       ((Binding.name 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 false ("", def)) defs)|\isasep\isanewline%
+\verb|       Thm.add_def false false (Binding.empty, def)) defs)|\isasep\isanewline%
 \verb|end|
   \end{mldecls}%
 \end{isamarkuptext}%
isabelle