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/Inductive.thy
author berghofe
Wed, 15 Mar 2000 23:41:42 +0100
changeset 8482 bbc805ebc904
parent 8343 fb604f0e5640
child 10212 33fe2d701ddd
permissions -rw-r--r--
Added setup for primrec theory data.

(*  Title:      HOL/Inductive.thy
    ID:         $Id$
*)

theory Inductive = Gfp + Prod + Sum + NatDef
files
  "Tools/induct_method.ML"
  "Tools/inductive_package.ML"
  "Tools/datatype_aux.ML"
  "Tools/datatype_prop.ML"
  "Tools/datatype_rep_proofs.ML"
  "Tools/datatype_abs_proofs.ML"
  "Tools/datatype_package.ML"
  "Tools/primrec_package.ML":

setup InductMethod.setup
setup InductivePackage.setup
setup DatatypePackage.setup
setup PrimrecPackage.setup

theorems [mono] =
   subset_refl imp_refl disj_mono conj_mono ex_mono all_mono
   Collect_mono in_mono vimage_mono
   imp_conv_disj not_not de_Morgan_disj de_Morgan_conj
   not_all not_ex
   Ball_def Bex_def

end
isabelle