src/HOL/Recdef.thy
author wenzelm
Mon Oct 04 21:44:07 1999 +0200 (1999-10-04)
changeset 7701 2c8c3b7003e5
parent 7357 d0e16da40ea2
child 8303 5e7037409118
permissions -rw-r--r--
load / setup recdef package (TFL);
     1 (*  Title:      HOL/Recdef.thy
     2     ID:         $Id$
     3     Author:     Konrad Slind
     4 
     5 TFL: recursive function definitions.
     6 *)
     7 
     8 theory Recdef = WF_Rel + Datatype
     9 files
    10   (*establish a base of common and/or helpful functions*)
    11   "../TFL/utils.sig"
    12 
    13   "../TFL/usyntax.sig"
    14   "../TFL/rules.sig"
    15   "../TFL/thry.sig"
    16   "../TFL/thms.sig"
    17   "../TFL/tfl.sig"
    18   "../TFL/utils.sml"
    19 
    20   (*supply implementations*)
    21   "../TFL/usyntax.sml"
    22   "../TFL/thms.sml"
    23   "../TFL/dcterm.sml"
    24   "../TFL/rules.sml"
    25   "../TFL/thry.sml"
    26 
    27   (*link system and specialize for Isabelle*)
    28   "../TFL/tfl.sml"
    29   "../TFL/post.sml"
    30 
    31   (*theory extender wrapper module*)
    32   "Tools/recdef_package.ML"
    33   "Tools/induct_method.ML":
    34 
    35 setup RecdefPackage.setup
    36 setup InductMethod.setup
    37 
    38 end