isabelle: TFL/tfl.sig@97bb3ff3c771 (annotated)

3302 404fe31fd8d2 New headers and other minor changes paulson parents: 3245 diff changeset	1	(* Title: TFL/tfl
404fe31fd8d2 New headers and other minor changes paulson parents: 3245 diff changeset	2	ID: $Id$
404fe31fd8d2 New headers and other minor changes paulson parents: 3245 diff changeset	3	Author: Konrad Slind, Cambridge University Computer Laboratory
404fe31fd8d2 New headers and other minor changes paulson parents: 3245 diff changeset	4	Copyright 1997 University of Cambridge
404fe31fd8d2 New headers and other minor changes paulson parents: 3245 diff changeset	5
3391 5e45dd3b64e9 More de-HOLification: using Free, Const, etc. instead of mk_var, mk_const paulson parents: 3333 diff changeset	6	Main module
3302 404fe31fd8d2 New headers and other minor changes paulson parents: 3245 diff changeset	7	*)
404fe31fd8d2 New headers and other minor changes paulson parents: 3245 diff changeset	8
2112 3902e9af752f Konrad Slind's TFL paulson parents: diff changeset	9	signature TFL_sig =
3902e9af752f Konrad Slind's TFL paulson parents: diff changeset	10	sig
3245 241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 3191 diff changeset	11	datatype pattern = GIVEN of term * int
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 3191 diff changeset	12	\| OMITTED of term * int
2112 3902e9af752f Konrad Slind's TFL paulson parents: diff changeset	13
3391 5e45dd3b64e9 More de-HOLification: using Free, Const, etc. instead of mk_var, mk_const paulson parents: 3333 diff changeset	14	val mk_functional : theory -> term list
3245 241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 3191 diff changeset	15	-> {functional:term,
2112 3902e9af752f Konrad Slind's TFL paulson parents: diff changeset	16	pats: pattern list}
3902e9af752f Konrad Slind's TFL paulson parents: diff changeset	17
3405 2cccd0e3e9ea Numerous simplifications and removal of HOL-isms paulson parents: 3391 diff changeset	18	val wfrec_definition0 : theory -> string -> term -> term -> theory
3191 14bd6e5985f1 TFL now integrated with HOL (more work needed) paulson parents: 2112 diff changeset	19
3459 112cbb8301dc Removal of structure Context and its replacement by a theorem list of paulson parents: 3405 diff changeset	20	val post_definition : simpset * thm list -> theory * (thm * pattern list)
3405 2cccd0e3e9ea Numerous simplifications and removal of HOL-isms paulson parents: 3391 diff changeset	21	-> {theory : theory,
2cccd0e3e9ea Numerous simplifications and removal of HOL-isms paulson parents: 3391 diff changeset	22	rules : thm,
2cccd0e3e9ea Numerous simplifications and removal of HOL-isms paulson parents: 3391 diff changeset	23	TCs : term list list,
2cccd0e3e9ea Numerous simplifications and removal of HOL-isms paulson parents: 3391 diff changeset	24	full_pats_TCs : (term * term list) list,
2cccd0e3e9ea Numerous simplifications and removal of HOL-isms paulson parents: 3391 diff changeset	25	patterns : pattern list}
3191 14bd6e5985f1 TFL now integrated with HOL (more work needed) paulson parents: 2112 diff changeset	26
3405 2cccd0e3e9ea Numerous simplifications and removal of HOL-isms paulson parents: 3391 diff changeset	27	(*CURRENTLY UNUSED
3459 112cbb8301dc Removal of structure Context and its replacement by a theorem list of paulson parents: 3405 diff changeset	28	val wfrec_eqns : simpset * thm list -> theory -> term list
3245 241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 3191 diff changeset	29	-> {WFR : term,
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 3191 diff changeset	30	proto_def : term,
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 3191 diff changeset	31	extracta :(thm * term list) list,
2112 3902e9af752f Konrad Slind's TFL paulson parents: diff changeset	32	pats : pattern list}
3902e9af752f Konrad Slind's TFL paulson parents: diff changeset	33
3245 241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 3191 diff changeset	34	val lazyR_def : theory
3391 5e45dd3b64e9 More de-HOLification: using Free, Const, etc. instead of mk_var, mk_const paulson parents: 3333 diff changeset	35	-> term list
3245 241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 3191 diff changeset	36	-> {theory:theory,
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 3191 diff changeset	37	rules :thm,
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 3191 diff changeset	38	R :term,
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 3191 diff changeset	39	full_pats_TCs :(term * term list) list,
2112 3902e9af752f Konrad Slind's TFL paulson parents: diff changeset	40	patterns: pattern list}
3405 2cccd0e3e9ea Numerous simplifications and removal of HOL-isms paulson parents: 3391 diff changeset	41	---------------------*)
2112 3902e9af752f Konrad Slind's TFL paulson parents: diff changeset	42
3405 2cccd0e3e9ea Numerous simplifications and removal of HOL-isms paulson parents: 3391 diff changeset	43	val mk_induction : theory -> term -> term -> (term * term list) list -> thm
2112 3902e9af752f Konrad Slind's TFL paulson parents: diff changeset	44
3245 241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 3191 diff changeset	45	val postprocess: {WFtac:tactic, terminator:tactic, simplifier:cterm -> thm}
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 3191 diff changeset	46	-> theory
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 3191 diff changeset	47	-> {rules:thm, induction:thm, TCs:term list list}
241838c01caf Removal of redundant code (unused or already present in Isabelle. paulson parents: 3191 diff changeset	48	-> {rules:thm, induction:thm, nested_tcs:thm list}
2112 3902e9af752f Konrad Slind's TFL paulson parents: diff changeset	49	end;

author	wenzelm
	Mon, 13 Oct 1997 10:31:21 +0200
changeset 3848	97bb3ff3c771
parent 3459	112cbb8301dc
child 6498	1ebbe18fe236
permissions	-rw-r--r--