summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Tools/inductive_package.ML

changeset 11991 | da6ee05d9f3d |

parent 11880 | a625de9ad62a |

child 12109 | bd6eb9194a5d |

1.1 --- a/src/HOL/Tools/inductive_package.ML Wed Oct 31 01:21:01 2001 +0100 1.2 +++ b/src/HOL/Tools/inductive_package.ML Wed Oct 31 01:21:31 2001 +0100 1.3 @@ -72,14 +72,14 @@ 1.4 val vimage_name = "Inverse_Image.vimage"; 1.5 val Const _ $ (vimage_f $ _) $ _ = HOLogic.dest_Trueprop (Thm.concl_of vimageD); 1.6 1.7 -val inductive_forall_name = "HOL.inductive_forall"; 1.8 -val inductive_forall_def = thm "inductive_forall_def"; 1.9 -val inductive_conj_name = "HOL.inductive_conj"; 1.10 -val inductive_conj_def = thm "inductive_conj_def"; 1.11 -val inductive_conj = thms "inductive_conj"; 1.12 -val inductive_atomize = thms "inductive_atomize"; 1.13 -val inductive_rulify1 = thms "inductive_rulify1"; 1.14 -val inductive_rulify2 = thms "inductive_rulify2"; 1.15 +val inductive_forall_name = "HOL.induct_forall"; 1.16 +val inductive_forall_def = thm "induct_forall_def"; 1.17 +val inductive_conj_name = "HOL.induct_conj"; 1.18 +val inductive_conj_def = thm "induct_conj_def"; 1.19 +val inductive_conj = thms "induct_conj"; 1.20 +val inductive_atomize = thms "induct_atomize"; 1.21 +val inductive_rulify1 = thms "induct_rulify1"; 1.22 +val inductive_rulify2 = thms "induct_rulify2"; 1.23 1.24 1.25