Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Isar/isar_cmd.ML
changeset 49889 00ea087e83d8
parent 49866 619acbd72664
child 50737 f310d1735d93 
--- a/src/Pure/Isar/isar_cmd.ML	Wed Oct 17 10:46:14 2012 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Wed Oct 17 13:20:08 2012 +0200
@@ -30,8 +30,8 @@
   val hence: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
   val show: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
   val thus: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
-  val qed: Method.text_position option -> Toplevel.transition -> Toplevel.transition
-  val terminal_proof: Method.text_position * Method.text_position option ->
+  val qed: Method.text_range option -> Toplevel.transition -> Toplevel.transition
+  val terminal_proof: Method.text_range * Method.text_range option ->
     Toplevel.transition -> Toplevel.transition
   val default_proof: Toplevel.transition -> Toplevel.transition
   val immediate_proof: Toplevel.transition -> Toplevel.transition
isabelle