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

author	wenzelm
	Mon, 23 Aug 2010 16:50:09 +0200
changeset 38638	94ed0f34aea2
parent 17566	484ff733f29c
child 41589	bbd861837ebc
permissions	-rw-r--r--