isabelle: src/HOLCF/ex/Fix2.ML@50be659d4222 (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
9265 35aab1c9c08c removal of batch style, and tidying paulson parents: 1461 diff changeset	17	Goal "gix`F=lub(range(%i. iterate i F UU))";
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
	Fri, 06 Oct 2000 17:35:58 +0200
changeset 10168	50be659d4222
parent 9265	35aab1c9c08c
child 10835	f4745d77e620
permissions	-rw-r--r--