src/HOL/Nitpick.thy
changeset 48891 c0eafbd55de3
parent 47988 e4b69e10b990
child 49989 34d0ac1bdac6
     1.1 --- a/src/HOL/Nitpick.thy	Wed Aug 22 22:47:16 2012 +0200
     1.2 +++ b/src/HOL/Nitpick.thy	Wed Aug 22 22:55:41 2012 +0200
     1.3 @@ -10,21 +10,6 @@
     1.4  theory Nitpick
     1.5  imports Map Quotient SAT Record
     1.6  keywords "nitpick" :: diag and "nitpick_params" :: thy_decl
     1.7 -uses ("Tools/Nitpick/kodkod.ML")
     1.8 -     ("Tools/Nitpick/kodkod_sat.ML")
     1.9 -     ("Tools/Nitpick/nitpick_util.ML")
    1.10 -     ("Tools/Nitpick/nitpick_hol.ML")
    1.11 -     ("Tools/Nitpick/nitpick_preproc.ML")
    1.12 -     ("Tools/Nitpick/nitpick_mono.ML")
    1.13 -     ("Tools/Nitpick/nitpick_scope.ML")
    1.14 -     ("Tools/Nitpick/nitpick_peephole.ML")
    1.15 -     ("Tools/Nitpick/nitpick_rep.ML")
    1.16 -     ("Tools/Nitpick/nitpick_nut.ML")
    1.17 -     ("Tools/Nitpick/nitpick_kodkod.ML")
    1.18 -     ("Tools/Nitpick/nitpick_model.ML")
    1.19 -     ("Tools/Nitpick/nitpick.ML")
    1.20 -     ("Tools/Nitpick/nitpick_isar.ML")
    1.21 -     ("Tools/Nitpick/nitpick_tests.ML")
    1.22  begin
    1.23  
    1.24  typedecl bisim_iterator
    1.25 @@ -212,21 +197,21 @@
    1.26  definition of_frac :: "'a \<Rightarrow> 'b\<Colon>{inverse,ring_1}" where
    1.27  "of_frac q \<equiv> of_int (num q) / of_int (denom q)"
    1.28  
    1.29 -use "Tools/Nitpick/kodkod.ML"
    1.30 -use "Tools/Nitpick/kodkod_sat.ML"
    1.31 -use "Tools/Nitpick/nitpick_util.ML"
    1.32 -use "Tools/Nitpick/nitpick_hol.ML"
    1.33 -use "Tools/Nitpick/nitpick_mono.ML"
    1.34 -use "Tools/Nitpick/nitpick_preproc.ML"
    1.35 -use "Tools/Nitpick/nitpick_scope.ML"
    1.36 -use "Tools/Nitpick/nitpick_peephole.ML"
    1.37 -use "Tools/Nitpick/nitpick_rep.ML"
    1.38 -use "Tools/Nitpick/nitpick_nut.ML"
    1.39 -use "Tools/Nitpick/nitpick_kodkod.ML"
    1.40 -use "Tools/Nitpick/nitpick_model.ML"
    1.41 -use "Tools/Nitpick/nitpick.ML"
    1.42 -use "Tools/Nitpick/nitpick_isar.ML"
    1.43 -use "Tools/Nitpick/nitpick_tests.ML"
    1.44 +ML_file "Tools/Nitpick/kodkod.ML"
    1.45 +ML_file "Tools/Nitpick/kodkod_sat.ML"
    1.46 +ML_file "Tools/Nitpick/nitpick_util.ML"
    1.47 +ML_file "Tools/Nitpick/nitpick_hol.ML"
    1.48 +ML_file "Tools/Nitpick/nitpick_mono.ML"
    1.49 +ML_file "Tools/Nitpick/nitpick_preproc.ML"
    1.50 +ML_file "Tools/Nitpick/nitpick_scope.ML"
    1.51 +ML_file "Tools/Nitpick/nitpick_peephole.ML"
    1.52 +ML_file "Tools/Nitpick/nitpick_rep.ML"
    1.53 +ML_file "Tools/Nitpick/nitpick_nut.ML"
    1.54 +ML_file "Tools/Nitpick/nitpick_kodkod.ML"
    1.55 +ML_file "Tools/Nitpick/nitpick_model.ML"
    1.56 +ML_file "Tools/Nitpick/nitpick.ML"
    1.57 +ML_file "Tools/Nitpick/nitpick_isar.ML"
    1.58 +ML_file "Tools/Nitpick/nitpick_tests.ML"
    1.59  
    1.60  setup {*
    1.61    Nitpick_Isar.setup #>