src/Provers/splitter.ML
changeset 9703 bf65780eed02
parent 9267 dbf30a2d1b56
child 9807 64b7f756c8f0
     1.1 --- a/src/Provers/splitter.ML	Mon Aug 28 20:29:19 2000 +0200
     1.2 +++ b/src/Provers/splitter.ML	Mon Aug 28 20:29:56 2000 +0200
     1.3 @@ -412,21 +412,22 @@
     1.4   (Attrib.add_del_args split_add_global split_del_global,
     1.5    Attrib.add_del_args split_add_local split_del_local);
     1.6  
     1.7 -val setup_attrs =
     1.8 -  Attrib.add_attributes [(splitN, split_attr, "declare splitter rule")];
     1.9  
    1.10 -
    1.11 -(* method modifiers *)
    1.12 +(* methods *)
    1.13  
    1.14  val split_modifiers =
    1.15   [Args.$$$ splitN -- Args.colon >> K ((I, split_add_local): Method.modifier),
    1.16    Args.$$$ splitN -- Args.$$$ "add" -- Args.colon >> K (I, split_add_local),
    1.17    Args.$$$ splitN -- Args.$$$ "del" -- Args.colon >> K (I, split_del_local)];
    1.18  
    1.19 +val split_meth = Method.thms_args (Method.SIMPLE_METHOD' HEADGOAL o split_tac);
    1.20 +
    1.21  
    1.22  
    1.23  (** theory setup **)
    1.24  
    1.25 -val setup = [setup_attrs];
    1.26 +val setup =
    1.27 + [Attrib.add_attributes [(splitN, split_attr, "declare splitter rule")],
    1.28 +  Method.add_methods [(splitN, split_meth, "apply splitter rule")]];
    1.29  
    1.30  end;