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 = \<open> |
49 method_setup wfd_strengthen = \<open> |
50 Scan.lift Args.name_inner_syntax >> (fn s => fn ctxt => |
50 Scan.lift Args.embedded_inner_syntax >> (fn s => fn ctxt => |
51 SIMPLE_METHOD' (fn i => |
51 SIMPLE_METHOD' (fn i => |
52 Rule_Insts.res_inst_tac ctxt [((("Q", 0), Position.none), s)] [] @{thm wfd_strengthen_lemma} i |
52 Rule_Insts.res_inst_tac ctxt [((("Q", 0), Position.none), s)] [] @{thm wfd_strengthen_lemma} i |
53 THEN assume_tac ctxt (i + 1))) |
53 THEN assume_tac ctxt (i + 1))) |
54 \<close> |
54 \<close> |
55 |
55 |