--- a/src/FOLP/FOLP.thy Wed Aug 22 22:47:16 2012 +0200
+++ b/src/FOLP/FOLP.thy Wed Aug 22 22:55:41 2012 +0200
@@ -7,8 +7,6 @@
theory FOLP
imports IFOLP
-uses
- ("classical.ML") ("simp.ML") ("simpdata.ML")
begin
axiomatization cla :: "[p=>p]=>p"
@@ -99,8 +97,8 @@
apply assumption
done
-use "classical.ML" (* Patched 'cos matching won't instantiate proof *)
-use "simp.ML" (* Patched 'cos matching won't instantiate proof *)
+ML_file "classical.ML" (* Patched because matching won't instantiate proof *)
+ML_file "simp.ML" (* Patched because matching won't instantiate proof *)
ML {*
structure Cla = Classical
@@ -139,6 +137,6 @@
apply (tactic {* ALLGOALS (Cla.fast_tac FOLP_cs) *})
done
-use "simpdata.ML"
+ML_file "simpdata.ML"
end