isabelle: src/HOLCF/ex/Fix2.ML@3e47692e3a3e (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
6bcb44e4d6e5 expanded tabs clasohm parents: 1274 diff changeset	4	Copyright 1995 Technische Universitaet Muenchen
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	wenzelm
	Thu, 15 Feb 2001 17:18:54 +0100
changeset 11145	3e47692e3a3e
parent 10835	f4745d77e620
child 12036	49f6c49454c2
permissions	-rw-r--r--