src/ZF/Tools/inductive_package.ML
 changeset 52145 28963df2dffb parent 52087 f3075fc4f5f6 child 54742 7a86358a3c0b
equal 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*)`