equal
deleted
inserted
replaced
7 signature SPLIT_RULE = |
7 signature SPLIT_RULE = |
8 sig |
8 sig |
9 val split_rule_var: Proof.context -> term -> thm -> thm |
9 val split_rule_var: Proof.context -> term -> thm -> thm |
10 val split_rule: Proof.context -> thm -> thm |
10 val split_rule: Proof.context -> thm -> thm |
11 val complete_split_rule: Proof.context -> thm -> thm |
11 val complete_split_rule: Proof.context -> thm -> thm |
12 val setup: theory -> theory |
|
13 end; |
12 end; |
14 |
13 |
15 structure Split_Rule: SPLIT_RULE = |
14 structure Split_Rule: SPLIT_RULE = |
16 struct |
15 struct |
17 |
16 |
108 end; |
107 end; |
109 |
108 |
110 |
109 |
111 (* attribute syntax *) |
110 (* attribute syntax *) |
112 |
111 |
113 val setup = |
112 val _ = |
114 Attrib.setup @{binding split_format} |
113 Theory.setup |
115 (Scan.lift (Args.parens (Args.$$$ "complete") |
114 (Attrib.setup @{binding split_format} |
116 >> K (Thm.rule_attribute (complete_split_rule o Context.proof_of)))) |
115 (Scan.lift (Args.parens (Args.$$$ "complete") |
117 "split pair-typed subterms in premises, or function arguments" #> |
116 >> K (Thm.rule_attribute (complete_split_rule o Context.proof_of)))) |
118 Attrib.setup @{binding split_rule} |
117 "split pair-typed subterms in premises, or function arguments" #> |
119 (Scan.succeed (Thm.rule_attribute (split_rule o Context.proof_of))) |
118 Attrib.setup @{binding split_rule} |
120 "curries ALL function variables occurring in a rule's conclusion"; |
119 (Scan.succeed (Thm.rule_attribute (split_rule o Context.proof_of))) |
|
120 "curries ALL function variables occurring in a rule's conclusion"); |
121 |
121 |
122 end; |
122 end; |
123 |
123 |