author wenzelm Sat, 11 Sep 2021 22:38:41 +0200 changeset 74297 ac130a6bd6b2 parent 74296 abc878973216 child 74298 45a77ee63e57
more antiquotations;
 src/ZF/arith_data.ML file | annotate | diff | comparison | revisions src/ZF/int_arith.ML file | annotate | diff | comparison | revisions
```--- a/src/ZF/arith_data.ML	Sat Sep 11 22:28:01 2021 +0200
+++ b/src/ZF/arith_data.ML	Sat Sep 11 22:38:41 2021 +0200
@@ -29,7 +29,7 @@
fun mk_succ t = succ \$ t;
val one = mk_succ zero;

+fun mk_plus (t, u) = \<^Const>\<open>Arith.add for t u\<close>;

(*Thus mk_sum[t] yields t+#0; longer sums don't have a trailing zero*)
fun mk_sum []        = zero
@@ -80,7 +80,7 @@
(*** Use CancelNumerals simproc without binary numerals,
just for cancellation ***)

-val mk_times = FOLogic.mk_binop \<^const_name>\<open>Arith.mult\<close>;
+fun mk_times (t, u) = \<^Const>\<open>Arith.mult for t u\<close>;

fun mk_prod [] = one
| mk_prod [t] = t
@@ -175,7 +175,7 @@
struct
open CancelNumeralsCommon
val prove_conv = prove_conv "natless_cancel_numerals"
-  val mk_bal   = FOLogic.mk_binrel \<^const_name>\<open>Ordinal.lt\<close>
+  fun mk_bal (t, u) = \<^Const>\<open>Ordinal.lt for t u\<close>
val dest_bal = FOLogic.dest_bin \<^const_name>\<open>Ordinal.lt\<close> iT
@@ -188,7 +188,7 @@
struct
open CancelNumeralsCommon
val prove_conv = prove_conv "natdiff_cancel_numerals"
-  val mk_bal   = FOLogic.mk_binop \<^const_name>\<open>Arith.diff\<close>
+  fun mk_bal (t, u) = \<^Const>\<open>Arith.diff for t u\<close>
val dest_bal = FOLogic.dest_bin \<^const_name>\<open>Arith.diff\<close> iT
```--- a/src/ZF/int_arith.ML	Sat Sep 11 22:28:01 2021 +0200
+++ b/src/ZF/int_arith.ML	Sat Sep 11 22:38:41 2021 +0200
@@ -53,7 +53,7 @@
| find_first_numeral past [] = raise TERM("find_first_numeral", []);

val zero = mk_numeral 0;
+fun mk_plus (t, u) = \<^Const>\<open>zadd for t u\<close>;

(*Thus mk_sum[t] yields t+#0; longer sums don't have a trailing zero*)
fun mk_sum []        = zero
@@ -75,7 +75,7 @@
fun dest_sum t = dest_summing (true, t, []);

val one = mk_numeral 1;
-val mk_times = FOLogic.mk_binop \<^const_name>\<open>zmult\<close>;
+fun mk_times (t, u) = \<^Const>\<open>zmult for t u\<close>;

fun mk_prod [] = one
| mk_prod [t] = t
@@ -191,7 +191,7 @@
structure LessCancelNumerals = CancelNumeralsFun
(open CancelNumeralsCommon
val prove_conv = ArithData.prove_conv "intless_cancel_numerals"
-  val mk_bal   = FOLogic.mk_binrel \<^const_name>\<open>zless\<close>
+  fun mk_bal (t, u) = \<^Const>\<open>zless for t u\<close>
val dest_bal = FOLogic.dest_bin \<^const_name>\<open>zless\<close> \<^typ>\<open>i\<close>