load / setup recdef package (TFL);
authorwenzelm
Mon Oct 04 21:44:07 1999 +0200 (1999-10-04)
changeset 77012c8c3b7003e5
parent 7700 38b6d2643630
child 7702 35c7e0df749f
load / setup recdef package (TFL);
src/HOL/Recdef.thy
     1.1 --- a/src/HOL/Recdef.thy	Mon Oct 04 21:43:45 1999 +0200
     1.2 +++ b/src/HOL/Recdef.thy	Mon Oct 04 21:44:07 1999 +0200
     1.3 @@ -1,6 +1,36 @@
     1.4 +(*  Title:      HOL/Recdef.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Konrad Slind
     1.7  
     1.8 -theory Recdef = WF_Rel
     1.9 -files "Tools/recdef_package.ML" "Tools/induct_method.ML":
    1.10 +TFL: recursive function definitions.
    1.11 +*)
    1.12 +
    1.13 +theory Recdef = WF_Rel + Datatype
    1.14 +files
    1.15 +  (*establish a base of common and/or helpful functions*)
    1.16 +  "../TFL/utils.sig"
    1.17 +
    1.18 +  "../TFL/usyntax.sig"
    1.19 +  "../TFL/rules.sig"
    1.20 +  "../TFL/thry.sig"
    1.21 +  "../TFL/thms.sig"
    1.22 +  "../TFL/tfl.sig"
    1.23 +  "../TFL/utils.sml"
    1.24 +
    1.25 +  (*supply implementations*)
    1.26 +  "../TFL/usyntax.sml"
    1.27 +  "../TFL/thms.sml"
    1.28 +  "../TFL/dcterm.sml"
    1.29 +  "../TFL/rules.sml"
    1.30 +  "../TFL/thry.sml"
    1.31 +
    1.32 +  (*link system and specialize for Isabelle*)
    1.33 +  "../TFL/tfl.sml"
    1.34 +  "../TFL/post.sml"
    1.35 +
    1.36 +  (*theory extender wrapper module*)
    1.37 +  "Tools/recdef_package.ML"
    1.38 +  "Tools/induct_method.ML":
    1.39  
    1.40  setup RecdefPackage.setup
    1.41  setup InductMethod.setup