equal
deleted
inserted
replaced
266 |
266 |
267 val ccl_dstncts = |
267 val ccl_dstncts = |
268 let |
268 let |
269 fun mk_raw_dstnct_thm rls s = |
269 fun mk_raw_dstnct_thm rls s = |
270 Goal.prove_global @{theory} [] [] (Syntax.read_prop_global @{theory} s) |
270 Goal.prove_global @{theory} [] [] (Syntax.read_prop_global @{theory} s) |
271 (fn {context = ctxt, ...} => rtac @{thm notI} 1 THEN eresolve_tac ctxt rls 1) |
271 (fn {context = ctxt, ...} => resolve_tac ctxt @{thms notI} 1 THEN eresolve_tac ctxt rls 1) |
272 in map (mk_raw_dstnct_thm caseB_lemmas) |
272 in map (mk_raw_dstnct_thm caseB_lemmas) |
273 (mk_dstnct_rls @{theory} ["bot","true","false","pair","lambda"]) end |
273 (mk_dstnct_rls @{theory} ["bot","true","false","pair","lambda"]) end |
274 |
274 |
275 fun mk_dstnct_thms ctxt defs inj_rls xs = |
275 fun mk_dstnct_thms ctxt defs inj_rls xs = |
276 let |
276 let |