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


use_thy "MutabelleExtra";