src/HOL/Quickcheck_Narrowing.thy
changeset 48891 c0eafbd55de3
parent 48565 7c497a239007
child 48901 5e0455e29339
     1.1 --- a/src/HOL/Quickcheck_Narrowing.thy	Wed Aug 22 22:47:16 2012 +0200
     1.2 +++ b/src/HOL/Quickcheck_Narrowing.thy	Wed Aug 22 22:55:41 2012 +0200
     1.3 @@ -5,11 +5,9 @@
     1.4  theory Quickcheck_Narrowing
     1.5  imports Quickcheck_Exhaustive
     1.6  keywords "find_unused_assms" :: diag
     1.7 -uses
     1.8 +uses  (* FIXME session files *)
     1.9    ("Tools/Quickcheck/PNF_Narrowing_Engine.hs")
    1.10    ("Tools/Quickcheck/Narrowing_Engine.hs")
    1.11 -  ("Tools/Quickcheck/narrowing_generators.ML")
    1.12 -  ("Tools/Quickcheck/find_unused_assms.ML")
    1.13  begin
    1.14  
    1.15  subsection {* Counterexample generator *}
    1.16 @@ -340,7 +338,7 @@
    1.17  
    1.18  subsubsection {* Setting up the counterexample generator *}
    1.19  
    1.20 -use "Tools/Quickcheck/narrowing_generators.ML"
    1.21 +ML_file "Tools/Quickcheck/narrowing_generators.ML"
    1.22  
    1.23  setup {* Narrowing_Generators.setup *}
    1.24  
    1.25 @@ -447,7 +445,7 @@
    1.26  
    1.27  subsection {* The @{text find_unused_assms} command *}
    1.28  
    1.29 -use "Tools/Quickcheck/find_unused_assms.ML"
    1.30 +ML_file "Tools/Quickcheck/find_unused_assms.ML"
    1.31  
    1.32  subsection {* Closing up *}
    1.33