equal
deleted
inserted
replaced
152 |
152 |
153 fun extend_entry ctxt (a, D) guess |
153 fun extend_entry ctxt (a, D) guess |
154 { inj = inj1, embed = embed1, return = return1, cong = cong1, hints = hints1 } |
154 { inj = inj1, embed = embed1, return = return1, cong = cong1, hints = hints1 } |
155 { inj = inj2, embed = embed2, return = return2, cong = cong2, hints = hints2 } = |
155 { inj = inj2, embed = embed2, return = return2, cong = cong2, hints = hints2 } = |
156 let |
156 let |
157 fun add_del eq del add = union eq add #> subtract eq del; |
|
158 val guessed = if guess |
157 val guessed = if guess |
159 then map (fn thm => transfer_thm |
158 then map (fn thm => transfer_thm |
160 ((a, D), (if null inj1 then inj2 else inj1, [], [], cong1)) [] ctxt thm RS sym) embed1 |
159 ((a, D), (if null inj1 then inj2 else inj1, [], [], cong1)) [] ctxt thm RS sym) embed1 |
161 else []; |
160 else []; |
162 in |
161 in |