isabelle: src/HOL/Import/HOL4/Generated/num.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	type_maps
37387 3581483cca6c qualified types "+" and nat; qualified constants Ball, Bex, Suc, curry; modernized some specifications haftmann parents: 17188 diff changeset	6	"num" > "Nat.nat"
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	7
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	8	const_maps
37387 3581483cca6c qualified types "+" and nat; qualified constants Ball, Bex, Suc, curry; modernized some specifications haftmann parents: 17188 diff changeset	9	"SUC" > "Nat.Suc"
44763 b50d5d694838 HOL/Import: Update HOL4 generated files to current Isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 37387 diff changeset	10	"0" > "Groups.zero_class.zero" :: "nat"
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	11
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	12	thm_maps
44763 b50d5d694838 HOL/Import: Update HOL4 generated files to current Isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 37387 diff changeset	13	"NOT_SUC" > "Nat.Suc_not_Zero"
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	14	"INV_SUC" > "Nat.Suc_inject"
44763 b50d5d694838 HOL/Import: Update HOL4 generated files to current Isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 37387 diff changeset	15	"INDUCTION" > "Fact.fact_nat.induct"
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	16
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	17	ignore_thms
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	18	"num_TY_DEF"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	19	"num_ISO_DEF"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	20	"ZERO_REP_DEF"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	21	"ZERO_DEF"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	22	"SUC_REP_DEF"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	23	"SUC_DEF"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	24	"IS_NUM_REP"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	25
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	26	end

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