src/HOLCF/IMP/ROOT.ML
author blanchet
Fri, 17 Sep 2010 00:54:56 +0200
changeset 39499 40bf0f66b994
parent 35174 e15040ae75d7
permissions -rw-r--r--
simplify Skolem handling; things are much easier now that Sledgehammer doesn't skolemize, only Metis
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
26438
090ced251009 fixed theory imports;
wenzelm
parents: 24106
diff changeset
     1
use_thys ["HoareEx"];