author berghofe
Tue, 30 May 2000 18:02:49 +0200
changeset 9001 93af64f54bf2
parent 8482 bbc805ebc904
child 10212 33fe2d701ddd
permissions -rw-r--r--
the is now defined using primrec, avoiding explicit use of arbitrary.

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

theory Inductive = Gfp + Prod + Sum + NatDef

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