equal
deleted
inserted
replaced
71 val gfp_name = "Gfp.gfp"; |
71 val gfp_name = "Gfp.gfp"; |
72 val lfp_name = "Lfp.lfp"; |
72 val lfp_name = "Lfp.lfp"; |
73 val vimage_name = "Inverse_Image.vimage"; |
73 val vimage_name = "Inverse_Image.vimage"; |
74 val Const _ $ (vimage_f $ _) $ _ = HOLogic.dest_Trueprop (Thm.concl_of vimageD); |
74 val Const _ $ (vimage_f $ _) $ _ = HOLogic.dest_Trueprop (Thm.concl_of vimageD); |
75 |
75 |
76 val inductive_forall_name = "Inductive.forall"; |
76 val inductive_forall_name = "HOL.inductive_forall"; |
77 val inductive_forall_def = thm "forall_def"; |
77 val inductive_forall_def = thm "inductive_forall_def"; |
78 val inductive_conj_name = "Inductive.conj"; |
78 val inductive_conj_name = "HOL.inductive_conj"; |
79 val inductive_conj_def = thm "conj_def"; |
79 val inductive_conj_def = thm "inductive_conj_def"; |
80 val inductive_conj = thms "inductive_conj"; |
80 val inductive_conj = thms "inductive_conj"; |
81 val inductive_atomize = thms "inductive_atomize"; |
81 val inductive_atomize = thms "inductive_atomize"; |
82 val inductive_rulify1 = thms "inductive_rulify1"; |
82 val inductive_rulify1 = thms "inductive_rulify1"; |
83 val inductive_rulify2 = thms "inductive_rulify2"; |
83 val inductive_rulify2 = thms "inductive_rulify2"; |
84 |
84 |