equal
deleted
inserted
replaced
74 in Buffer.content (trans t Buffer.empty) end\<close> |
74 in Buffer.content (trans t Buffer.empty) end\<close> |
75 |
75 |
76 text \<open> |
76 text \<open> |
77 Here is the string representation of the term @{term "p = (q = p)"}: |
77 Here is the string representation of the term @{term "p = (q = p)"}: |
78 |
78 |
79 @{ML_response |
79 @{ML_matchresult |
80 "translate @{term \"p = (q = p)\"}" |
80 "translate @{term \"p = (q = p)\"}" |
81 "\" ( p <=> ( q <=> p ) ) \""} |
81 "\" ( p <=> ( q <=> p ) ) \""} |
82 |
82 |
83 Let us check, what the solver returns when given a tautology: |
83 Let us check, what the solver returns when given a tautology: |
84 |
84 |
85 @{ML_response |
85 @{ML_matchresult |
86 "IffSolver.decide (translate @{term \"p = (q = p) = q\"})" |
86 "IffSolver.decide (translate @{term \"p = (q = p) = q\"})" |
87 "true"} |
87 "true"} |
88 |
88 |
89 And here is what it returns for a formula which is not valid: |
89 And here is what it returns for a formula which is not valid: |
90 |
90 |
91 @{ML_response |
91 @{ML_matchresult |
92 "IffSolver.decide (translate @{term \"p = (q = p)\"})" |
92 "IffSolver.decide (translate @{term \"p = (q = p)\"})" |
93 "false"} |
93 "false"} |
94 \<close> |
94 \<close> |
95 |
95 |
96 text \<open> |
96 text \<open> |
111 else error "Proof failed."\<close> |
111 else error "Proof failed."\<close> |
112 |
112 |
113 text \<open> |
113 text \<open> |
114 Here is what we get when applying the oracle: |
114 Here is what we get when applying the oracle: |
115 |
115 |
116 @{ML_response_fake "iff_oracle @{cprop \"p = (p::bool)\"}" "p = p"} |
116 @{ML_matchresult_fake "iff_oracle @{cprop \"p = (p::bool)\"}" "p = p"} |
117 |
117 |
118 (FIXME: is there a better way to present the theorem?) |
118 (FIXME: is there a better way to present the theorem?) |
119 |
119 |
120 To be able to use our oracle for Isar proofs, we wrap it into a tactic: |
120 To be able to use our oracle for Isar proofs, we wrap it into a tactic: |
121 \<close> |
121 \<close> |