src/FOL/simpdata.ML

 
 fun int_prove_fun s = 
  (writeln s;  
   prove_goal IFOL.thy s
    (fn prems => [ (cut_facts_tac prems 1), 
-                  (Int.fast_tac 1) ]));
+                  (IntPr.fast_tac 1) ]));
 
 val conj_simps = map int_prove_fun
  ["P & True <-> P",      "True & P <-> P",
   "P & False <-> False", "False & P <-> False",
   "P & P <-> P",

                  "(ALL x. P(x) --> Q) <-> (EX x.P(x)) --> Q",
                  "(ALL x. P --> Q(x)) <-> P --> (ALL x.Q(x))"];
 
 fun int_prove nm thm  = qed_goal nm IFOL.thy thm
     (fn prems => [ (cut_facts_tac prems 1), 
-                   (Int.fast_tac 1) ]);
+                   (IntPr.fast_tac 1) ]);
 
 fun prove nm thm  = qed_goal nm FOL.thy thm (fn _ => [fast_tac FOL_cs 1]);
 
 int_prove "conj_commute" "P&Q <-> Q&P";
 int_prove "conj_left_commute" "P&(Q&R) <-> Q&(P&R)";