isabelle: src/HOLCF/HOLCF.thy@20d01210b9b1 (annotated)

1479 21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	1	(* Title: HOLCF/HOLCF.thy
21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	2	Author: Franz Regensburger
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	3
16841 228d663cc9b3 use all files in HOLCF.thy; wenzelm parents: 16054 diff changeset	4	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	5	*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	6
15650 b37dc98fbbc5 converted to new-style theory huffman parents: 15576 diff changeset	7	theory HOLCF
29130 685c9e05a6ab new theory Dsum: cpo of disjoint sum huffman parents: 28892 diff changeset	8	imports
29534 247e4c816004 rename Dsum.thy to Sum_Cpo.thy huffman parents: 29530 diff changeset	9	Domain ConvexPD Algebraic Universal Sum_Cpo Main
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"
23152 9497234a2743 moved HOLCF tools to canonical place; wenzelm parents: 19105 diff changeset	12	"Tools/cont_consts.ML"
29530 9905b660612b change to simpler, more extensible continuity simproc huffman parents: 29355 diff changeset	13	"Tools/cont_proc.ML"
23152 9497234a2743 moved HOLCF tools to canonical place; wenzelm parents: 19105 diff changeset	14	"Tools/domain/domain_library.ML"
9497234a2743 moved HOLCF tools to canonical place; wenzelm parents: 19105 diff changeset	15	"Tools/domain/domain_syntax.ML"
9497234a2743 moved HOLCF tools to canonical place; wenzelm parents: 19105 diff changeset	16	"Tools/domain/domain_axioms.ML"
9497234a2743 moved HOLCF tools to canonical place; wenzelm parents: 19105 diff changeset	17	"Tools/domain/domain_theorems.ML"
9497234a2743 moved HOLCF tools to canonical place; wenzelm parents: 19105 diff changeset	18	"Tools/domain/domain_extender.ML"
9497234a2743 moved HOLCF tools to canonical place; wenzelm parents: 19105 diff changeset	19	"Tools/adm_tac.ML"
15650 b37dc98fbbc5 converted to new-style theory huffman parents: 15576 diff changeset	20	begin
b37dc98fbbc5 converted to new-style theory huffman parents: 15576 diff changeset	21
25904 8161f137b0e9 new theory of powerdomains huffman parents: 23152 diff changeset	22	defaultsort pcpo
8161f137b0e9 new theory of powerdomains huffman parents: 23152 diff changeset	23
26339 7825c83c9eff eliminated change_claset/simpset; wenzelm parents: 25904 diff changeset	24	declaration {* fn _ =>
7825c83c9eff eliminated change_claset/simpset; wenzelm parents: 25904 diff changeset	25	Simplifier.map_ss (fn simpset => simpset addSolver
17612 5b37787d2d9e adm_tac/cont_tacRs: proper simpset; wenzelm parents: 16841 diff changeset	26	(mk_solver' "adm_tac" (fn ss =>
30603 71180005f251 proper context for prove_cont/adm_tac; wenzelm parents: 29542 diff changeset	27	Adm.adm_tac (Simplifier.the_context ss)
71180005f251 proper context for prove_cont/adm_tac; wenzelm parents: 29542 diff changeset	28	(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	29	*}
228d663cc9b3 use all files in HOLCF.thy; wenzelm parents: 16054 diff changeset	30
15650 b37dc98fbbc5 converted to new-style theory huffman parents: 15576 diff changeset	31	end

author	haftmann
	Mon, 20 Apr 2009 16:28:13 +0200
changeset 30957	20d01210b9b1
parent 30603	71180005f251
child 30910	a7cc0ef93269
permissions	-rw-r--r--