src/HOL/Quickcheck_Narrowing.thy
changeset 48891 c0eafbd55de3
parent 48565 7c497a239007
child 48901 5e0455e29339
--- a/src/HOL/Quickcheck_Narrowing.thy	Wed Aug 22 22:47:16 2012 +0200
+++ b/src/HOL/Quickcheck_Narrowing.thy	Wed Aug 22 22:55:41 2012 +0200
@@ -5,11 +5,9 @@
 theory Quickcheck_Narrowing
 imports Quickcheck_Exhaustive
 keywords "find_unused_assms" :: diag
-uses
+uses  (* FIXME session files *)
   ("Tools/Quickcheck/PNF_Narrowing_Engine.hs")
   ("Tools/Quickcheck/Narrowing_Engine.hs")
-  ("Tools/Quickcheck/narrowing_generators.ML")
-  ("Tools/Quickcheck/find_unused_assms.ML")
 begin
 
 subsection {* Counterexample generator *}
@@ -340,7 +338,7 @@
 
 subsubsection {* Setting up the counterexample generator *}
 
-use "Tools/Quickcheck/narrowing_generators.ML"
+ML_file "Tools/Quickcheck/narrowing_generators.ML"
 
 setup {* Narrowing_Generators.setup *}
 
@@ -447,7 +445,7 @@
 
 subsection {* The @{text find_unused_assms} command *}
 
-use "Tools/Quickcheck/find_unused_assms.ML"
+ML_file "Tools/Quickcheck/find_unused_assms.ML"
 
 subsection {* Closing up *}