| changeset 74561 | 8e6c973003c8 |
| parent 58061 | 3d060f43accb |
| child 78025 | 51d135645d70 |
| 74560:5c8177fd1295 | 74561:8e6c973003c8 |
|---|---|
14 |
14 |
15 structure Data = Generic_Data |
15 structure Data = Generic_Data |
16 ( |
16 ( |
17 type T = thm Net.net |
17 type T = thm Net.net |
18 val empty = Net.empty |
18 val empty = Net.empty |
19 val extend = I |
|
20 val merge = Net.merge Thm.eq_thm |
19 val merge = Net.merge Thm.eq_thm |
21 ) |
20 ) |
22 |
21 |
23 fun maybe_instantiate ct thm = |
22 fun maybe_instantiate ct thm = |
24 try Thm.first_order_match (Thm.cprop_of thm, ct) |
23 try Thm.first_order_match (Thm.cprop_of thm, ct) |