summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/ZF/Tools/inductive_package.ML

changeset 52145 | 28963df2dffb |

parent 52087 | f3075fc4f5f6 |

child 54742 | 7a86358a3c0b |

equal
deleted
inserted
replaced

52144:9065615d0360 | 52145:28963df2dffb |
---|---|

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*) |