added add_method;
authorwenzelm
Thu Jun 29 22:31:29 2000 +0200 (2000-06-29)
changeset 9194a57987e0250b
parent 9193 4f4936582889
child 9195 29f1e53f9937
added add_method;
src/Pure/Isar/method.ML
     1.1 --- a/src/Pure/Isar/method.ML	Thu Jun 29 22:31:12 2000 +0200
     1.2 +++ b/src/Pure/Isar/method.ML	Thu Jun 29 22:31:29 2000 +0200
     1.3 @@ -55,6 +55,7 @@
     1.4    exception METHOD_FAIL of (string * Position.T) * exn
     1.5    val help_methods: theory option -> Pretty.T list
     1.6    val method: theory -> Args.src -> Proof.context -> Proof.method
     1.7 +  val add_method: bstring * (Args.src -> Proof.context -> Proof.method) * string -> theory -> theory
     1.8    val add_methods: (bstring * (Args.src -> Proof.context -> Proof.method) * string) list
     1.9      -> theory -> theory
    1.10    val syntax: (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list)) ->
    1.11 @@ -417,7 +418,7 @@
    1.12    in meth end;
    1.13  
    1.14  
    1.15 -(* add_methods *)
    1.16 +(* add_method(s) *)
    1.17  
    1.18  fun add_methods raw_meths thy =
    1.19    let
    1.20 @@ -433,6 +434,8 @@
    1.21      thy |> MethodsData.put {space = space', meths = meths'}
    1.22    end;
    1.23  
    1.24 +val add_method = add_methods o Library.single;
    1.25 +
    1.26  (*implicit version*)
    1.27  fun Method name meth cmt = Context.>> (add_methods [(name, meth, cmt)]);
    1.28