isabelle: src/HOL/Import/HOL4/Generated/sum.imp@ade3fc826af3 (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
44763 b50d5d694838 HOL/Import: Update HOL4 generated files to current Isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 15647 diff changeset	6	"sum" > "Sum_Type.sum"
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	7
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	8	const_maps
44763 b50d5d694838 HOL/Import: Update HOL4 generated files to current Isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 15647 diff changeset	9	"sum_case" > "Sum_Type.sum.sum_case"
46787 3d3d8f8929a7 file system structure separating HOL4 and HOL Light concerns haftmann parents: 44763 diff changeset	10	"OUTR" > "Compatibility.OUTR"
3d3d8f8929a7 file system structure separating HOL4 and HOL Light concerns haftmann parents: 44763 diff changeset	11	"OUTL" > "Compatibility.OUTL"
3d3d8f8929a7 file system structure separating HOL4 and HOL Light concerns haftmann parents: 44763 diff changeset	12	"ISR" > "Compatibility.ISR"
3d3d8f8929a7 file system structure separating HOL4 and HOL Light concerns haftmann parents: 44763 diff changeset	13	"ISL" > "Compatibility.ISL"
15647 b1f486a9c56b Updated import configuration. skalberg parents: 14516 diff changeset	14	"INR" > "Sum_Type.Inr"
b1f486a9c56b Updated import configuration. skalberg parents: 14516 diff changeset	15	"INL" > "Sum_Type.Inl"
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	16
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	17	thm_maps
44763 b50d5d694838 HOL/Import: Update HOL4 generated files to current Isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 15647 diff changeset	18	"sum_distinct1" > "Sum_Type.Inr_not_Inl"
b50d5d694838 HOL/Import: Update HOL4 generated files to current Isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 15647 diff changeset	19	"sum_distinct" > "Sum_Type.Inl_not_Inr"
46787 3d3d8f8929a7 file system structure separating HOL4 and HOL Light concerns haftmann parents: 44763 diff changeset	20	"sum_case_def" > "Compatibility.sum_case_def"
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	21	"sum_case_cong" > "HOL4Base.sum.sum_case_cong"
46787 3d3d8f8929a7 file system structure separating HOL4 and HOL Light concerns haftmann parents: 44763 diff changeset	22	"sum_axiom" > "Compatibility.sum_axiom"
44763 b50d5d694838 HOL/Import: Update HOL4 generated files to current Isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 15647 diff changeset	23	"sum_INDUCT" > "Sum_Type.sum.induct"
b50d5d694838 HOL/Import: Update HOL4 generated files to current Isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 15647 diff changeset	24	"sum_CASES" > "Sum_Type.sum.nchotomy"
46787 3d3d8f8929a7 file system structure separating HOL4 and HOL Light concerns haftmann parents: 44763 diff changeset	25	"OUTR" > "Compatibility.OUTR"
3d3d8f8929a7 file system structure separating HOL4 and HOL Light concerns haftmann parents: 44763 diff changeset	26	"OUTL" > "Compatibility.OUTL"
3d3d8f8929a7 file system structure separating HOL4 and HOL Light concerns haftmann parents: 44763 diff changeset	27	"ISR" > "Compatibility.ISR"
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	28	"ISL_OR_ISR" > "HOL4Base.sum.ISL_OR_ISR"
46787 3d3d8f8929a7 file system structure separating HOL4 and HOL Light concerns haftmann parents: 44763 diff changeset	29	"ISL" > "Compatibility.ISL"
44763 b50d5d694838 HOL/Import: Update HOL4 generated files to current Isabelle. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 15647 diff changeset	30	"INR_neq_INL" > "Sum_Type.Inr_not_Inl"
46787 3d3d8f8929a7 file system structure separating HOL4 and HOL Light concerns haftmann parents: 44763 diff changeset	31	"INR_INL_11" > "Compatibility.INR_INL_11"
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	32	"INR" > "HOL4Base.sum.INR"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	33	"INL" > "HOL4Base.sum.INL"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	34
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	35	ignore_thms
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	36	"sum_TY_DEF"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	37	"sum_ISO_DEF"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	38	"sum_Axiom"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	39	"IS_SUM_REP"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	40	"INR_DEF"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	41	"INL_DEF"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	42
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	43	end

author	boehmes
	Tue, 27 Mar 2012 17:11:02 +0200
changeset 47155	ade3fc826af3
parent 46787	3d3d8f8929a7
permissions	-rw-r--r--