equal
deleted
inserted
replaced
899 (lin_arith_tac ctxt ex); |
899 (lin_arith_tac ctxt ex); |
900 |
900 |
901 in |
901 in |
902 |
902 |
903 fun gen_tac ex ctxt = FIRST' [simple_tac ctxt, |
903 fun gen_tac ex ctxt = FIRST' [simple_tac ctxt, |
904 ObjectLogic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_tac ctxt ex]; |
904 Object_Logic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_tac ctxt ex]; |
905 |
905 |
906 val tac = gen_tac true; |
906 val tac = gen_tac true; |
907 |
907 |
908 end; |
908 end; |
909 |
909 |