src/Pure/Isar/attrib.ML
changeset 44046 a43ca8ed6564
parent 43347 f18cf88453d6
child 44053 3cc902f81a26
equal deleted inserted replaced
44045:2814ff2a6e3e 44046:a43ca8ed6564
   265   >> (fn true => Object_Logic.rule_format_no_asm | false => Object_Logic.rule_format);
   265   >> (fn true => Object_Logic.rule_format_no_asm | false => Object_Logic.rule_format);
   266 
   266 
   267 val elim_format = Thm.rule_attribute (K Tactic.make_elim);
   267 val elim_format = Thm.rule_attribute (K Tactic.make_elim);
   268 
   268 
   269 
   269 
       
   270 (* case names *)
       
   271 
       
   272 fun hname NONE = Rule_Cases.case_hypsN
       
   273   | hname (SOME n) = n;
       
   274 
       
   275 fun case_names cs =
       
   276   Rule_Cases.case_names (map fst cs) #>
       
   277   Rule_Cases.cases_hyp_names (map (map hname o snd) cs)
       
   278 
       
   279 val hnamesP =
       
   280   Scan.optional
       
   281     (Parse.$$$ "[" |-- Scan.repeat1 (Args.maybe Args.name) --| Parse.$$$ "]")
       
   282     []
       
   283 
       
   284 val case_namesP = Scan.lift (Scan.repeat1 (Args.name -- hnamesP))
       
   285 
   270 (* misc rules *)
   286 (* misc rules *)
   271 
   287 
   272 val no_vars = Thm.rule_attribute (fn context => fn th =>
   288 val no_vars = Thm.rule_attribute (fn context => fn th =>
   273   let
   289   let
   274     val ctxt = Variable.set_body false (Context.proof_of context);
   290     val ctxt = Variable.set_body false (Context.proof_of context);
   298   setup (Binding.name "folded") folded "folded definitions" #>
   314   setup (Binding.name "folded") folded "folded definitions" #>
   299   setup (Binding.name "consumes") (Scan.lift (Scan.optional Parse.nat 1) >> Rule_Cases.consumes)
   315   setup (Binding.name "consumes") (Scan.lift (Scan.optional Parse.nat 1) >> Rule_Cases.consumes)
   300     "number of consumed facts" #>
   316     "number of consumed facts" #>
   301   setup (Binding.name "constraints") (Scan.lift Parse.nat >> Rule_Cases.constraints)
   317   setup (Binding.name "constraints") (Scan.lift Parse.nat >> Rule_Cases.constraints)
   302     "number of equality constraints" #>
   318     "number of equality constraints" #>
   303   setup (Binding.name "case_names") (Scan.lift (Scan.repeat1 Args.name) >> Rule_Cases.case_names)
   319   setup (Binding.name "case_names") (case_namesP >> case_names)
   304     "named rule cases" #>
   320     "named rule cases" #>
   305   setup (Binding.name "case_conclusion")
   321   setup (Binding.name "case_conclusion")
   306     (Scan.lift (Args.name -- Scan.repeat Args.name) >> Rule_Cases.case_conclusion)
   322     (Scan.lift (Args.name -- Scan.repeat Args.name) >> Rule_Cases.case_conclusion)
   307     "named conclusion of rule cases" #>
   323     "named conclusion of rule cases" #>
   308   setup (Binding.name "params")
   324   setup (Binding.name "params")