src/HOL/Boogie/ROOT.ML
author blanchet
Thu, 14 Apr 2011 11:24:05 +0200
changeset 42348 187354e22c7d
parent 33615 261abc2e3155
permissions -rw-r--r--
improve on 0b05cc14c2cb: make sure that a literal variable "?foo" isn't accidentally renamed "?Q", which might be enough to confuse the new Skolemizer (cf. "Clausify.thy" example)

use_thys ["Boogie"];