isabelle: src/HOLCF/ex/Fix2.ML@59bc43b51aa2 (annotated)

1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1274 diff changeset	1	(* Title: HOLCF/ex/Fix2.ML
1274 ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	2	ID: $Id$
1461 6bcb44e4d6e5 expanded tabs clasohm parents: 1274 diff changeset	3	Author: Franz Regensburger
12036 49f6c49454c2 GPLed; wenzelm parents: 10835 diff changeset	4	License: GPL (GNU GENERAL PUBLIC LICENSE)
1274 ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	5	*)
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	6
9265 35aab1c9c08c removal of batch style, and tidying paulson parents: 1461 diff changeset	7	Goal "fix = gix";
35aab1c9c08c removal of batch style, and tidying paulson parents: 1461 diff changeset	8	by (rtac ext_cfun 1);
35aab1c9c08c removal of batch style, and tidying paulson parents: 1461 diff changeset	9	by (rtac antisym_less 1);
35aab1c9c08c removal of batch style, and tidying paulson parents: 1461 diff changeset	10	by (rtac fix_least 1);
35aab1c9c08c removal of batch style, and tidying paulson parents: 1461 diff changeset	11	by (rtac gix1_def 1);
35aab1c9c08c removal of batch style, and tidying paulson parents: 1461 diff changeset	12	by (rtac gix2_def 1);
35aab1c9c08c removal of batch style, and tidying paulson parents: 1461 diff changeset	13	by (rtac (fix_eq RS sym) 1);
35aab1c9c08c removal of batch style, and tidying paulson parents: 1461 diff changeset	14	qed "lemma1";
1274 ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	15
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	16
10835 f4745d77e620 ` -> $ nipkow parents: 9265 diff changeset	17	Goal "gix$F=lub(range(%i. iterate i F UU))";
9265 35aab1c9c08c removal of batch style, and tidying paulson parents: 1461 diff changeset	18	by (rtac (lemma1 RS subst) 1);
35aab1c9c08c removal of batch style, and tidying paulson parents: 1461 diff changeset	19	by (rtac fix_def2 1);
35aab1c9c08c removal of batch style, and tidying paulson parents: 1461 diff changeset	20	qed "lemma2";
1274 ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	21
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	22

author	nipkow
	Mon, 13 May 2002 15:27:28 +0200
changeset 13145	59bc43b51aa2
parent 12036	49f6c49454c2
child 14981	e73f8140af78
permissions	-rw-r--r--