equal
deleted
inserted
replaced
71 \smallskip |
71 \smallskip |
72 |
72 |
73 \begin{readmore} |
73 \begin{readmore} |
74 A short introduction to oracles can be found in [isar-ref: no suitable label |
74 A short introduction to oracles can be found in [isar-ref: no suitable label |
75 for section 3.11]. A simple example, which we will slightly extend here, |
75 for section 3.11]. A simple example, which we will slightly extend here, |
76 is given in @{ML_file "FOL/ex/IffOracle"}. The raw interface for adding |
76 is given in @{ML_file "FOL/ex/IffOracle.thy"}. The raw interface for adding |
77 oracles is @{ML add_oracle in Thm} in @{ML_file "Pure/thm"}. |
77 oracles is @{ML add_oracle in Thm} in @{ML_file "Pure/thm.ML"}. |
78 \end{readmore} |
78 \end{readmore} |
79 |
79 |
80 For our explanation here, we restrict ourselves to decide propositional |
80 For our explanation here, we restrict ourselves to decide propositional |
81 formulae which consist only of equivalences between propositional variables, |
81 formulae which consist only of equivalences between propositional variables, |
82 i.e. we want to decide whether @{term "P = (Q = P) = Q"} is a tautology. |
82 i.e. we want to decide whether @{term "P = (Q = P) = Q"} is a tautology. |