isabelle: src/HOL/Import/HOL/numeral.imp@7ff939586e83 (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	"iiSUC" > "iiSUC_def"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	7	"iZ" > "iZ_def"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	8	"iSUB" > "iSUB_def"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	9	"iSQR" > "iSQR_def"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	10	"iDUB" > "iDUB_def"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	11	"iBIT_cases" > "iBIT_cases_def"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	12
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	13	const_maps
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	14	"iiSUC" > "HOL4Base.numeral.iiSUC"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	15	"iZ" > "HOL4Base.numeral.iZ"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	16	"iSQR" > "HOL4Base.numeral.iSQR"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	17	"iDUB" > "HOL4Base.numeral.iDUB"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	18
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	19	thm_maps
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	20	"numeral_suc" > "HOL4Base.numeral.numeral_suc"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	21	"numeral_sub" > "HOL4Base.numeral.numeral_sub"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	22	"numeral_pre" > "HOL4Base.numeral.numeral_pre"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	23	"numeral_mult" > "HOL4Base.numeral.numeral_mult"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	24	"numeral_lte" > "HOL4Base.numeral.numeral_lte"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	25	"numeral_lt" > "HOL4Base.numeral.numeral_lt"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	26	"numeral_iisuc" > "HOL4Base.numeral.numeral_iisuc"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	27	"numeral_funpow" > "HOL4Base.numeral.numeral_funpow"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	28	"numeral_fact" > "HOL4Base.numeral.numeral_fact"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	29	"numeral_exp" > "HOL4Base.numeral.numeral_exp"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	30	"numeral_evenodd" > "HOL4Base.numeral.numeral_evenodd"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	31	"numeral_eq" > "HOL4Base.numeral.numeral_eq"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	32	"numeral_distrib" > "HOL4Base.numeral.numeral_distrib"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	33	"numeral_add" > "HOL4Base.numeral.numeral_add"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	34	"iiSUC_def" > "HOL4Base.numeral.iiSUC_def"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	35	"iiSUC" > "HOL4Base.numeral.iiSUC"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	36	"iZ_def" > "HOL4Base.numeral.iZ_def"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	37	"iZ" > "HOL4Base.numeral.iZ"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	38	"iSUB_THM" > "HOL4Base.numeral.iSUB_THM"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	39	"iSUB_DEF" > "HOL4Base.numeral.iSUB_DEF"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	40	"iSQR_def" > "HOL4Base.numeral.iSQR_def"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	41	"iSQR" > "HOL4Base.numeral.iSQR"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	42	"iDUB_removal" > "HOL4Base.numeral.iDUB_removal"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	43	"iDUB_def" > "HOL4Base.numeral.iDUB_def"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	44	"iDUB" > "HOL4Base.numeral.iDUB"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	45	"iBIT_cases" > "HOL4Base.numeral.iBIT_cases"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	46	"bit_initiality" > "HOL4Base.numeral.bit_initiality"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	47	"bit_induction" > "HOL4Base.numeral.bit_induction"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	48
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	49	end

author	wenzelm
	Wed, 08 Oct 2008 19:20:29 +0200
changeset 28529	7ff939586e83
parent 14516	a183dec876ab
permissions	-rw-r--r--