equal
deleted
inserted
replaced
142 * An interface to the Stanford Validity Checker (SVC) is available through the |
142 * An interface to the Stanford Validity Checker (SVC) is available through the |
143 tactic svc_tac. Propositional tautologies and theorems of linear arithmetic |
143 tactic svc_tac. Propositional tautologies and theorems of linear arithmetic |
144 are proved automatically. SVC must be installed separately, and its results |
144 are proved automatically. SVC must be installed separately, and its results |
145 must be TAKEN ON TRUST (Isabelle does not check the proofs, but tags any |
145 must be TAKEN ON TRUST (Isabelle does not check the proofs, but tags any |
146 invocation of the underlying oracle). For SVC see |
146 invocation of the underlying oracle). For SVC see |
147 http://agamemnon.stanford.edu/~levitt/vc/index.html |
147 http://verify.stanford.edu/SVC |
148 |
148 |
149 * IsaMakefile: the HOL-Real target now builds an actual image; |
149 * IsaMakefile: the HOL-Real target now builds an actual image; |
150 |
150 |
151 |
151 |
152 ** HOL misc ** |
152 ** HOL misc ** |