src/ZF/Tools/inductive_package.ML
changeset 11680 b5b96188e94c
parent 9329 d2655dc8a4b4
child 12132 1ef58b332ca9
equal deleted inserted replaced
11679:afdbee613f58 11680:b5b96188e94c
   260   fun prove_intr (ct, tacsf) = prove_goalw_cterm part_rec_defs ct tacsf;
   260   fun prove_intr (ct, tacsf) = prove_goalw_cterm part_rec_defs ct tacsf;
   261 
   261 
   262   val intrs = ListPair.map prove_intr
   262   val intrs = ListPair.map prove_intr
   263 		(map (cterm_of sign1) intr_tms,
   263 		(map (cterm_of sign1) intr_tms,
   264 		 map intro_tacsf (mk_disj_rls(length intr_tms)))
   264 		 map intro_tacsf (mk_disj_rls(length intr_tms)))
   265 	       handle SIMPLIFIER (msg,thm) => (print_thm thm; error msg);
   265 	       handle MetaSimplifier.SIMPLIFIER (msg,thm) => (print_thm thm; error msg);
   266 
   266 
   267   (********)
   267   (********)
   268   val dummy = writeln "  Proving the elimination rule...";
   268   val dummy = writeln "  Proving the elimination rule...";
   269 
   269 
   270   (*Breaks down logical connectives in the monotonic function*)
   270   (*Breaks down logical connectives in the monotonic function*)