isabelle: src/HOLCF/ex/Fix2.ML@c9c6ae9e8b88 (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
1274 ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	4	*)
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	5
9265 35aab1c9c08c removal of batch style, and tidying paulson parents: 1461 diff changeset	6	Goal "fix = gix";
35aab1c9c08c removal of batch style, and tidying paulson parents: 1461 diff changeset	7	by (rtac ext_cfun 1);
35aab1c9c08c removal of batch style, and tidying paulson parents: 1461 diff changeset	8	by (rtac antisym_less 1);
35aab1c9c08c removal of batch style, and tidying paulson parents: 1461 diff changeset	9	by (rtac fix_least 1);
35aab1c9c08c removal of batch style, and tidying paulson parents: 1461 diff changeset	10	by (rtac gix1_def 1);
35aab1c9c08c removal of batch style, and tidying paulson parents: 1461 diff changeset	11	by (rtac gix2_def 1);
35aab1c9c08c removal of batch style, and tidying paulson parents: 1461 diff changeset	12	by (rtac (fix_eq RS sym) 1);
35aab1c9c08c removal of batch style, and tidying paulson parents: 1461 diff changeset	13	qed "lemma1";
1274 ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	14
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	15
18075 43000d7a017c changed iterate to a continuous type huffman parents: 17291 diff changeset	16	Goal "gix$F=lub(range(%i. iterate i$F$UU))";
9265 35aab1c9c08c removal of batch style, and tidying paulson parents: 1461 diff changeset	17	by (rtac (lemma1 RS subst) 1);
35aab1c9c08c removal of batch style, and tidying paulson parents: 1461 diff changeset	18	by (rtac fix_def2 1);
35aab1c9c08c removal of batch style, and tidying paulson parents: 1461 diff changeset	19	qed "lemma2";

author	paulson
	Mon, 23 Jan 2006 11:38:43 +0100
changeset 18752	c9c6ae9e8b88
parent 18075	43000d7a017c
permissions	-rw-r--r--