equal
deleted
inserted
replaced
1360 SOME (Goal.prove ctxt [] [] |
1360 SOME (Goal.prove ctxt [] [] |
1361 (Const (@{const_name Pure.eq}, T --> T --> propT) $ S $ S') |
1361 (Const (@{const_name Pure.eq}, T --> T --> propT) $ S $ S') |
1362 (K (EVERY |
1362 (K (EVERY |
1363 [resolve_tac ctxt [eq_reflection] 1, |
1363 [resolve_tac ctxt [eq_reflection] 1, |
1364 resolve_tac ctxt @{thms subset_antisym} 1, |
1364 resolve_tac ctxt @{thms subset_antisym} 1, |
1365 resolve_tac ctxt [subsetI] 1, dresolve_tac ctxt [CollectD] 1, simp, |
1365 resolve_tac ctxt @{thms subsetI} 1, |
1366 resolve_tac ctxt [subsetI] 1, resolve_tac ctxt [CollectI] 1, simp]))) |
1366 dresolve_tac ctxt @{thms CollectD} 1, simp, |
|
1367 resolve_tac ctxt @{thms subsetI} 1, |
|
1368 resolve_tac ctxt @{thms CollectI} 1, simp]))) |
1367 end |
1369 end |
1368 else NONE) |
1370 else NONE) |
1369 | _ => NONE) |
1371 | _ => NONE) |
1370 end |
1372 end |
1371 | _ => NONE) |
1373 | _ => NONE) |