summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Wed, 31 Oct 2001 01:21:31 +0100 | |

changeset 11991 | da6ee05d9f3d |

parent 11990 | c1daefc08eff |

child 11992 | a39798b57344 |

use HOL.induct_XXX;

--- a/src/HOL/Tools/inductive_package.ML Wed Oct 31 01:21:01 2001 +0100 +++ b/src/HOL/Tools/inductive_package.ML Wed Oct 31 01:21:31 2001 +0100 @@ -72,14 +72,14 @@ val vimage_name = "Inverse_Image.vimage"; val Const _ $ (vimage_f $ _) $ _ = HOLogic.dest_Trueprop (Thm.concl_of vimageD); -val inductive_forall_name = "HOL.inductive_forall"; -val inductive_forall_def = thm "inductive_forall_def"; -val inductive_conj_name = "HOL.inductive_conj"; -val inductive_conj_def = thm "inductive_conj_def"; -val inductive_conj = thms "inductive_conj"; -val inductive_atomize = thms "inductive_atomize"; -val inductive_rulify1 = thms "inductive_rulify1"; -val inductive_rulify2 = thms "inductive_rulify2"; +val inductive_forall_name = "HOL.induct_forall"; +val inductive_forall_def = thm "induct_forall_def"; +val inductive_conj_name = "HOL.induct_conj"; +val inductive_conj_def = thm "induct_conj_def"; +val inductive_conj = thms "induct_conj"; +val inductive_atomize = thms "induct_atomize"; +val inductive_rulify1 = thms "induct_rulify1"; +val inductive_rulify2 = thms "induct_rulify2";