equal
deleted
inserted
replaced
482 end |
482 end |
483 *} |
483 *} |
484 |
484 |
485 |
485 |
486 ML {* atomize_goal @{theory} @{term "x memb [] = False"} *} |
486 ML {* atomize_goal @{theory} @{term "x memb [] = False"} *} |
487 ML {* atomize_goal @{theory} @{term "x = xa ⟹ a # x = a # xa"} *} |
487 ML {* atomize_goal @{theory} @{term "x = xa ? a # x = a # xa"} *} |
488 |
488 |
489 |
489 |
490 |
490 |
491 ML {* |
491 ML {* |
492 fun lift_thm_goal lthy qty qty_name rsp_thms defs rthm goal = |
492 fun lift_thm_goal lthy qty qty_name rsp_thms defs rthm goal = |