src/Pure/Isar/attrib.ML
changeset 35021 c839a4c670c6
parent 34986 7f7939c9370f
child 35624 c4e29a0bb8c1
equal deleted inserted replaced
35020:862a20ffa8e2 35021:c839a4c670c6
   296     (Scan.lift (Args.name -- Scan.repeat Args.name) >> Rule_Cases.case_conclusion)
   296     (Scan.lift (Args.name -- Scan.repeat Args.name) >> Rule_Cases.case_conclusion)
   297     "named conclusion of rule cases" #>
   297     "named conclusion of rule cases" #>
   298   setup (Binding.name "params")
   298   setup (Binding.name "params")
   299     (Scan.lift (P.and_list1 (Scan.repeat Args.name)) >> Rule_Cases.params)
   299     (Scan.lift (P.and_list1 (Scan.repeat Args.name)) >> Rule_Cases.params)
   300     "named rule parameters" #>
   300     "named rule parameters" #>
   301   setup (Binding.name "standard") (Scan.succeed (Thm.rule_attribute (K Drule.standard)))
   301   setup (Binding.name "standard") (Scan.succeed (Thm.rule_attribute (K Drule.export_without_context)))
   302     "result put into standard form (legacy)" #>
   302     "result put into standard form (legacy)" #>
   303   setup (Binding.name "rule_format") rule_format "result put into canonical rule format" #>
   303   setup (Binding.name "rule_format") rule_format "result put into canonical rule format" #>
   304   setup (Binding.name "elim_format") (Scan.succeed elim_format)
   304   setup (Binding.name "elim_format") (Scan.succeed elim_format)
   305     "destruct rule turned into elimination rule format" #>
   305     "destruct rule turned into elimination rule format" #>
   306   setup (Binding.name "no_vars") (Scan.succeed no_vars) "frozen schematic vars" #>
   306   setup (Binding.name "no_vars") (Scan.succeed no_vars) "frozen schematic vars" #>