src/HOLCF/ex/ROOT.ML
author huffman
Mon, 24 May 2010 11:29:49 -0700
changeset 37109 e67760c1b851
parent 37000 41a22e7c1145
child 37110 7ffdbc24b27f
permissions -rw-r--r--
move unused pattern match syntax stuff into HOLCF/ex

(*  Title:      HOLCF/ex/ROOT.ML

Misc HOLCF examples.
*)

use_thys ["Dnat", "Stream", "Dagstuhl", "Focus_ex", "Fix2", "Hoare",
  "Loop", "Powerdomain_ex", "Domain_Proofs",
  "Letrec",
  "Pattern_Match",
  "Strict_Fun"];