ProgTutorial/Helper/Command/ROOT.ML
author Christian Urban <urbanc@in.tum.de>
Thu, 01 Oct 2009 10:19:21 +0200 (2009-10-01)
changeset 326 f76135c6c527
parent 320 185921021551
permissions -rw-r--r--
more work on the tutorial
(*
  no_document use_thys ["This_Theory1", "This_Theory2"];
  use_thys ["That_Theory1", "That_Theory2", "That_Theory3"];
*)
no_document use_thy "Command";