src/HOL/Decision_Procs/ROOT.ML
author haftmann
Mon, 29 Nov 2010 22:47:55 +0100
changeset 40818 b117df72e56b
parent 33615 261abc2e3155
permissions -rw-r--r--
reorienting iff in Quotient_rel prevents simplifier looping; lemma QuotientI; tuned theory text

use_thys ["Decision_Procs"];