equal
deleted
inserted
replaced
45 using 1 3 |
45 using 1 3 |
46 apply blast |
46 apply blast |
47 done |
47 done |
48 |
48 |
49 method_setup wfd_strengthen = {* |
49 method_setup wfd_strengthen = {* |
50 Scan.lift Args.name >> (fn s => fn ctxt => |
50 Scan.lift Args.name_inner_syntax >> (fn s => fn ctxt => |
51 SIMPLE_METHOD' (fn i => |
51 SIMPLE_METHOD' (fn i => |
52 res_inst_tac ctxt [(("Q", 0), s)] @{thm wfd_strengthen_lemma} i THEN assume_tac ctxt (i+1))) |
52 res_inst_tac ctxt [(("Q", 0), s)] @{thm wfd_strengthen_lemma} i THEN assume_tac ctxt (i+1))) |
53 *} |
53 *} |
54 |
54 |
55 lemma wf_anti_sym: "[| Wfd(r); <a,x>:r; <x,a>:r |] ==> P" |
55 lemma wf_anti_sym: "[| Wfd(r); <a,x>:r; <x,a>:r |] ==> P" |