isabelle: src/HOL/Recdef.thy@6e0f23304061 (annotated)

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

author	wenzelm
	Thu, 16 Mar 2000 00:35:27 +0100
changeset 8490	6e0f23304061
parent 8303	5e7037409118
child 9855	709a295731e2
permissions	-rw-r--r--