changeset 36864 | 116be5acd5a7 |
parent 36610 | bafd82950e24 |
child 36954 | ef698bd61057 |
36863:6637878680b0 | 36864:116be5acd5a7 |
---|---|
17 |
17 |
18 (* theory data *) |
18 (* theory data *) |
19 |
19 |
20 structure IndCasesData = Theory_Data |
20 structure IndCasesData = Theory_Data |
21 ( |
21 ( |
22 type T = (Proof.context -> cterm -> thm) Symtab.table; |
22 type T = (Proof.context -> conv) Symtab.table; |
23 val empty = Symtab.empty; |
23 val empty = Symtab.empty; |
24 val extend = I; |
24 val extend = I; |
25 fun merge data = Symtab.merge (K true) data; |
25 fun merge data = Symtab.merge (K true) data; |
26 ); |
26 ); |
27 |
27 |