isabelle: src/HOLCF/HOLCF.thy@5b37787d2d9e (annotated)

1479 21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	1	(* Title: HOLCF/HOLCF.thy
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	2	ID: $Id$
1479 21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	3	Author: Franz Regensburger
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	4
16841 228d663cc9b3 use all files in HOLCF.thy; wenzelm parents: 16054 diff changeset	5	HOLCF -- a semantic extension of HOL by the LCF logic.
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	6	*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	7
15650 b37dc98fbbc5 converted to new-style theory huffman parents: 15576 diff changeset	8	theory HOLCF
15742 64eae3513064 speed improvements for the domain package huffman parents: 15651 diff changeset	9	imports Sprod Ssum Up Lift Discrete One Tr Domain
16841 228d663cc9b3 use all files in HOLCF.thy; wenzelm parents: 16054 diff changeset	10	uses
228d663cc9b3 use all files in HOLCF.thy; wenzelm parents: 16054 diff changeset	11	"holcf_logic.ML"
228d663cc9b3 use all files in HOLCF.thy; wenzelm parents: 16054 diff changeset	12	"cont_consts.ML"
228d663cc9b3 use all files in HOLCF.thy; wenzelm parents: 16054 diff changeset	13	"domain/library.ML"
228d663cc9b3 use all files in HOLCF.thy; wenzelm parents: 16054 diff changeset	14	"domain/syntax.ML"
228d663cc9b3 use all files in HOLCF.thy; wenzelm parents: 16054 diff changeset	15	"domain/axioms.ML"
228d663cc9b3 use all files in HOLCF.thy; wenzelm parents: 16054 diff changeset	16	"domain/theorems.ML"
228d663cc9b3 use all files in HOLCF.thy; wenzelm parents: 16054 diff changeset	17	"domain/extender.ML"
228d663cc9b3 use all files in HOLCF.thy; wenzelm parents: 16054 diff changeset	18	"domain/interface.ML"
228d663cc9b3 use all files in HOLCF.thy; wenzelm parents: 16054 diff changeset	19	"adm_tac.ML"
228d663cc9b3 use all files in HOLCF.thy; wenzelm parents: 16054 diff changeset	20
15650 b37dc98fbbc5 converted to new-style theory huffman parents: 15576 diff changeset	21	begin
b37dc98fbbc5 converted to new-style theory huffman parents: 15576 diff changeset	22
16841 228d663cc9b3 use all files in HOLCF.thy; wenzelm parents: 16054 diff changeset	23	ML_setup {*
228d663cc9b3 use all files in HOLCF.thy; wenzelm parents: 16054 diff changeset	24	simpset_ref() := simpset() addSolver
17612 5b37787d2d9e adm_tac/cont_tacRs: proper simpset; wenzelm parents: 16841 diff changeset	25	(mk_solver' "adm_tac" (fn ss =>
5b37787d2d9e adm_tac/cont_tacRs: proper simpset; wenzelm parents: 16841 diff changeset	26	adm_tac (cut_facts_tac (Simplifier.prems_of_ss ss) THEN' cont_tacRs ss)));
16841 228d663cc9b3 use all files in HOLCF.thy; wenzelm parents: 16054 diff changeset	27	*}
228d663cc9b3 use all files in HOLCF.thy; wenzelm parents: 16054 diff changeset	28
15650 b37dc98fbbc5 converted to new-style theory huffman parents: 15576 diff changeset	29	end

author	wenzelm
	Fri, 23 Sep 2005 22:21:52 +0200
changeset 17612	5b37787d2d9e
parent 16841	228d663cc9b3
child 17876	b9c92f384109
permissions	-rw-r--r--