src/Provers/splitter.ML
changeset 18688 abf0f018b5ec
parent 18545 e2b09fda748c
child 18708 4b3dadb4fe33
     1.1 --- a/src/Provers/splitter.ML	Sat Jan 14 17:20:51 2006 +0100
     1.2 +++ b/src/Provers/splitter.ML	Sat Jan 14 22:25:34 2006 +0100
     1.3 @@ -32,10 +32,8 @@
     1.4    val delsplits       : simpset * thm list -> simpset
     1.5    val Addsplits       : thm list -> unit
     1.6    val Delsplits       : thm list -> unit
     1.7 -  val split_add_global: theory attribute
     1.8 -  val split_del_global: theory attribute
     1.9 -  val split_add_local: Proof.context attribute
    1.10 -  val split_del_local: Proof.context attribute
    1.11 +  val split_add: Context.generic attribute
    1.12 +  val split_del: Context.generic attribute
    1.13    val split_modifiers : (Args.T list -> (Method.modifier * Args.T list)) list
    1.14    val setup: (theory -> theory) list
    1.15  end;
    1.16 @@ -405,6 +403,7 @@
    1.17           gen_split_tac splits
    1.18        end;
    1.19  
    1.20 +
    1.21  (** declare split rules **)
    1.22  
    1.23  (* addsplits / delsplits *)
    1.24 @@ -437,33 +436,28 @@
    1.25  
    1.26  val splitN = "split";
    1.27  
    1.28 -val split_add_global = Simplifier.change_global_ss (op addsplits);
    1.29 -val split_del_global = Simplifier.change_global_ss (op delsplits);
    1.30 -val split_add_local = Simplifier.change_local_ss (op addsplits);
    1.31 -val split_del_local = Simplifier.change_local_ss (op delsplits);
    1.32 -
    1.33 -val split_attr =
    1.34 - (Attrib.add_del_args split_add_global split_del_global,
    1.35 -  Attrib.add_del_args split_add_local split_del_local);
    1.36 +val split_add = Simplifier.attrib (op addsplits);
    1.37 +val split_del = Simplifier.attrib (op delsplits);
    1.38  
    1.39  
    1.40  (* methods *)
    1.41  
    1.42  val split_modifiers =
    1.43 - [Args.$$$ splitN -- Args.colon >> K ((I, split_add_local): Method.modifier),
    1.44 -  Args.$$$ splitN -- Args.add -- Args.colon >> K (I, split_add_local),
    1.45 -  Args.$$$ splitN -- Args.del -- Args.colon >> K (I, split_del_local)];
    1.46 + [Args.$$$ splitN -- Args.colon >> K ((I, Attrib.context split_add): Method.modifier),
    1.47 +  Args.$$$ splitN -- Args.add -- Args.colon >> K (I, Attrib.context split_add),
    1.48 +  Args.$$$ splitN -- Args.del -- Args.colon >> K (I, Attrib.context split_del)];
    1.49  
    1.50 -val split_args = #2 oo Method.syntax Attrib.local_thms;
    1.51 -
    1.52 -fun split_meth ths = Method.SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o gen_split_tac ths);
    1.53 +fun split_meth src =
    1.54 +  Method.syntax Attrib.local_thms src
    1.55 +  #> (fn (_, ths) => Method.SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o gen_split_tac ths));
    1.56  
    1.57  
    1.58 -
    1.59 -(** theory setup **)
    1.60 +(* theory setup *)
    1.61  
    1.62  val setup =
    1.63 - [Attrib.add_attributes [(splitN, split_attr, "declaration of case split rule")],
    1.64 -  Method.add_methods [(splitN, split_meth oo split_args, "apply case split rule")]];
    1.65 + [Attrib.add_attributes
    1.66 +  [(splitN, Attrib.common (Attrib.add_del_args split_add split_del),
    1.67 +    "declaration of case split rule")],
    1.68 +  Method.add_methods [(splitN, split_meth, "apply case split rule")]];
    1.69  
    1.70  end;