isabelle: src/HOL/Import/HOL4/Generated/combin.imp@3bbc156823dd (annotated)

14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	1	import
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	2
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	3	import_segment "hol4"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	4
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	5	def_maps
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	6	"W" > "W_def"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	7	"S" > "S_def"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	8	"K" > "K_def"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	9	"I" > "I_def"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	10	"C" > "C_def"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	11
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	12	const_maps
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	13	"o" > "Fun.comp"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	14	"W" > "HOL4Base.combin.W"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	15	"S" > "HOL4Base.combin.S"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	16	"K" > "HOL4Base.combin.K"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	17	"I" > "HOL4Base.combin.I"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	18	"C" > "HOL4Base.combin.C"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	19
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	20	thm_maps
44763 b50d5d694838 HOL/Import: Update HOL4 generated files to current Isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 14516 diff changeset	21	"o_THM" > "Fun.comp_def"
b50d5d694838 HOL/Import: Update HOL4 generated files to current Isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 14516 diff changeset	22	"o_DEF" > "Fun.comp_def"
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	23	"o_ASSOC" > "Fun.o_assoc"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	24	"W_def" > "HOL4Base.combin.W_def"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	25	"W_THM" > "HOL4Base.combin.W_def"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	26	"W_DEF" > "HOL4Base.combin.W_DEF"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	27	"S_def" > "HOL4Base.combin.S_def"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	28	"S_THM" > "HOL4Base.combin.S_def"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	29	"S_DEF" > "HOL4Base.combin.S_DEF"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	30	"K_def" > "HOL4Base.combin.K_def"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	31	"K_THM" > "HOL4Base.combin.K_def"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	32	"K_DEF" > "HOL4Base.combin.K_DEF"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	33	"I_o_ID" > "HOL4Base.combin.I_o_ID"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	34	"I_def" > "HOL4Base.combin.I_def"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	35	"I_THM" > "HOL4Base.combin.I_THM"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	36	"I_DEF" > "HOL4Base.combin.I_DEF"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	37	"C_def" > "HOL4Base.combin.C_def"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	38	"C_THM" > "HOL4Base.combin.C_def"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	39	"C_DEF" > "HOL4Base.combin.C_DEF"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	40
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	41	end

author	wenzelm
	Sat, 03 Mar 2012 22:53:24 +0100
changeset 46793	3bbc156823dd
parent 46787	3d3d8f8929a7
permissions	-rw-r--r--