equal
deleted
inserted
replaced
76 val zero_one_idom_simproc = |
76 val zero_one_idom_simproc = |
77 make_simproc {lhss = lhss' , name = "zero_one_idom_simproc", |
77 make_simproc {lhss = lhss' , name = "zero_one_idom_simproc", |
78 proc = sproc, identifier = []} |
78 proc = sproc, identifier = []} |
79 |
79 |
80 fun number_of thy T n = |
80 fun number_of thy T n = |
81 if not (Sign.of_sort thy (T, @{sort number})) |
81 if not (Sign.of_sort thy (T, @{sort numeral})) |
82 then raise CTERM ("number_of", []) |
82 then raise CTERM ("number_of", []) |
83 else Numeral.mk_cnumber (Thm.ctyp_of thy T) n; |
83 else Numeral.mk_cnumber (Thm.ctyp_of thy T) n; |
84 |
84 |
85 val setup = |
85 val setup = |
86 Lin_Arith.add_inj_thms [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2] |
86 Lin_Arith.add_inj_thms [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2] |