equal
deleted
inserted
replaced
258 THEN prune_params_tac |
258 THEN prune_params_tac |
259 (*Mutual recursion: collapse references to Part(D,h)*) |
259 (*Mutual recursion: collapse references to Part(D,h)*) |
260 THEN (PRIMITIVE (fold_rule part_rec_defs)); |
260 THEN (PRIMITIVE (fold_rule part_rec_defs)); |
261 |
261 |
262 (*Elimination*) |
262 (*Elimination*) |
263 val elim = rule_by_tactic (Proof_Context.init_global thy1) (basic_elim_tac ctxt1) |
263 val elim = |
264 (unfold RS Ind_Syntax.equals_CollectD) |
264 rule_by_tactic ctxt1 (basic_elim_tac ctxt1) (unfold RS Ind_Syntax.equals_CollectD) |
265 |
265 |
266 (*Applies freeness of the given constructors, which *must* be unfolded by |
266 (*Applies freeness of the given constructors, which *must* be unfolded by |
267 the given defs. Cannot simply use the local con_defs because |
267 the given defs. Cannot simply use the local con_defs because |
268 con_defs=[] for inference systems. |
268 con_defs=[] for inference systems. |
269 Proposition A should have the form t:Si where Si is an inductive set*) |
269 Proposition A should have the form t:Si where Si is an inductive set*) |