equal
deleted
inserted
replaced
663 |
663 |
664 structure Proofs = Theory_Data |
664 structure Proofs = Theory_Data |
665 ( |
665 ( |
666 type T = thm list lazy Inttab.table; |
666 type T = thm list lazy Inttab.table; |
667 val empty = Inttab.empty; |
667 val empty = Inttab.empty; |
668 val extend = I; |
|
669 val merge = Inttab.merge (K true); |
668 val merge = Inttab.merge (K true); |
670 ); |
669 ); |
671 |
670 |
672 fun reset_proofs thy = |
671 fun reset_proofs thy = |
673 if Inttab.is_empty (Proofs.get thy) then NONE |
672 if Inttab.is_empty (Proofs.get thy) then NONE |