equal
deleted
inserted
replaced
277 val setup_case_cong = Datatype_Data.interpretation (K (fold add_case_cong)) |
277 val setup_case_cong = Datatype_Data.interpretation (K (fold add_case_cong)) |
278 |
278 |
279 |
279 |
280 (* setup *) |
280 (* setup *) |
281 |
281 |
282 val setup = |
282 val setup = setup_case_cong |
283 setup_case_cong |
|
284 #> Function_Common.Termination_Simps.setup |
|
285 |
283 |
286 val get_congs = Function_Ctx_Tree.get_function_congs |
284 val get_congs = Function_Ctx_Tree.get_function_congs |
287 |
285 |
288 fun get_info ctxt t = Item_Net.retrieve (get_function ctxt) t |
286 fun get_info ctxt t = Item_Net.retrieve (get_function ctxt) t |
289 |> the_single |> snd |
287 |> the_single |> snd |