equal
deleted
inserted
replaced
64 val _ = Theory.requires thy "Inductive_ZF" "(co)inductive definitions"; |
64 val _ = Theory.requires thy "Inductive_ZF" "(co)inductive definitions"; |
65 val ctxt = ProofContext.init thy; |
65 val ctxt = ProofContext.init thy; |
66 |
66 |
67 val intr_specs = map (apfst (apfst Binding.name_of)) raw_intr_specs; |
67 val intr_specs = map (apfst (apfst Binding.name_of)) raw_intr_specs; |
68 val (intr_names, intr_tms) = split_list (map fst intr_specs); |
68 val (intr_names, intr_tms) = split_list (map fst intr_specs); |
69 val case_names = RuleCases.case_names intr_names; |
69 val case_names = Rule_Cases.case_names intr_names; |
70 |
70 |
71 (*recT and rec_params should agree for all mutually recursive components*) |
71 (*recT and rec_params should agree for all mutually recursive components*) |
72 val rec_hds = map head_of rec_tms; |
72 val rec_hds = map head_of rec_tms; |
73 |
73 |
74 val dummy = assert_all is_Const rec_hds |
74 val dummy = assert_all is_Const rec_hds |