ProgTutorial/Helper/Command/ROOT.ML
author Christian Urban <urbanc@in.tum.de>
Thu, 01 Oct 2009 10:19:21 +0200
changeset 326 f76135c6c527
parent 320 185921021551
permissions -rw-r--r--
more work on the tutorial
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
320
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     1
(*
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     2
  no_document use_thys ["This_Theory1", "This_Theory2"];
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     3
  use_thys ["That_Theory1", "That_Theory2", "That_Theory3"];
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     4
*)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     5
no_document use_thy "Command";