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