--- a/src/Pure/Pure.thy Thu Apr 07 12:08:02 2016 +0200
+++ b/src/Pure/Pure.thy Thu Apr 07 12:13:11 2016 +0200
@@ -1281,109 +1281,6 @@
in end\<close>
-section \<open>Isar attributes\<close>
-
-attribute_setup tagged =
- \<open>Scan.lift (Args.name -- Args.name) >> Thm.tag\<close>
- "tagged theorem"
-
-attribute_setup untagged =
- \<open>Scan.lift Args.name >> Thm.untag\<close>
- "untagged theorem"
-
-attribute_setup kind =
- \<open>Scan.lift Args.name >> Thm.kind\<close>
- "theorem kind"
-
-attribute_setup THEN =
- \<open>Scan.lift (Scan.optional (Args.bracks Parse.nat) 1) -- Attrib.thm
- >> (fn (i, B) => Thm.rule_attribute [B] (fn _ => fn A => A RSN (i, B)))\<close>
- "resolution with rule"
-
-attribute_setup OF =
- \<open>Attrib.thms >> (fn Bs => Thm.rule_attribute Bs (fn _ => fn A => A OF Bs))\<close>
- "rule resolved with facts"
-
-attribute_setup rename_abs =
- \<open>Scan.lift (Scan.repeat (Args.maybe Args.name)) >> (fn vs =>
- Thm.rule_attribute [] (K (Drule.rename_bvars' vs)))\<close>
- "rename bound variables in abstractions"
-
-attribute_setup unfolded =
- \<open>Attrib.thms >> (fn ths =>
- Thm.rule_attribute ths (fn context => Local_Defs.unfold (Context.proof_of context) ths))\<close>
- "unfolded definitions"
-
-attribute_setup folded =
- \<open>Attrib.thms >> (fn ths =>
- Thm.rule_attribute ths (fn context => Local_Defs.fold (Context.proof_of context) ths))\<close>
- "folded definitions"
-
-attribute_setup consumes =
- \<open>Scan.lift (Scan.optional Parse.int 1) >> Rule_Cases.consumes\<close>
- "number of consumed facts"
-
-attribute_setup constraints =
- \<open>Scan.lift Parse.nat >> Rule_Cases.constraints\<close>
- "number of equality constraints"
-
-attribute_setup case_names =
- \<open>Scan.lift (Scan.repeat1 (Args.name --
- Scan.optional (@{keyword "["} |-- Scan.repeat1 (Args.maybe Args.name) --| @{keyword "]"}) []))
- >> (fn cs =>
- Rule_Cases.cases_hyp_names
- (map #1 cs)
- (map (map (the_default Rule_Cases.case_hypsN) o #2) cs))\<close>
- "named rule cases"
-
-attribute_setup case_conclusion =
- \<open>Scan.lift (Args.name -- Scan.repeat Args.name) >> Rule_Cases.case_conclusion\<close>
- "named conclusion of rule cases"
-
-attribute_setup params =
- \<open>Scan.lift (Parse.and_list1 (Scan.repeat Args.name)) >> Rule_Cases.params\<close>
- "named rule parameters"
-
-attribute_setup rule_format =
- \<open>Scan.lift (Args.mode "no_asm")
- >> (fn true => Object_Logic.rule_format_no_asm | false => Object_Logic.rule_format)\<close>
- "result put into canonical rule format"
-
-attribute_setup elim_format =
- \<open>Scan.succeed (Thm.rule_attribute [] (K Tactic.make_elim))\<close>
- "destruct rule turned into elimination rule format"
-
-attribute_setup no_vars =
- \<open>Scan.succeed (Thm.rule_attribute [] (fn context => fn th =>
- let
- val ctxt = Variable.set_body false (Context.proof_of context);
- val ((_, [th']), _) = Variable.import true [th] ctxt;
- in th' end))\<close>
- "imported schematic variables"
-
-attribute_setup atomize =
- \<open>Scan.succeed Object_Logic.declare_atomize\<close>
- "declaration of atomize rule"
-
-attribute_setup rulify =
- \<open>Scan.succeed Object_Logic.declare_rulify\<close>
- "declaration of rulify rule"
-
-attribute_setup rotated =
- \<open>Scan.lift (Scan.optional Parse.int 1
- >> (fn n => Thm.rule_attribute [] (fn _ => rotate_prems n)))\<close>
- "rotated theorem premises"
-
-attribute_setup defn =
- \<open>Attrib.add_del Local_Defs.defn_add Local_Defs.defn_del\<close>
- "declaration of definitional transformations"
-
-attribute_setup abs_def =
- \<open>Scan.succeed (Thm.rule_attribute [] (fn context =>
- Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def))\<close>
- "abstract over free variables of definitional theorem"
-
-
section \<open>Further content for the Pure theory\<close>
subsection \<open>Meta-level connectives in assumptions\<close>