changeset 4784 | 06556ca5036d |
parent 4741 | 7fcd106cb0ed |
child 4795 | 721b532ada7a |
4783:ca29125de4af | 4784:06556ca5036d |
---|---|
248 |
248 |
249 (** simpset theory data **) |
249 (** simpset theory data **) |
250 |
250 |
251 (* data kind simpset *) |
251 (* data kind simpset *) |
252 |
252 |
253 val simpsetK = "simpset"; |
253 val simpsetK = "Provers/simpset"; |
254 exception SimpsetData of simpset ref; |
254 exception SimpsetData of simpset ref; |
255 |
255 |
256 local |
256 local |
257 val empty = SimpsetData (ref empty_ss); |
257 val empty = SimpsetData (ref empty_ss); |
258 |
258 |