src/HOL/Recdef.thy
author berghofe
Tue, 30 May 2000 18:02:49 +0200
changeset 9001 93af64f54bf2
parent 8303 5e7037409118
child 9855 709a295731e2
permissions -rw-r--r--
the is now defined using primrec, avoiding explicit use of arbitrary.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
7701
2c8c3b7003e5 load / setup recdef package (TFL);
wenzelm
parents: 7357
diff changeset
     1
(*  Title:      HOL/Recdef.thy
2c8c3b7003e5 load / setup recdef package (TFL);
wenzelm
parents: 7357
diff changeset
     2
    ID:         $Id$
2c8c3b7003e5 load / setup recdef package (TFL);
wenzelm
parents: 7357
diff changeset
     3
    Author:     Konrad Slind
5123
97c1d5c7b701 stepping stones;
wenzelm
parents:
diff changeset
     4
7701
2c8c3b7003e5 load / setup recdef package (TFL);
wenzelm
parents: 7357
diff changeset
     5
TFL: recursive function definitions.
2c8c3b7003e5 load / setup recdef package (TFL);
wenzelm
parents: 7357
diff changeset
     6
*)
2c8c3b7003e5 load / setup recdef package (TFL);
wenzelm
parents: 7357
diff changeset
     7
2c8c3b7003e5 load / setup recdef package (TFL);
wenzelm
parents: 7357
diff changeset
     8
theory Recdef = WF_Rel + Datatype
2c8c3b7003e5 load / setup recdef package (TFL);
wenzelm
parents: 7357
diff changeset
     9
files
2c8c3b7003e5 load / setup recdef package (TFL);
wenzelm
parents: 7357
diff changeset
    10
  (*establish a base of common and/or helpful functions*)
2c8c3b7003e5 load / setup recdef package (TFL);
wenzelm
parents: 7357
diff changeset
    11
  "../TFL/utils.sig"
2c8c3b7003e5 load / setup recdef package (TFL);
wenzelm
parents: 7357
diff changeset
    12
2c8c3b7003e5 load / setup recdef package (TFL);
wenzelm
parents: 7357
diff changeset
    13
  "../TFL/usyntax.sig"
2c8c3b7003e5 load / setup recdef package (TFL);
wenzelm
parents: 7357
diff changeset
    14
  "../TFL/rules.sig"
2c8c3b7003e5 load / setup recdef package (TFL);
wenzelm
parents: 7357
diff changeset
    15
  "../TFL/thry.sig"
2c8c3b7003e5 load / setup recdef package (TFL);
wenzelm
parents: 7357
diff changeset
    16
  "../TFL/thms.sig"
2c8c3b7003e5 load / setup recdef package (TFL);
wenzelm
parents: 7357
diff changeset
    17
  "../TFL/tfl.sig"
2c8c3b7003e5 load / setup recdef package (TFL);
wenzelm
parents: 7357
diff changeset
    18
  "../TFL/utils.sml"
2c8c3b7003e5 load / setup recdef package (TFL);
wenzelm
parents: 7357
diff changeset
    19
2c8c3b7003e5 load / setup recdef package (TFL);
wenzelm
parents: 7357
diff changeset
    20
  (*supply implementations*)
2c8c3b7003e5 load / setup recdef package (TFL);
wenzelm
parents: 7357
diff changeset
    21
  "../TFL/usyntax.sml"
2c8c3b7003e5 load / setup recdef package (TFL);
wenzelm
parents: 7357
diff changeset
    22
  "../TFL/thms.sml"
2c8c3b7003e5 load / setup recdef package (TFL);
wenzelm
parents: 7357
diff changeset
    23
  "../TFL/dcterm.sml"
2c8c3b7003e5 load / setup recdef package (TFL);
wenzelm
parents: 7357
diff changeset
    24
  "../TFL/rules.sml"
2c8c3b7003e5 load / setup recdef package (TFL);
wenzelm
parents: 7357
diff changeset
    25
  "../TFL/thry.sml"
2c8c3b7003e5 load / setup recdef package (TFL);
wenzelm
parents: 7357
diff changeset
    26
2c8c3b7003e5 load / setup recdef package (TFL);
wenzelm
parents: 7357
diff changeset
    27
  (*link system and specialize for Isabelle*)
2c8c3b7003e5 load / setup recdef package (TFL);
wenzelm
parents: 7357
diff changeset
    28
  "../TFL/tfl.sml"
2c8c3b7003e5 load / setup recdef package (TFL);
wenzelm
parents: 7357
diff changeset
    29
  "../TFL/post.sml"
2c8c3b7003e5 load / setup recdef package (TFL);
wenzelm
parents: 7357
diff changeset
    30
2c8c3b7003e5 load / setup recdef package (TFL);
wenzelm
parents: 7357
diff changeset
    31
  (*theory extender wrapper module*)
8303
5e7037409118 early setup of induct_method;
wenzelm
parents: 7701
diff changeset
    32
  "Tools/recdef_package.ML":
6438
e55a1869ed38 'HOL/recdef' theory data;
wenzelm
parents: 5123
diff changeset
    33
e55a1869ed38 'HOL/recdef' theory data;
wenzelm
parents: 5123
diff changeset
    34
setup RecdefPackage.setup
e55a1869ed38 'HOL/recdef' theory data;
wenzelm
parents: 5123
diff changeset
    35
e55a1869ed38 'HOL/recdef' theory data;
wenzelm
parents: 5123
diff changeset
    36
end