equal
deleted
inserted
replaced
747 end; |
747 end; |
748 |
748 |
749 end; |
749 end; |
750 |
750 |
751 end; |
751 end; |
752 (* FIXME |
752 |
753 structure Local_Theory : LOCAL_THEORY = struct open Local_Theory; end; |
753 structure Local_Theory : LOCAL_THEORY = struct open Local_Theory; end; |
754 *) |
|