src/HOL/base.ML
author boehmes
Thu, 27 May 2010 17:09:06 +0200
changeset 37155 e3f18cfc9829
parent 33615 261abc2e3155
child 37694 19e8b730ddeb
permissions -rw-r--r--
sort signature in SMT-LIB output (improves sharing of SMT certificates: goals of the same logical structure are translated into equal SMT-LIB benchmarks)

(*side-entry for HOL-Base*)
use_thys ["HOL"];