ProgTutorial/Helper/Command/ROOT.ML
author Christian Urban <urbanc@in.tum.de>
Mon, 14 Nov 2011 20:30:46 +0000
changeset 499 42bac8b16951
parent 320 185921021551
permissions -rw-r--r--
more on contexts

(*
  no_document use_thys ["This_Theory1", "This_Theory2"];
  use_thys ["That_Theory1", "That_Theory2", "That_Theory3"];
*)
no_document use_thy "Command";