isabelle: src/HOLCF/ex/Fix2.ML@81a4b4a245b0 (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
10835 f4745d77e620 ` -> $ nipkow parents: 9265 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";
1274 ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	20
ea0668a1c0ba added 8bit pragmas regensbu parents: diff changeset	21

author	huffman
	Thu, 26 May 2005 02:23:27 +0200
changeset 16081	81a4b4a245b0
parent 14981	e73f8140af78
child 17291	94f6113fe9ed
permissions	-rw-r--r--