# HG changeset patch # User blanchet # Date 1425397065 -3600 # Node ID de392405a851743376358e0bca73f8f804612784 # Parent d09cc83cdce9d23a37609e333edff4205e5ef2d4 import 'Main' to be on the safe side diff -r d09cc83cdce9 -r de392405a851 src/HOL/Mirabelle/Mirabelle.thy --- a/src/HOL/Mirabelle/Mirabelle.thy Sun Mar 01 23:35:41 2015 +0100 +++ b/src/HOL/Mirabelle/Mirabelle.thy Tue Mar 03 16:37:45 2015 +0100 @@ -3,7 +3,7 @@ *) theory Mirabelle -imports Sledgehammer +imports Main begin ML_file "Tools/mirabelle.ML"