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/HOL/option.imp
changeset 44763 b50d5d694838
parent 14516 a183dec876ab 
--- a/src/HOL/Import/HOL/option.imp	Wed Sep 07 00:08:09 2011 +0200
+++ b/src/HOL/Import/HOL/option.imp	Wed Sep 07 07:59:45 2011 +0900
@@ -3,34 +3,34 @@
 import_segment "hol4"
 
 type_maps
-  "option" > "Datatype.option"
+  "option" > "Option.option"
 
 const_maps
-  "option_case" > "Datatype.option.option_case"
-  "THE" > "Datatype.the"
-  "SOME" > "Datatype.option.Some"
-  "OPTION_MAP" > "Datatype.option_map"
+  "option_case" > "Option.option.option_case"
+  "THE" > "Option.the"
+  "SOME" > "Option.option.Some"
+  "OPTION_MAP" > "Option.map"
   "OPTION_JOIN" > "HOL4Compat.OPTION_JOIN"
-  "NONE" > "Datatype.option.None"
+  "NONE" > "Option.option.None"
   "IS_SOME" > "HOL4Compat.IS_SOME"
   "IS_NONE" > "HOL4Compat.IS_NONE"
 
 thm_maps
-  "option_nchotomy" > "Datatype.option.nchotomy"
-  "option_induction" > "HOL4Compat.OPTION_JOIN.induct"
+  "option_nchotomy" > "Option.option.nchotomy"
+  "option_induction" > "Option.option.induct"
   "option_case_def" > "HOL4Compat.option_case_def"
   "option_case_cong" > "HOL4Base.option.option_case_cong"
   "option_case_compute" > "HOL4Base.option.option_case_compute"
   "option_CLAUSES" > "HOL4Base.option.option_CLAUSES"
-  "THE_DEF" > "Datatype.the.simps"
-  "SOME_11" > "Datatype.option.simps_3"
+  "THE_DEF" > "Option.the.simps"
+  "SOME_11" > "Option.option.inject"
   "OPTION_MAP_EQ_SOME" > "HOL4Base.option.OPTION_MAP_EQ_SOME"
-  "OPTION_MAP_EQ_NONE" > "Datatype.option_map_is_None"
+  "OPTION_MAP_EQ_NONE" > "Option.option_map_is_None"
   "OPTION_MAP_DEF" > "HOL4Compat.OPTION_MAP_DEF"
   "OPTION_JOIN_EQ_SOME" > "HOL4Base.option.OPTION_JOIN_EQ_SOME"
   "OPTION_JOIN_DEF" > "HOL4Compat.OPTION_JOIN_DEF"
-  "NOT_SOME_NONE" > "Datatype.option.simps_2"
-  "NOT_NONE_SOME" > "Datatype.option.simps_1"
+  "NOT_SOME_NONE" > "Option.option.distinct_2"
+  "NOT_NONE_SOME" > "Option.option.distinct_1"
   "IS_SOME_DEF" > "HOL4Compat.IS_SOME_DEF"
   "IS_NONE_DEF" > "HOL4Compat.IS_NONE_DEF"
isabelle