author  berghofe 
Tue, 30 May 2000 18:02:49 +0200  
changeset 9001  93af64f54bf2 
parent 8482  bbc805ebc904 
child 10212  33fe2d701ddd 
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 
8482  19 
setup PrimrecPackage.setup 
7700  20 

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

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

22 
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

23 
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

24 
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

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

26 
Ball_def Bex_def 
6437  27 

28 
end 