simplified 'split_format' syntax;
authorwenzelm
Sat Feb 03 00:01:54 2001 +0100 (2001-02-03)
changeset 11040194406da4e43
parent 11039 55de839f4850
child 11041 e07b601e2b5a
simplified 'split_format' syntax;
src/HOL/MicroJava/J/Eval.thy
src/HOL/Tools/split_rule.ML
     1.1 --- a/src/HOL/MicroJava/J/Eval.thy	Fri Feb 02 23:59:30 2001 +0100
     1.2 +++ b/src/HOL/MicroJava/J/Eval.thy	Sat Feb 03 00:01:54 2001 +0100
     1.3 @@ -139,7 +139,7 @@
     1.4  	    G\<turnstile>s1 -c-> s2; G\<turnstile>s2 -While(e) c-> s3 |] ==>
     1.5           G\<turnstile>Norm s0 -While(e) c-> s3"
     1.6  
     1.7 -lemmas eval_evals_exec_induct = eval_evals_exec.induct [complete_split]
     1.8 +lemmas eval_evals_exec_induct = eval_evals_exec.induct [split_format (complete)]
     1.9  
    1.10  lemma NewCI: "[|new_Addr (heap s) = (a,x);  
    1.11         s' = c_hupd (heap s(a\<mapsto>(C,init_vars (fields (G,C))))) (x,s)|] ==>  
     2.1 --- a/src/HOL/Tools/split_rule.ML	Fri Feb 02 23:59:30 2001 +0100
     2.2 +++ b/src/HOL/Tools/split_rule.ML	Sat Feb 03 00:01:54 2001 +0100
     2.3 @@ -127,26 +127,15 @@
     2.4  
     2.5  (* attribute syntax *)
     2.6  
     2.7 -fun complete_split x =
     2.8 -  Attrib.no_args (Drule.rule_attribute (K complete_split_rule)) x;
     2.9 -
    2.10 -fun split_format x =
    2.11 -  Attrib.syntax (Args.and_list1 (Scan.lift (Scan.repeat Args.name))
    2.12 -    >> (fn xss => Drule.rule_attribute (K (split_rule_goal xss)))) x;
    2.13 -
    2.14 -val split_attributes =
    2.15 - [("complete_split", (complete_split, complete_split),
    2.16 -    "recursively split all pair-typed function arguments"),
    2.17 -  ("split_format", (split_format, split_format),
    2.18 -    "split given pair-typed subterms in premises")];
    2.19 -
    2.20 -
    2.21 -
    2.22 -(** theory setup **)
    2.23 +fun split_format x = Attrib.syntax
    2.24 +  (Args.mode "complete" >> K (Drule.rule_attribute (K complete_split_rule)) ||
    2.25 +    Args.and_list1 (Scan.lift (Scan.repeat Args.name))
    2.26 +      >> (fn xss => Drule.rule_attribute (K (split_rule_goal xss)))) x;
    2.27  
    2.28  val setup =
    2.29 - [Attrib.add_attributes split_attributes];
    2.30 -
    2.31 + [Attrib.add_attributes
    2.32 +  [("split_format", (split_format, split_format),
    2.33 +    "split pair-typed subterms in premises, or function arguments")]];
    2.34  
    2.35  end;
    2.36