| changeset 15647 | b1f486a9c56b |
| parent 15570 | 8d8c70b41bab |
| child 16424 | 18a07ad8fea8 |
| 15646:b45393fb38c0 | 15647:b1f486a9c56b |
|---|---|
494 in |
494 in |
495 thy2 |
495 thy2 |
496 end; |
496 end; |
497 |
497 |
498 fun setup_dump (dir,thyname) thy = |
498 fun setup_dump (dir,thyname) thy = |
499 HOL4Dump.put (dir,thyname,[]) thy |
499 HOL4Dump.put (dir,thyname,["(* AUTOMATICALLY GENERATED, DO NOT EDIT! *)"]) thy |
500 |
500 |
501 fun add_dump str thy = |
501 fun add_dump str thy = |
502 let |
502 let |
503 val (dir,thyname,curdump) = HOL4Dump.get thy |
503 val (dir,thyname,curdump) = HOL4Dump.get thy |
504 in |
504 in |