src/HOLCF/ROOT.ML
author huffman
Mon May 11 08:28:09 2009 -0700 (2009-05-11)
changeset 31095 b79d140f6d0b
parent 29921 3d50e96bcd6b
child 33615 261abc2e3155
permissions -rw-r--r--
simplify fixrec proofs for mutually-recursive definitions; generate better fixpoint induction rules
wenzelm@3623
     1
(*  Title:      HOLCF/ROOT.ML
nipkow@243
     2
    ID:         $Id$
clasohm@1461
     3
    Author:     Franz Regensburger
nipkow@243
     4
wenzelm@16841
     5
HOLCF -- a semantic extension of HOL by the LCF logic.
nipkow@243
     6
*)
nipkow@243
     7
nipkow@29921
     8
no_document use_thy "Nat_Int_Bij";
nipkow@29921
     9
regensbu@1274
    10
use_thy "HOLCF";