src/ZF/intr_elim.ML
changeset 202 4e68398cdc06
parent 70 8a29f8b4aca1
child 231 cb6a24451544
equal deleted inserted replaced
201:9e41c6cec27c 202:4e68398cdc06
   202 	   [_] => [] 			(*no mutual recursion*)
   202 	   [_] => [] 			(*no mutual recursion*)
   203 	 | _ => rec_tms ~~		(*define the sets as Parts*)
   203 	 | _ => rec_tms ~~		(*define the sets as Parts*)
   204 		map (subst_atomic [(Free(X',iT),big_rec_tm)]) parts));
   204 		map (subst_atomic [(Free(X',iT),big_rec_tm)]) parts));
   205 
   205 
   206 val thy = extend_theory Ind.thy (big_rec_name ^ "_Inductive")
   206 val thy = extend_theory Ind.thy (big_rec_name ^ "_Inductive")
   207     ([], [], [], [], [], None) axpairs;
   207     ([], [], [], [], [], [], None) axpairs;
   208 
   208 
   209 val defs = map (get_axiom thy o #1) axpairs;
   209 val defs = map (get_axiom thy o #1) axpairs;
   210 
   210 
   211 val big_rec_def::part_rec_defs = defs;
   211 val big_rec_def::part_rec_defs = defs;
   212 
   212