equal
deleted
inserted
replaced
136 |
136 |
137 |
137 |
138 |
138 |
139 (** prepare nat_cancel simprocs **) |
139 (** prepare nat_cancel simprocs **) |
140 |
140 |
141 fun prep_pat s = Thm.read_cterm (Theory.sign_of (the_context ())) |
141 fun prep_pat s = HOLogic.read_cterm (Theory.sign_of (the_context ())) s; |
142 (s, HOLogic.termT); |
|
143 val prep_pats = map prep_pat; |
142 val prep_pats = map prep_pat; |
144 |
143 |
145 fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc; |
144 fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc; |
146 |
145 |
147 val eq_pats = prep_pats ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", |
146 val eq_pats = prep_pats ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", |