src/HOL/Number_Theory/ROOT.ML
author blanchet
Tue, 24 Apr 2012 13:56:13 +0200
changeset 47728 6ee015f6ea4b
parent 33615 261abc2e3155
permissions -rw-r--r--
reintroduce file offsets in Mirabelle output, but make sure they are not influenced by the length of the path

use_thys ["Number_Theory"];