equal
deleted
inserted
replaced
241 Buildin("=>", [mt (not pos) p, mt pos q]) |
241 Buildin("=>", [mt (not pos) p, mt pos q]) |
242 | mt pos t = fm pos (iff_tag t) (*it might be a formula*) |
242 | mt pos t = fm pos (iff_tag t) (*it might be a formula*) |
243 |
243 |
244 val body_e = mt pos body (*evaluate now to assign into !nat_vars*) |
244 val body_e = mt pos body (*evaluate now to assign into !nat_vars*) |
245 in |
245 in |
246 Library.foldr add_nat_var (!nat_vars, body_e) |
246 foldr add_nat_var body_e (!nat_vars) |
247 end; |
247 end; |
248 |
248 |
249 |
249 |
250 (*The oracle proves the given formula t, if possible*) |
250 (*The oracle proves the given formula t, if possible*) |
251 fun oracle (sign, OracleExn t) = |
251 fun oracle (sign, OracleExn t) = |