src/ZF/Epsilon.ML
changeset 13149 773657d466cb
parent 12814 2f5edb146f7e
equal deleted inserted replaced
13148:fe118a977a6d 13149:773657d466cb
   312 qed "transrec2_0";
   312 qed "transrec2_0";
   313 
   313 
   314 Goal "transrec2(succ(i),a,b) = b(i, transrec2(i,a,b))";
   314 Goal "transrec2(succ(i),a,b) = b(i, transrec2(i,a,b))";
   315 by (rtac (transrec2_def RS def_transrec RS trans) 1);
   315 by (rtac (transrec2_def RS def_transrec RS trans) 1);
   316 by (simp_tac (simpset() addsimps [the_equality, if_P]) 1);
   316 by (simp_tac (simpset() addsimps [the_equality, if_P]) 1);
   317 by (Blast_tac 1);
       
   318 qed "transrec2_succ";
   317 qed "transrec2_succ";
   319 
   318 
   320 Goal "Limit(i) ==> transrec2(i,a,b) = (UN j<i. transrec2(j,a,b))";
   319 Goal "Limit(i) ==> transrec2(i,a,b) = (UN j<i. transrec2(j,a,b))";
   321 by (rtac (transrec2_def RS def_transrec RS trans) 1);
   320 by (rtac (transrec2_def RS def_transrec RS trans) 1);
   322 by (Simp_tac 1);
   321 by (Simp_tac 1);