equal
deleted
inserted
replaced
194 |
194 |
195 |
195 |
196 (* setup *) |
196 (* setup *) |
197 |
197 |
198 val setup = |
198 val setup = |
199 Attrib.add_attributes |
199 Attrib.setup @{binding fundef_cong} (Attrib.add_del FundefCtxTree.cong_add FundefCtxTree.cong_del) |
200 [("fundef_cong", Attrib.add_del_args FundefCtxTree.cong_add FundefCtxTree.cong_del, |
200 "declaration of congruence rule for function definitions" |
201 "declaration of congruence rule for function definitions")] |
|
202 #> setup_case_cong |
201 #> setup_case_cong |
203 #> FundefRelation.setup |
202 #> FundefRelation.setup |
204 #> FundefCommon.TerminationSimps.setup |
203 #> FundefCommon.TerminationSimps.setup |
205 |
204 |
206 val get_congs = FundefCtxTree.get_fundef_congs |
205 val get_congs = FundefCtxTree.get_fundef_congs |