isabelle: src/HOLCF/HOLCF.ML@5d278411e127 (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	Copyright 1993 Technische Universitaet Muenchen
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
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	7	open HOLCF;
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	8
3661 1ea4a45b9412 moved extended adm_tac to new place mueller parents: 2355 diff changeset	9	use"adm.ML";
1ea4a45b9412 moved extended adm_tac to new place mueller parents: 2355 diff changeset	10
1ea4a45b9412 moved extended adm_tac to new place mueller parents: 2355 diff changeset	11	simpset := !simpset addSolver(fn thms =>
1ea4a45b9412 moved extended adm_tac to new place mueller parents: 2355 diff changeset	12	(adm_tac (cut_facts_tac thms THEN' cont_tacRs)));
1ea4a45b9412 moved extended adm_tac to new place mueller parents: 2355 diff changeset	13
1274 ea0668a1c0ba added 8bit pragmas regensbu parents: 1267 diff changeset	14	val HOLCF_ss = !simpset;

author	wenzelm
	Thu, 30 Oct 1997 10:50:04 +0100
changeset 4038	5d278411e127
parent 3661	1ea4a45b9412
child 4098	71e05eb27fb6
permissions	-rw-r--r--