isabelle: src/LCF/ex/Ex3.thy@81bf91654e73 (annotated)

4905 be73ddff6c5a proper thy files; wenzelm parents: diff changeset	1
17248 81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	2	(* $Id$ *)
81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	3
81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	4	header {* Addition with fixpoint of successor *}
4905 be73ddff6c5a proper thy files; wenzelm parents: diff changeset	5
17248 81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	6	theory Ex3
81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	7	imports LCF
81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	8	begin
4905 be73ddff6c5a proper thy files; wenzelm parents: diff changeset	9
be73ddff6c5a proper thy files; wenzelm parents: diff changeset	10	consts
17248 81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	11	s :: "'a => 'a"
81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	12	p :: "'a => 'a => 'a"
4905 be73ddff6c5a proper thy files; wenzelm parents: diff changeset	13
17248 81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	14	axioms
81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	15	p_strict: "p(UU) = UU"
81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	16	p_s: "p(s(x),y) = s(p(x,y))"
81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	17
81bf91654e73 converted to Isar theory format; wenzelm parents: 4905 diff changeset	18	ML {* use_legacy_bindings (the_context ()) *}
4905 be73ddff6c5a proper thy files; wenzelm parents: diff changeset	19
be73ddff6c5a proper thy files; wenzelm parents: diff changeset	20	end

author	wenzelm
	Sat, 03 Sep 2005 17:54:10 +0200
changeset 17248	81bf91654e73
parent 4905	be73ddff6c5a
child 19755	90f80de04c46
permissions	-rw-r--r--