Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Import/HOL4/Generated/list.imp
changeset 46787 3d3d8f8929a7
parent 44763 b50d5d694838 
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Import/HOL4/Generated/list.imp	Sat Mar 03 22:37:41 2012 +0100
@@ -0,0 +1,135 @@
+import
+
+import_segment "hol4"
+
+def_maps
+  "EL" > "EL_def"
+
+type_maps
+  "list" > "List.list"
+
+const_maps
+  "list_size" > "Compatibility.list_size"
+  "list_case" > "List.list.list_case"
+  "ZIP" > "Compatibility.ZIP"
+  "UNZIP" > "Compatibility.unzip"
+  "TL" > "List.tl"
+  "SUM" > "Compatibility.sum"
+  "REVERSE" > "List.rev"
+  "REPLICATE" > "List.replicate"
+  "NULL" > "List.null"
+  "NIL" > "List.list.Nil"
+  "MEM" > "Compatibility.list_mem"
+  "MAP2" > "Compatibility.map2"
+  "MAP" > "List.map"
+  "LENGTH" > "Nat.size_class.size"
+  "LAST" > "List.last"
+  "HD" > "List.hd"
+  "FRONT" > "List.butlast"
+  "FOLDR" > "Compatibility.FOLDR"
+  "FOLDL" > "List.foldl"
+  "FLAT" > "List.concat"
+  "FILTER" > "List.filter"
+  "EXISTS" > "List.list_ex"
+  "EVERY" > "List.list_all"
+  "CONS" > "List.list.Cons"
+  "APPEND" > "List.append"
+
+thm_maps
+  "list_size_def" > "Compatibility.list_size_def'"
+  "list_size_cong" > "HOL4Base.list.list_size_cong"
+  "list_nchotomy" > "Compatibility.list_CASES"
+  "list_induction" > "Compatibility.list_INDUCT"
+  "list_distinct" > "List.list.distinct_1"
+  "list_case_def" > "Compatibility.list_case_def"
+  "list_case_cong" > "Compatibility.list_case_cong"
+  "list_case_compute" > "HOL4Base.list.list_case_compute"
+  "list_INDUCT" > "Compatibility.list_INDUCT"
+  "list_CASES" > "Compatibility.list_CASES"
+  "list_Axiom_old" > "Compatibility.list_Axiom_old"
+  "list_Axiom" > "Compatibility.list_Axiom"
+  "list_11" > "List.list.inject"
+  "ZIP_UNZIP" > "HOL4Base.list.ZIP_UNZIP"
+  "ZIP_MAP" > "HOL4Base.list.ZIP_MAP"
+  "ZIP" > "Compatibility.ZIP"
+  "WF_LIST_PRED" > "HOL4Base.list.WF_LIST_PRED"
+  "UNZIP_ZIP" > "HOL4Base.list.UNZIP_ZIP"
+  "UNZIP" > "Compatibility.UNZIP"
+  "TL" > "List.tl.simps_2"
+  "SUM" > "Compatibility.SUM"
+  "REVERSE_REVERSE" > "List.rev_rev_ident"
+  "REVERSE_DEF" > "Compatibility.REVERSE"
+  "REVERSE_APPEND" > "List.rev_append"
+  "NULL_DEF" > "Compatibility.NULL_DEF"
+  "NULL" > "HOL4Base.list.NULL"
+  "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.distinct_2"
+  "MEM_ZIP" > "HOL4Base.list.MEM_ZIP"
+  "MEM_MAP" > "HOL4Base.list.MEM_MAP"
+  "MEM_EL" > "HOL4Base.list.MEM_EL"
+  "MEM_APPEND" > "HOL4Base.list.MEM_APPEND"
+  "MEM" > "Compatibility.MEM"
+  "MAP_EQ_NIL" > "HOL4Base.list.MAP_EQ_NIL"
+  "MAP_CONG" > "HOL4Base.list.MAP_CONG"
+  "MAP_APPEND" > "List.map_append"
+  "MAP2_ZIP" > "HOL4Base.list.MAP2_ZIP"
+  "MAP2" > "Compatibility.MAP2"
+  "MAP" > "Compatibility.MAP"
+  "LIST_NOT_EQ" > "HOL4Base.list.LIST_NOT_EQ"
+  "LENGTH_ZIP" > "HOL4Base.list.LENGTH_ZIP"
+  "LENGTH_UNZIP" > "HOL4Base.list.LENGTH_UNZIP"
+  "LENGTH_NIL" > "List.length_0_conv"
+  "LENGTH_MAP" > "List.length_map"
+  "LENGTH_EQ_NIL" > "HOL4Base.list.LENGTH_EQ_NIL"
+  "LENGTH_EQ_CONS" > "HOL4Base.list.LENGTH_EQ_CONS"
+  "LENGTH_CONS" > "HOL4Base.list.LENGTH_CONS"
+  "LENGTH_APPEND" > "List.length_append"
+  "LENGTH" > "Compatibility.LENGTH"
+  "LAST_DEF" > "List.last.simps"
+  "LAST_CONS" > "HOL4Base.list.LAST_CONS"
+  "HD" > "List.hd.simps"
+  "FRONT_DEF" > "List.butlast.simps_2"
+  "FRONT_CONS" > "HOL4Base.list.FRONT_CONS"
+  "FOLDR_CONG" > "HOL4Base.list.FOLDR_CONG"
+  "FOLDR" > "Compatibility.FOLDR"
+  "FOLDL_CONG" > "HOL4Base.list.FOLDL_CONG"
+  "FOLDL" > "Compatibility.FOLDL"
+  "FLAT" > "Compatibility.FLAT"
+  "FILTER" > "Compatibility.FILTER"
+  "EXISTS_MEM" > "HOL4Base.list.EXISTS_MEM"
+  "EXISTS_DEF" > "Compatibility.list_exists_DEF"
+  "EXISTS_CONG" > "HOL4Base.list.EXISTS_CONG"
+  "EXISTS_APPEND" > "List.list_ex_append"
+  "EVERY_MONOTONIC" > "HOL4Base.list.EVERY_MONOTONIC"
+  "EVERY_MEM" > "HOL4Base.list.EVERY_MEM"
+  "EVERY_EL" > "HOL4Base.list.EVERY_EL"
+  "EVERY_DEF" > "Compatibility.EVERY_DEF"
+  "EVERY_CONJ" > "HOL4Base.list.EVERY_CONJ"
+  "EVERY_CONG" > "HOL4Base.list.EVERY_CONG"
+  "EVERY_APPEND" > "List.list_all_append"
+  "EQ_LIST" > "HOL4Base.list.EQ_LIST"
+  "EL_compute" > "HOL4Base.list.EL_compute"
+  "EL_ZIP" > "HOL4Base.list.EL_ZIP"
+  "EL" > "HOL4Base.list.EL"
+  "CONS_ACYCLIC" > "HOL4Base.list.CONS_ACYCLIC"
+  "CONS_11" > "List.list.inject"
+  "CONS" > "HOL4Base.list.CONS"
+  "APPEND_eq_NIL" > "HOL4Base.list.APPEND_eq_NIL"
+  "APPEND_NIL" > "List.append_Nil2"
+  "APPEND_FRONT_LAST" > "List.append_butlast_last_id"
+  "APPEND_ASSOC" > "List.append_assoc"
+  "APPEND_11" > "HOL4Base.list.APPEND_11"
+  "APPEND" > "Compatibility.APPEND"
+
+ignore_thms
+  "list_repfns"
+  "list_TY_DEF"
+  "list1_def"
+  "list0_def"
+  "NIL"
+  "CONS_def"
+
+end
isabelle