equal
deleted
inserted
replaced
74 else |
74 else |
75 let val conjs = Logic.dest_conjunctions (Thm.major_prem_of thm); |
75 let val conjs = Logic.dest_conjunctions (Thm.major_prem_of thm); |
76 in Conjunction.curry_balanced (length conjs) thm end; |
76 in Conjunction.curry_balanced (length conjs) thm end; |
77 \<close> |
77 \<close> |
78 |
78 |
79 attribute_setup uncurry = \<open>Scan.succeed (Thm.rule_attribute (K uncurry_rule))\<close> |
79 attribute_setup uncurry = \<open>Scan.succeed (Thm.rule_attribute [] (K uncurry_rule))\<close> |
80 attribute_setup curry = \<open>Scan.succeed (Thm.rule_attribute (K curry_rule))\<close> |
80 attribute_setup curry = \<open>Scan.succeed (Thm.rule_attribute [] (K curry_rule))\<close> |
81 |
81 |
82 end |
82 end |