Quot/ROOT.ML
changeset 603 7f35355df72e
parent 601 81f40b8bde7b
child 604 0cf166548856
equal deleted inserted replaced
602:e56eeb9fedb3 603:7f35355df72e
     1 (*
     1 no_document use_thys 
     2   no_document use_thys ["This_Theory1", "This_Theory2"];
     2    ["QuotMain",
     3   use_thys ["That_Theory1", "That_Theory2", "That_Theory3"];
     3     "Examples/Fset",
     4 *)
     4     "Examples/IntEx",
       
     5     "Examples/IntEx2",
       
     6     "Examples/LFex",
       
     7     "Examples/LamEx"];
       
     8