--- a/src/FOLP/simpdata.ML Mon Dec 20 15:24:25 2010 +0100
+++ b/src/FOLP/simpdata.ML Mon Dec 20 16:44:33 2010 +0100
@@ -17,15 +17,15 @@
(* Conversion into rewrite rules *)
fun mk_eq th = case concl_of th of
- _ $ (Const (@{const_name "op <->"}, _) $ _ $ _) $ _ => th
- | _ $ (Const (@{const_name "op ="}, _) $ _ $ _) $ _ => th
+ _ $ (Const (@{const_name iff}, _) $ _ $ _) $ _ => th
+ | _ $ (Const (@{const_name eq}, _) $ _ $ _) $ _ => th
| _ $ (Const (@{const_name Not}, _) $ _) $ _ => th RS @{thm not_P_imp_P_iff_F}
| _ => make_iff_T th;
val mksimps_pairs =
- [(@{const_name "op -->"}, [@{thm mp}]),
- (@{const_name "op &"}, [@{thm conjunct1}, @{thm conjunct2}]),
+ [(@{const_name imp}, [@{thm mp}]),
+ (@{const_name conj}, [@{thm conjunct1}, @{thm conjunct2}]),
(@{const_name "All"}, [@{thm spec}]),
(@{const_name True}, []),
(@{const_name False}, [])];