equal
deleted
inserted
replaced
361 or |
361 or |
362 |
362 |
363 A = B ----> (R ===> R) A B |
363 A = B ----> (R ===> R) A B |
364 |
364 |
365 for more complicated types of A and B |
365 for more complicated types of A and B |
|
366 |
|
367 |
|
368 The regularize_trm accepts raw theorems in which equalities |
|
369 and quantifiers match exactly the ones in the lifted theorem |
|
370 but also accepts partially regularized terms. |
|
371 |
|
372 This means that the raw theorems can have: |
|
373 Ball (Respects R), Bex (Respects R), Bexeq (Respects R), R |
|
374 in the places where: |
|
375 All, Ex, Ex1, (op =) |
|
376 is required the lifted theorem. |
|
377 |
366 *) |
378 *) |
367 |
379 |
368 val mk_babs = Const (@{const_name Babs}, dummyT) |
380 val mk_babs = Const (@{const_name Babs}, dummyT) |
369 val mk_ball = Const (@{const_name Ball}, dummyT) |
381 val mk_ball = Const (@{const_name Ball}, dummyT) |
370 val mk_bex = Const (@{const_name Bex}, dummyT) |
382 val mk_bex = Const (@{const_name Bex}, dummyT) |