changeset 69605 | a96320074298 |
parent 69597 | ff784d5a5bfb |
--- a/src/HOL/Statespace/DistinctTreeProver.thy Sun Jan 06 13:44:33 2019 +0100 +++ b/src/HOL/Statespace/DistinctTreeProver.thy Sun Jan 06 15:04:34 2019 +0100 @@ -630,6 +630,6 @@ text \<open>Now we have all the theorems in place that are needed for the certificate generating ML functions.\<close> -ML_file "distinct_tree_prover.ML" +ML_file \<open>distinct_tree_prover.ML\<close> end