equal
deleted
inserted
replaced
17 \smallskip |
17 \smallskip |
18 |
18 |
19 \begin{readmore} |
19 \begin{readmore} |
20 A short introduction to oracles can be found in [isar-ref: no suitable label |
20 A short introduction to oracles can be found in [isar-ref: no suitable label |
21 for section 3.11]. A simple example, which we will slightly extend here, |
21 for section 3.11]. A simple example, which we will slightly extend here, |
22 is given in @{ML_file "FOL/ex/IffOracle.thy"}. The raw interface for adding |
22 is given in @{ML_file "FOL/ex/Iff_Oracle.thy"}. The raw interface for adding |
23 oracles is @{ML add_oracle in Thm} in @{ML_file "Pure/thm.ML"}. |
23 oracles is @{ML add_oracle in Thm} in @{ML_file "Pure/thm.ML"}. |
24 \end{readmore} |
24 \end{readmore} |
25 |
25 |
26 For our explanation here, we restrict ourselves to decide propositional |
26 For our explanation here, we restrict ourselves to decide propositional |
27 formulae which consist only of equivalences between propositional variables, |
27 formulae which consist only of equivalences between propositional variables, |