equal
deleted
inserted
replaced
120 (FIXME: is there a better way to present the theorem?) |
120 (FIXME: is there a better way to present the theorem?) |
121 |
121 |
122 To be able to use our oracle for Isar proofs, we wrap it into a tactic: |
122 To be able to use our oracle for Isar proofs, we wrap it into a tactic: |
123 *} |
123 *} |
124 |
124 |
125 ML{*val iff_oracle_tac = |
125 ML %grayML{*val iff_oracle_tac = |
126 CSUBGOAL (fn (goal, i) => |
126 CSUBGOAL (fn (goal, i) => |
127 (case try iff_oracle goal of |
127 (case try iff_oracle goal of |
128 NONE => no_tac |
128 NONE => no_tac |
129 | SOME thm => rtac thm i))*} |
129 | SOME thm => rtac thm i))*} |
130 |
130 |