author  wenzelm 
Mon, 23 Oct 2000 22:12:04 +0200  
changeset 10312  4c5a03649af7 
parent 10212  33fe2d701ddd 
child 10402  5e82d6cafb5f 
permissions  rwrr 
7700  1 
(* Title: HOL/Inductive.thy 
2 
ID: $Id$ 

3 
*) 

1187  4 

10212  5 
theory Inductive = Gfp + Sum_Type + 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 

10312  21 
theorems basic_monos [mono] = 
7710
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 

10312  28 
(*belongs to theory Transitive_Closure*) 
29 
declare rtrancl_induct [induct set: rtrancl] 

30 
declare rtranclE [cases set: rtrancl] 

31 
declare trancl_induct [induct set: trancl] 

32 
declare tranclE [cases set: trancl] 

33 

6437  34 
end 