src/HOL/Word/ROOT.ML
author kuncar
Thu, 24 May 2012 14:20:23 +0200
changeset 47982 7aa35601ff65
parent 33615 261abc2e3155
permissions -rw-r--r--
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule

use_thys ["Word"];