isabelle: src/HOL/Import/HOL4/Template/GenHOL4Vec.thy@a8b1236e0837 (annotated)

46879 a8b1236e0837 tuned headers; wenzelm parents: 46787 diff changeset	1	(* Title: HOL/Import/HOL4/Template/GenHOL4Vec.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
46787 3d3d8f8929a7 file system structure separating HOL4 and HOL Light concerns haftmann parents: 46780 diff changeset	5	theory GenHOL4Vec
3d3d8f8929a7 file system structure separating HOL4 and HOL Light concerns haftmann parents: 46780 diff changeset	6	imports GenHOL4Base
3d3d8f8929a7 file system structure separating HOL4 and HOL Light concerns haftmann parents: 46780 diff changeset	7	begin
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	8
46787 3d3d8f8929a7 file system structure separating HOL4 and HOL Light concerns haftmann parents: 46780 diff changeset	9	import_segment "hol4"
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	10
46787 3d3d8f8929a7 file system structure separating HOL4 and HOL Light concerns haftmann parents: 46780 diff changeset	11	setup_dump "../Generated" "HOL4Vev"
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	12
46787 3d3d8f8929a7 file system structure separating HOL4 and HOL Light concerns haftmann parents: 46780 diff changeset	13	append_dump {*theory HOL4Vec
3d3d8f8929a7 file system structure separating HOL4 and HOL Light concerns haftmann parents: 46780 diff changeset	14	imports HOL4Base
3d3d8f8929a7 file system structure separating HOL4 and HOL Light concerns haftmann parents: 46780 diff changeset	15	begin
3d3d8f8929a7 file system structure separating HOL4 and HOL Light concerns haftmann parents: 46780 diff changeset	16	*}
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	17
46787 3d3d8f8929a7 file system structure separating HOL4 and HOL Light concerns haftmann parents: 46780 diff changeset	18	import_theory "~~/src/HOL/Import/HOL4/Generated" res_quan;
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	19	end_import;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	20
46787 3d3d8f8929a7 file system structure separating HOL4 and HOL Light concerns haftmann parents: 46780 diff changeset	21	import_theory "~~/src/HOL/Import/HOL4/Generated" word_base;
14516 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	BIT > bit;
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
46787 3d3d8f8929a7 file system structure separating HOL4 and HOL Light concerns haftmann parents: 46780 diff changeset	28	import_theory "~~/src/HOL/Import/HOL4/Generated" word_num;
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	29	end_import;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	30
46787 3d3d8f8929a7 file system structure separating HOL4 and HOL Light concerns haftmann parents: 46780 diff changeset	31	import_theory "~~/src/HOL/Import/HOL4/Generated" word_bitop;
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	32	end_import;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	33
46787 3d3d8f8929a7 file system structure separating HOL4 and HOL Light concerns haftmann parents: 46780 diff changeset	34	import_theory "~~/src/HOL/Import/HOL4/Generated" bword_num;
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	35	end_import;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	36
46787 3d3d8f8929a7 file system structure separating HOL4 and HOL Light concerns haftmann parents: 46780 diff changeset	37	import_theory "~~/src/HOL/Import/HOL4/Generated" bword_arith;
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	38	end_import;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	39
46787 3d3d8f8929a7 file system structure separating HOL4 and HOL Light concerns haftmann parents: 46780 diff changeset	40	import_theory "~~/src/HOL/Import/HOL4/Generated" bword_bitop;
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	41	end_import;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	42
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	43	append_dump "end";
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	44
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	45	flush_dump;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	46
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	47	import_segment "";
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	48
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	49	end

author	wenzelm
	Mon, 12 Mar 2012 19:09:38 +0100
changeset 46879	a8b1236e0837
parent 46787	3d3d8f8929a7
permissions	-rw-r--r--