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/method.ML
changeset 9864 b4a170f7d658
parent 9777 232fb8886765
child 9900 8035a13c61a0 
--- a/src/Pure/Isar/method.ML	Tue Sep 05 18:51:25 2000 +0200
+++ b/src/Pure/Isar/method.ML	Tue Sep 05 18:51:49 2000 +0200
@@ -71,21 +71,20 @@
   type modifier
   val sectioned_args: (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list)) ->
     (Args.T list -> modifier * Args.T list) list ->
-    ('a -> Proof.context -> Proof.method) -> Args.src -> Proof.context -> Proof.method
+    ('a -> Proof.context -> 'b) -> Args.src -> Proof.context -> 'b
   val bang_sectioned_args:
     (Args.T list -> modifier * Args.T list) list ->
-    (thm list -> Proof.context -> Proof.method) -> Args.src -> Proof.context -> Proof.method
+    (thm list -> Proof.context -> 'a) -> Args.src -> Proof.context -> 'a
   val bang_sectioned_args':
     (Args.T list -> modifier * Args.T list) list ->
     (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list)) ->
-    ('a -> thm list -> Proof.context -> Proof.method) -> Args.src -> Proof.context -> Proof.method
+    ('a -> thm list -> Proof.context -> 'b) -> Args.src -> Proof.context -> 'b
   val only_sectioned_args:
     (Args.T list -> modifier * Args.T list) list ->
-    (Proof.context -> Proof.method) -> Args.src -> Proof.context -> Proof.method
-  val thms_ctxt_args: (thm list -> Proof.context -> Proof.method)
-    -> Args.src -> Proof.context -> Proof.method
-  val thms_args: (thm list -> Proof.method) -> Args.src -> Proof.context -> Proof.method
-  val thm_args: (thm -> Proof.method) -> Args.src -> Proof.context -> Proof.method
+    (Proof.context -> 'a) -> Args.src -> Proof.context -> 'a
+  val thms_ctxt_args: (thm list -> Proof.context -> 'a) -> Args.src -> Proof.context -> 'a
+  val thms_args: (thm list -> 'a) -> Args.src -> Proof.context -> 'a
+  val thm_args: (thm -> 'a) -> Args.src -> Proof.context -> 'a
   datatype text =
     Basic of (Proof.context -> Proof.method) |
     Source of Args.src |
isabelle