isabelle: src/HOLCF/HOLCF.ML@d539d47cce69 (annotated)

1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1274 diff changeset	1	(* Title: HOLCF/HOLCF.ML
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	2	ID: $Id$
1461 6bcb44e4d6e5 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	*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	5
15650 b37dc98fbbc5 converted to new-style theory huffman parents: 14981 diff changeset	6	structure HOLCF =
b37dc98fbbc5 converted to new-style theory huffman parents: 14981 diff changeset	7	struct
b37dc98fbbc5 converted to new-style theory huffman parents: 14981 diff changeset	8	val thy = the_context ();
b37dc98fbbc5 converted to new-style theory huffman parents: 14981 diff changeset	9	end;
b37dc98fbbc5 converted to new-style theory huffman parents: 14981 diff changeset	10
16062 f8110bd9957f cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other paulson parents: 15650 diff changeset	11	use "adm_tac.ML";
3661 1ea4a45b9412 moved extended adm_tac to new place mueller parents: 2355 diff changeset	12
7570 a9391550eea1 Mod because of new solver interface. nipkow parents: 4098 diff changeset	13	simpset_ref() := simpset() addSolver
a9391550eea1 Mod because of new solver interface. nipkow parents: 4098 diff changeset	14	(mk_solver "adm_tac" (fn thms => (adm_tac (cut_facts_tac thms THEN' cont_tacRs))));
3661 1ea4a45b9412 moved extended adm_tac to new place mueller parents: 2355 diff changeset	15
4098 71e05eb27fb6 isatool fixclasimp; wenzelm parents: 3661 diff changeset	16	val HOLCF_ss = simpset();

author	wenzelm
	Wed, 22 Jun 2005 19:41:29 +0200
changeset 16541	d539d47cce69
parent 16062	f8110bd9957f
child 16841	228d663cc9b3
permissions	-rw-r--r--