src/FOLP/IFOLP.thy
changeset 48891 c0eafbd55de3
parent 45602 2a858377c3d2
child 51306 f0e5af7aa68b
     1.1 --- a/src/FOLP/IFOLP.thy	Wed Aug 22 22:47:16 2012 +0200
     1.2 +++ b/src/FOLP/IFOLP.thy	Wed Aug 22 22:55:41 2012 +0200
     1.3 @@ -7,9 +7,10 @@
     1.4  
     1.5  theory IFOLP
     1.6  imports Pure
     1.7 -uses "~~/src/Tools/misc_legacy.ML" ("hypsubst.ML") ("intprover.ML")
     1.8  begin
     1.9  
    1.10 +ML_file "~~/src/Tools/misc_legacy.ML"
    1.11 +
    1.12  setup Pure_Thy.old_appl_syntax_setup
    1.13  
    1.14  classes "term"
    1.15 @@ -587,7 +588,7 @@
    1.16  
    1.17  lemma thin_refl: "!!X. [|p:x=x; PROP W|] ==> PROP W" .
    1.18  
    1.19 -use "hypsubst.ML"
    1.20 +ML_file "hypsubst.ML"
    1.21  
    1.22  ML {*
    1.23  structure Hypsubst = Hypsubst
    1.24 @@ -609,7 +610,7 @@
    1.25  open Hypsubst;
    1.26  *}
    1.27  
    1.28 -use "intprover.ML"
    1.29 +ML_file "intprover.ML"
    1.30  
    1.31  
    1.32  (*** Rewrite rules ***)