src/HOL/Hoare/ROOT.ML
author bulwahn
Tue, 08 May 2012 14:31:03 +0200
changeset 47893 4cf901b1089a
parent 35316 870dfea4f9c0
permissions -rw-r--r--
specialised fact in the Record theory should not be appear in proofs discovered by sledgehammer
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
     1
35316
870dfea4f9c0 dropped axclass; dropped Id; session theory Hoare.thy
haftmann
parents: 24584
diff changeset
     2
use_thy "Hoare";