--- a/src/HOL/Import/HOL/list.imp Wed Sep 07 00:08:09 2011 +0200
+++ b/src/HOL/Import/HOL/list.imp Wed Sep 07 07:59:45 2011 +0900
@@ -19,7 +19,7 @@
"REPLICATE" > "List.replicate"
"NULL" > "List.null"
"NIL" > "List.list.Nil"
- "MEM" > "List.op mem"
+ "MEM" > "HOL4Compat.list_mem"
"MAP2" > "HOL4Compat.map2"
"MAP" > "List.map"
"LENGTH" > "Nat.size_class.size"
@@ -30,25 +30,25 @@
"FOLDL" > "List.foldl"
"FLAT" > "List.concat"
"FILTER" > "List.filter"
- "EXISTS" > "HOL4Compat.list_exists"
+ "EXISTS" > "List.list_ex"
"EVERY" > "List.list_all"
"CONS" > "List.list.Cons"
"APPEND" > "List.append"
thm_maps
- "list_size_def" > "HOL4Compat.list_size_def"
+ "list_size_def" > "HOL4Compat.list_size_def'"
"list_size_cong" > "HOL4Base.list.list_size_cong"
"list_nchotomy" > "HOL4Compat.list_CASES"
- "list_induction" > "HOL4Compat.unzip.induct"
- "list_distinct" > "List.list.simps_1"
+ "list_induction" > "HOL4Compat.list_INDUCT"
+ "list_distinct" > "List.list.distinct_1"
"list_case_def" > "HOL4Compat.list_case_def"
"list_case_cong" > "HOL4Compat.list_case_cong"
"list_case_compute" > "HOL4Base.list.list_case_compute"
- "list_INDUCT" > "HOL4Compat.unzip.induct"
+ "list_INDUCT" > "HOL4Compat.list_INDUCT"
"list_CASES" > "HOL4Compat.list_CASES"
"list_Axiom_old" > "HOL4Compat.list_Axiom_old"
"list_Axiom" > "HOL4Compat.list_Axiom"
- "list_11" > "List.list.simps_3"
+ "list_11" > "List.list.inject"
"ZIP_UNZIP" > "HOL4Base.list.ZIP_UNZIP"
"ZIP_MAP" > "HOL4Base.list.ZIP_MAP"
"ZIP" > "HOL4Compat.ZIP"
@@ -62,11 +62,11 @@
"REVERSE_APPEND" > "List.rev_append"
"NULL_DEF" > "HOL4Compat.NULL_DEF"
"NULL" > "HOL4Base.list.NULL"
- "NOT_NIL_CONS" > "List.list.simps_1"
+ "NOT_NIL_CONS" > "List.list.distinct_1"
"NOT_EXISTS" > "HOL4Base.list.NOT_EXISTS"
"NOT_EVERY" > "HOL4Base.list.NOT_EVERY"
"NOT_EQ_LIST" > "HOL4Base.list.NOT_EQ_LIST"
- "NOT_CONS_NIL" > "List.list.simps_2"
+ "NOT_CONS_NIL" > "List.list.distinct_2"
"MEM_ZIP" > "HOL4Base.list.MEM_ZIP"
"MEM_MAP" > "HOL4Base.list.MEM_MAP"
"MEM_EL" > "HOL4Base.list.MEM_EL"
@@ -102,7 +102,7 @@
"EXISTS_MEM" > "HOL4Base.list.EXISTS_MEM"
"EXISTS_DEF" > "HOL4Compat.list_exists_DEF"
"EXISTS_CONG" > "HOL4Base.list.EXISTS_CONG"
- "EXISTS_APPEND" > "HOL4Base.list.EXISTS_APPEND"
+ "EXISTS_APPEND" > "List.list_ex_append"
"EVERY_MONOTONIC" > "HOL4Base.list.EVERY_MONOTONIC"
"EVERY_MEM" > "HOL4Base.list.EVERY_MEM"
"EVERY_EL" > "HOL4Base.list.EVERY_EL"
@@ -115,7 +115,7 @@
"EL_ZIP" > "HOL4Base.list.EL_ZIP"
"EL" > "HOL4Base.list.EL"
"CONS_ACYCLIC" > "HOL4Base.list.CONS_ACYCLIC"
- "CONS_11" > "List.list.simps_3"
+ "CONS_11" > "List.list.inject"
"CONS" > "HOL4Base.list.CONS"
"APPEND_eq_NIL" > "HOL4Base.list.APPEND_eq_NIL"
"APPEND_NIL" > "List.append_Nil2"