Mercurial Mercurial > repos > isabelle / file revision
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
author Cezary Kaliszyk <kaliszyk@in.tum.de>
Wed, 07 Sep 2011 07:59:45 +0900
changeset 44763 b50d5d694838
parent 14516 a183dec876ab
permissions -rw-r--r--
HOL/Import: Update HOL4 generated files to current Isabelle.

import

import_segment "hol4"

type_maps
  "option" > "Option.option"

const_maps
  "option_case" > "Option.option.option_case"
  "THE" > "Option.the"
  "SOME" > "Option.option.Some"
  "OPTION_MAP" > "Option.map"
  "OPTION_JOIN" > "HOL4Compat.OPTION_JOIN"
  "NONE" > "Option.option.None"
  "IS_SOME" > "HOL4Compat.IS_SOME"
  "IS_NONE" > "HOL4Compat.IS_NONE"

thm_maps
  "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" > "Option.the.simps"
  "SOME_11" > "Option.option.inject"
  "OPTION_MAP_EQ_SOME" > "HOL4Base.option.OPTION_MAP_EQ_SOME"
  "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" > "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"

ignore_thms
  "option_axiom"
  "option_TY_DEF"
  "option_REP_ABS_DEF"
  "option_Axiom"
  "SOME_DEF"
  "NONE_DEF"

end
isabelle