changeset 601 | 81f40b8bde7b |
parent 597 | 8a1c8dc72b5c |
child 604 | 0cf166548856 |
--- a/Quot/ROOT.ML Mon Dec 07 14:35:45 2009 +0100 +++ b/Quot/ROOT.ML Mon Dec 07 14:37:10 2009 +0100 @@ -1,4 +1,8 @@ -(* - no_document use_thys ["This_Theory1", "This_Theory2"]; - use_thys ["That_Theory1", "That_Theory2", "That_Theory3"]; -*) +no_document use_thys + ["QuotMain", + "Examples/Fset", + "Examples/IntEx", + "Examples/IntEx2", + "Examples/LFex", + "Examples/LamEx"]; +