equal
deleted
inserted
replaced
1162 specification of axioms! Invoking the oracle only works within the |
1162 specification of axioms! Invoking the oracle only works within the |
1163 scope of the resulting theory. |
1163 scope of the resulting theory. |
1164 |
1164 |
1165 \end{description} |
1165 \end{description} |
1166 |
1166 |
1167 See @{"file" "~~/src/HOL/ex/Iff_Oracle.thy"} for a worked example of |
1167 See @{file "~~/src/HOL/ex/Iff_Oracle.thy"} for a worked example of |
1168 defining a new primitive rule as oracle, and turning it into a proof |
1168 defining a new primitive rule as oracle, and turning it into a proof |
1169 method. |
1169 method. |
1170 *} |
1170 *} |
1171 |
1171 |
1172 |
1172 |