author  wenzelm 
Sat, 04 Mar 2000 13:25:09 +0100  
changeset 8343  fb604f0e5640 
parent 8303  5e7037409118 
child 8482  bbc805ebc904 
permissions  rwrr 
7700  1 
(* Title: HOL/Inductive.thy 
2 
ID: $Id$ 

3 
*) 

1187  4 

8343  5 
theory Inductive = Gfp + Prod + Sum + NatDef 
7700  6 
files 
8303  7 
"Tools/induct_method.ML" 
7700  8 
"Tools/inductive_package.ML" 
9 
"Tools/datatype_aux.ML" 

10 
"Tools/datatype_prop.ML" 

11 
"Tools/datatype_rep_proofs.ML" 

12 
"Tools/datatype_abs_proofs.ML" 

13 
"Tools/datatype_package.ML" 

14 
"Tools/primrec_package.ML": 

6437  15 

8303  16 
setup InductMethod.setup 
6437  17 
setup InductivePackage.setup 
7700  18 
setup DatatypePackage.setup 
19 

7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7700
diff
changeset

20 
theorems [mono] = 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7700
diff
changeset

21 
subset_refl imp_refl disj_mono conj_mono ex_mono all_mono 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7700
diff
changeset

22 
Collect_mono in_mono vimage_mono 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7700
diff
changeset

23 
imp_conv_disj not_not de_Morgan_disj de_Morgan_conj 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7700
diff
changeset

24 
not_all not_ex 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7700
diff
changeset

25 
Ball_def Bex_def 
6437  26 

27 
end 