src/HOL/Statespace/DistinctTreeProver.thy
changeset 48891 c0eafbd55de3
parent 45358 4849133d7a78
child 53015 a1119cf551e8
     1.1 --- a/src/HOL/Statespace/DistinctTreeProver.thy	Wed Aug 22 22:47:16 2012 +0200
     1.2 +++ b/src/HOL/Statespace/DistinctTreeProver.thy	Wed Aug 22 22:55:41 2012 +0200
     1.3 @@ -6,7 +6,6 @@
     1.4  
     1.5  theory DistinctTreeProver 
     1.6  imports Main
     1.7 -uses ("distinct_tree_prover.ML")
     1.8  begin
     1.9  
    1.10  text {* A state space manages a set of (abstract) names and assumes
    1.11 @@ -631,7 +630,7 @@
    1.12  text {* Now we have all the theorems in place that are needed for the
    1.13  certificate generating ML functions. *}
    1.14  
    1.15 -use "distinct_tree_prover.ML"
    1.16 +ML_file "distinct_tree_prover.ML"
    1.17  
    1.18  (* Uncomment for profiling or debugging *)
    1.19  (*