isabelle: src/HOLCF/Fun3.ML@bb5f4faea1f3 (annotated)

9245 428385c4bc50 removed most batch-style proofs paulson parents: 3842 diff changeset	1	(* Title: HOLCF/Fun3.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: 243 diff changeset	3	Author: Franz Regensburger
12030 46d57d0290a2 GPLed; wenzelm parents: 9248 diff changeset	4	License: GPL (GNU GENERAL PUBLIC LICENSE)
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
2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 1461 diff changeset	7	(* for compatibility with old HOLCF-Version *)
9248 e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc. paulson parents: 9245 diff changeset	8	Goal "UU = (%x. UU)";
9245 428385c4bc50 removed most batch-style proofs paulson parents: 3842 diff changeset	9	by (simp_tac (HOL_ss addsimps [UU_def,UU_fun_def]) 1);
428385c4bc50 removed most batch-style proofs paulson parents: 3842 diff changeset	10	qed "inst_fun_pcpo";