equal
deleted
inserted
replaced
38 eqns = merge_rules (eqns1, eqns2)}; |
38 eqns = merge_rules (eqns1, eqns2)}; |
39 ); |
39 ); |
40 |
40 |
41 |
41 |
42 fun warn thm = warning ("InductiveCodegen: Not a proper clause:\n" ^ |
42 fun warn thm = warning ("InductiveCodegen: Not a proper clause:\n" ^ |
43 string_of_thm thm); |
43 Display.string_of_thm thm); |
44 |
44 |
45 fun add_node (g, x) = Graph.new_node (x, ()) g handle Graph.DUP _ => g; |
45 fun add_node (g, x) = Graph.new_node (x, ()) g handle Graph.DUP _ => g; |
46 |
46 |
47 fun add optmod optnparms = Thm.declaration_attribute (fn thm => Context.mapping (fn thy => |
47 fun add optmod optnparms = Thm.declaration_attribute (fn thm => Context.mapping (fn thy => |
48 let |
48 let |