--- a/src/ZF/arith_data.ML Thu Sep 16 18:59:59 2021 +0200
+++ b/src/ZF/arith_data.ML Sun Sep 19 20:47:16 2021 +0200
@@ -36,12 +36,6 @@
| mk_sum [t,u] = mk_plus (t, u)
| mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
-(*this version ALWAYS includes a trailing zero*)
-fun long_mk_sum [] = zero
- | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
-
-val dest_plus = FOLogic.dest_bin \<^const_name>\<open>Arith.add\<close> iT;
-
(* dest_sum *)
fun dest_sum \<^Const_>\<open>zero\<close> = []
@@ -63,8 +57,6 @@
fun is_eq_thm th =
can FOLogic.dest_eq (FOLogic.dest_Trueprop (Thm.prop_of th));
-fun add_chyps chyps ct = Drule.list_implies (map Thm.cprop_of chyps, ct);
-
fun prove_conv name tacs ctxt prems (t,u) =
if t aconv u then NONE
else