src/HOL/HOLCF/ex/ROOT.ML
author kuncar
Fri Dec 09 18:07:04 2011 +0100 (2011-12-09)
changeset 45802 b16f976db515
parent 43524 d75e285fcf3e
permissions -rw-r--r--
Quotient_Info stores only relation maps
wenzelm@42151
     1
(*  Title:      HOL/HOLCF/ex/ROOT.ML
nipkow@244
     2
wenzelm@9000
     3
Misc HOLCF examples.
nipkow@244
     4
*)
nipkow@244
     5
huffman@37110
     6
use_thys ["Dnat", "Dagstuhl", "Focus_ex", "Fix2", "Hoare",
huffman@43524
     7
  "Concurrency_Monad",
huffman@37000
     8
  "Loop", "Powerdomain_ex", "Domain_Proofs",
huffman@35932
     9
  "Letrec",
huffman@37110
    10
  "Pattern_Match"];