equal
deleted
inserted
replaced
448 fun pc_tac ctxt thms = DEPTH_SOLVE_1 o (step_tac ctxt thms) |
448 fun pc_tac ctxt thms = DEPTH_SOLVE_1 o (step_tac ctxt thms) |
449 \<close> |
449 \<close> |
450 |
450 |
451 method_setup eqintr = \<open>Scan.succeed (SIMPLE_METHOD o eqintr_tac)\<close> |
451 method_setup eqintr = \<open>Scan.succeed (SIMPLE_METHOD o eqintr_tac)\<close> |
452 method_setup NE = \<open> |
452 method_setup NE = \<open> |
453 Scan.lift Args.embedded_inner_syntax >> (fn s => fn ctxt => SIMPLE_METHOD' (NE_tac ctxt s)) |
453 Scan.lift Parse.embedded_inner_syntax >> (fn s => fn ctxt => SIMPLE_METHOD' (NE_tac ctxt s)) |
454 \<close> |
454 \<close> |
455 method_setup pc = \<open>Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (pc_tac ctxt ths))\<close> |
455 method_setup pc = \<open>Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (pc_tac ctxt ths))\<close> |
456 method_setup add_mp = \<open>Scan.succeed (SIMPLE_METHOD' o add_mp_tac)\<close> |
456 method_setup add_mp = \<open>Scan.succeed (SIMPLE_METHOD' o add_mp_tac)\<close> |
457 |
457 |
458 ML_file \<open>rew.ML\<close> |
458 ML_file \<open>rew.ML\<close> |