equal
deleted
inserted
replaced
128 | _ => th; |
128 | _ => th; |
129 |
129 |
130 fun try_rewrite th = temp_rewrite th handle THM _ => temp_use th; |
130 fun try_rewrite th = temp_rewrite th handle THM _ => temp_use th; |
131 *} |
131 *} |
132 |
132 |
133 setup {* |
133 attribute_setup temp_unlift = {* Scan.succeed (Thm.rule_attribute (K temp_unlift)) *} "" |
134 Attrib.add_attributes [ |
134 attribute_setup temp_rewrite = {* Scan.succeed (Thm.rule_attribute (K temp_rewrite)) *} "" |
135 ("temp_unlift", Attrib.no_args (Thm.rule_attribute (K temp_unlift)), ""), |
135 attribute_setup temp_use = {* Scan.succeed (Thm.rule_attribute (K temp_use)) *} "" |
136 ("temp_rewrite", Attrib.no_args (Thm.rule_attribute (K temp_rewrite)), ""), |
136 attribute_setup try_rewrite = {* Scan.succeed (Thm.rule_attribute (K try_rewrite)) *} "" |
137 ("temp_use", Attrib.no_args (Thm.rule_attribute (K temp_use)), ""), |
137 |
138 ("try_rewrite", Attrib.no_args (Thm.rule_attribute (K try_rewrite)), "")] |
|
139 *} |
|
140 |
138 |
141 (* Update classical reasoner---will be updated once more below! *) |
139 (* Update classical reasoner---will be updated once more below! *) |
142 |
140 |
143 declare tempI [intro!] |
141 declare tempI [intro!] |
144 declare tempD [dest] |
142 declare tempD [dest] |