src/HOLCF/ex/ROOT.ML
author huffman
Wed Feb 17 08:05:16 2010 -0800 (2010-02-17)
changeset 35167 eba22d68a0a7
parent 33813 0bc8d4f786bd
child 35932 86559356502d
permissions -rw-r--r--
add theory HOLCF/ex/Strict_Fun.thy
wenzelm@9000
     1
(*  Title:      HOLCF/ex/ROOT.ML
nipkow@244
     2
wenzelm@9000
     3
Misc HOLCF examples.
nipkow@244
     4
*)
nipkow@244
     5
wenzelm@24106
     6
use_thys ["Dnat", "Stream", "Dagstuhl", "Focus_ex", "Fix2", "Hoare",
huffman@33813
     7
  "Loop", "Fixrec_ex", "Powerdomain_ex", "Domain_ex", "Domain_Proofs",
huffman@35167
     8
  "Strict_Fun",
huffman@33813
     9
  "New_Domain"];