tphols-2011/ROOT.ML
author urbanc
Fri, 05 Aug 2011 05:34:11 +0000 (2011-08-05)
changeset 187 9f46a9571e37
parent 42 f809cb54de4e
permissions -rw-r--r--
more on the derivatives section
(*
  no_document use_thys ["This_Theory1", "This_Theory2"];
  use_thys ["That_Theory1", "That_Theory2", "That_Theory3"];
*)
  use_thys ["../Myhill"];