src/HOL/Tools/split_rule.ML
changeset 15661 9ef583b08647
parent 15574 b1d1b5bfc464
child 18050 652c95961a8b
equal deleted inserted replaced
15660:255055554c67 15661:9ef583b08647
     1 (*  Title:      Tools/split_rule.ML
     1 (*  Title:      Tools/split_rule.ML
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Stefan Berghofer, David von Oheimb, and Markus Wenzel, TU Muenchen
     3     Author:     Stefan Berghofer, David von Oheimb, and Markus Wenzel, TU Muenchen
     4 
     4 
     5 SOME tools for managing tupled arguments and abstractions in rules.
     5 Some tools for managing tupled arguments and abstractions in rules.
     6 *)
     6 *)
     7 
     7 
     8 signature BASIC_SPLIT_RULE =
     8 signature BASIC_SPLIT_RULE =
     9 sig
     9 sig
    10   val split_rule: thm -> thm
    10   val split_rule: thm -> thm
   128   end;
   128   end;
   129 
   129 
   130 
   130 
   131 (* attribute syntax *)
   131 (* attribute syntax *)
   132 
   132 
       
   133 (* FIXME dynamically scoped due to Args.name/pair_tac *)
       
   134 
   133 fun split_format x = Attrib.syntax
   135 fun split_format x = Attrib.syntax
   134   (Scan.lift (Args.parens (Args.$$$ "complete"))
   136   (Scan.lift (Args.parens (Args.$$$ "complete"))
   135     >> K (Drule.rule_attribute (K complete_split_rule)) ||
   137     >> K (Drule.rule_attribute (K complete_split_rule)) ||
   136   Args.and_list1 (Scan.lift (Scan.repeat Args.name))
   138   Args.and_list1 (Scan.lift (Scan.repeat Args.name))
   137     >> (fn xss => Drule.rule_attribute (K (split_rule_goal xss)))) x;
   139     >> (fn xss => Drule.rule_attribute (K (split_rule_goal xss)))) x;