--- a/src/HOL/Import/HOLLight/hollight.imp Fri Jul 15 16:51:01 2011 +0200
+++ b/src/HOL/Import/HOLLight/hollight.imp Sat Jul 16 00:01:17 2011 +0200
@@ -572,7 +572,7 @@
"WF_DCHAIN" > "HOLLight.hollight.WF_DCHAIN"
"UNWIND_THM2" > "HOL.simp_thms_39"
"UNWIND_THM1" > "HOL.simp_thms_40"
- "UNIV_SUBSET" > "HOLLight.hollight.UNIV_SUBSET"
+ "UNIV_SUBSET" > "Orderings.top_class.top_unique"
"UNIV_NOT_EMPTY" > "Set.UNIV_not_empty"
"UNIQUE_SKOLEM_THM" > "HOL.choice_eq"
"UNIQUE_SKOLEM_ALT" > "HOLLight.hollight.UNIQUE_SKOLEM_ALT"
@@ -791,7 +791,7 @@
"SUBSET_INSERT_DELETE" > "HOLLight.hollight.SUBSET_INSERT_DELETE"
"SUBSET_INSERT" > "Set.subset_insert"
"SUBSET_IMAGE" > "Set.subset_image_iff"
- "SUBSET_EMPTY" > "Set.subset_empty"
+ "SUBSET_EMPTY" > "Orderings.bot_class.bot_unique"
"SUBSET_DIFF" > "Set.Diff_subset"
"SUBSET_DELETE" > "HOLLight.hollight.SUBSET_DELETE"
"SUBSET_CARD_EQ" > "HOLLight.hollight.SUBSET_CARD_EQ"
@@ -1547,6 +1547,7 @@
"IN_UNION" > "Complete_Lattice.mem_simps_3"
"IN_SUPPORT" > "HOLLight.hollight.IN_SUPPORT"
"IN_SING" > "Set.singleton_iff"
+ "IN_SET_OF_LIST" > "HOLLightList.IN_SET_OF_LIST"
"IN_REST" > "HOLLight.hollight.IN_REST"
"IN_NUMSEG_0" > "HOLLight.hollight.IN_NUMSEG_0"
"IN_NUMSEG" > "SetInterval.ord_class.atLeastAtMost_iff"
@@ -2278,6 +2279,7 @@
"$_def" > "HOLLight.hollight.$_def"
ignore_thms
+ "WF_REC_CASES"
"TYDEF_sum"
"TYDEF_prod"
"TYDEF_option"
@@ -2287,12 +2289,15 @@
"SNDCART_PASTECART"
"SET_OF_LIST_OF_SET"
"REP_ABS_PAIR"
+ "RECURSION_CASEWISE_PAIRWISE"
+ "RECURSION_CASEWISE"
"PASTECART_FST_SND"
"PASTECART_EQ"
"MEM_LIST_OF_SET"
"MEM_ASSOC"
"LIST_OF_SET_PROPERTIES"
"LENGTH_LIST_OF_SET"
+ "HAS_SIZE_SET_OF_LIST"
"FSTCART_PASTECART"
"FORALL_PASTECART"
"FINITE_SET_OF_LIST"
@@ -2321,6 +2326,10 @@
"DEF_CONS"
"DEF_ASSOC"
"DEF_,"
+ "CASEWISE_WORKS"
+ "CASEWISE_CASES"
+ "CASEWISE"
+ "CARD_SET_OF_LIST_LE"
"ALL_MAP"
end