isabelle: src/HOL/Import/HOL/pair.imp@19cb8d558166 (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	"RPROD" > "RPROD_def"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	7	"LEX" > "LEX_def"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	8
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	9	type_maps
37678 0040bafffdef "prod" and "sum" replace "" and "+" respectively haftmann* parents: 37591 diff changeset	10	"prod" > "Product_Type.prod"
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	11
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	12	const_maps
37591 d3daea901123 merged constants "split" and "prod_case" haftmann parents: 37391 diff changeset	13	"pair_case" > "Product_Type.prod_case"
d3daea901123 merged constants "split" and "prod_case" haftmann parents: 37391 diff changeset	14	"UNCURRY" > "Product_Type.prod_case"
37391 476270a6c2dc tuned quotes, antiquotations and whitespace haftmann parents: 37387 diff changeset	15	"FST" > "Product_Type.fst"
476270a6c2dc tuned quotes, antiquotations and whitespace haftmann parents: 37387 diff changeset	16	"SND" > "Product_Type.snd"
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	17	"RPROD" > "HOL4Base.pair.RPROD"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	18	"LEX" > "HOL4Base.pair.LEX"
37387 3581483cca6c qualified types "+" and nat; qualified constants Ball, Bex, Suc, curry; modernized some specifications haftmann parents: 17916 diff changeset	19	"CURRY" > "Product_Type.curry"
37391 476270a6c2dc tuned quotes, antiquotations and whitespace haftmann parents: 37387 diff changeset	20	"," > "Product_Type.Pair"
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	21	"##" > "prod_fun"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	22
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	23	thm_maps
17916 51269a053504 updated; wenzelm parents: 17889 diff changeset	24	"pair_induction" > "Datatype.prod.induct_correctness"
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	25	"pair_case_thm" > "Product_Type.split"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	26	"pair_case_def" > "HOL4Compat.pair_case_def"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	27	"pair_case_cong" > "HOL4Base.pair.pair_case_cong"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	28	"pair_Axiom" > "HOL4Base.pair.pair_Axiom"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	29	"WF_RPROD" > "HOL4Base.pair.WF_RPROD"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	30	"WF_LEX" > "HOL4Base.pair.WF_LEX"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	31	"UNCURRY_VAR" > "Product_Type.split_beta"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	32	"UNCURRY_ONE_ONE_THM" > "HOL4Base.pair.UNCURRY_ONE_ONE_THM"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	33	"UNCURRY_DEF" > "Product_Type.split"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	34	"UNCURRY_CURRY_THM" > "Product_Type.split_curry"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	35	"UNCURRY_CONG" > "HOL4Base.pair.UNCURRY_CONG"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	36	"UNCURRY" > "Product_Type.split_beta"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	37	"SND" > "Product_Type.snd_conv"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	38	"RPROD_def" > "HOL4Base.pair.RPROD_def"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	39	"RPROD_DEF" > "HOL4Base.pair.RPROD_DEF"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	40	"PFORALL_THM" > "HOL4Base.pair.PFORALL_THM"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	41	"PEXISTS_THM" > "HOL4Base.pair.PEXISTS_THM"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	42	"PAIR_MAP_THM" > "Product_Type.prod_fun"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	43	"PAIR_MAP" > "HOL4Compat.PAIR_MAP"
15647 b1f486a9c56b Updated import configuration. skalberg parents: 14516 diff changeset	44	"PAIR_EQ" > "Datatype.prod.simps_1"
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	45	"PAIR" > "HOL4Compat.PAIR"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	46	"LEX_def" > "HOL4Base.pair.LEX_def"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	47	"LEX_DEF" > "HOL4Base.pair.LEX_DEF"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	48	"LET2_RATOR" > "HOL4Base.pair.LET2_RATOR"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	49	"LET2_RAND" > "HOL4Base.pair.LET2_RAND"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	50	"LAMBDA_PROD" > "Product_Type.split_eta"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	51	"FST" > "Product_Type.fst_conv"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	52	"FORALL_PROD" > "Product_Type.split_paired_All"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	53	"EXISTS_PROD" > "Product_Type.split_paired_Ex"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	54	"ELIM_UNCURRY" > "Product_Type.split_beta"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	55	"ELIM_PFORALL" > "HOL4Base.pair.ELIM_PFORALL"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	56	"ELIM_PEXISTS" > "HOL4Base.pair.ELIM_PEXISTS"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	57	"CURRY_UNCURRY_THM" > "Product_Type.curry_split"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	58	"CURRY_ONE_ONE_THM" > "HOL4Base.pair.CURRY_ONE_ONE_THM"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	59	"CURRY_DEF" > "Product_Type.curry_conv"
15647 b1f486a9c56b Updated import configuration. skalberg parents: 14516 diff changeset	60	"CLOSED_PAIR_EQ" > "Datatype.prod.simps_1"
b1f486a9c56b Updated import configuration. skalberg parents: 14516 diff changeset	61	"ABS_PAIR_THM" > "Datatype.prod.nchotomy"
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	62
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	63	ignore_thms
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	64	"prod_TY_DEF"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	65	"MK_PAIR_DEF"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	66	"IS_PAIR_DEF"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	67	"COMMA_DEF"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	68	"ABS_REP_prod"
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	69
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	70	end

author	bulwahn
	Tue, 28 Sep 2010 11:59:53 +0200
changeset 39765	19cb8d558166
parent 37678	0040bafffdef
child 40607	30d512bf47a7
permissions	-rw-r--r--