isabelle: src/HOL/Import/Generate-HOL/GenHOL4Word32.thy@01ef1c3d9cfd (annotated)

14620 1be590fd2422 Minor cleanup of headers and some speedup of the HOL4 import. skalberg parents: 14516 diff changeset	1	(* Title: HOL/Import/Generate-HOL/GenHOL4Word32.thy
41589 bbd861837ebc tuned headers; wenzelm parents: 17566 diff changeset	2	Author: Sebastian Skalberg, TU Muenchen
14620 1be590fd2422 Minor cleanup of headers and some speedup of the HOL4 import. skalberg parents: 14516 diff changeset	3	*)
1be590fd2422 Minor cleanup of headers and some speedup of the HOL4 import. skalberg parents: 14516 diff changeset	4
16417 9bc16273c2d4 migrated theory headers to new format haftmann parents: 14620 diff changeset	5	theory GenHOL4Word32 imports GenHOL4Base begin;
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	6
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	7	import_segment "hol4";
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	8
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	9	setup_dump "../HOL" "HOL4Word32";
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	10
17566 484ff733f29c new header syntax; wenzelm parents: 16417 diff changeset	11	append_dump "theory HOL4Word32 imports HOL4Base begin";
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	12
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	13	import_theory bits;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	14
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	15	const_renames
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	16	BIT > bit
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	17
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	18	end_import;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	19
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	20	import_theory word32;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	21
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	22	const_renames
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	23	"==" > EQUIV;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	24
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	25	end_import;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	26
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	27	append_dump "end";
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	28
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	29	flush_dump;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	30
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	31	import_segment "";
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	32
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	33	end

author	blanchet
	Thu, 12 May 2011 15:29:19 +0200
changeset 42733	01ef1c3d9cfd
parent 41589	bbd861837ebc
child 46780	ab4f3f765f91
permissions	-rw-r--r--