src/HOL/Nitpick.thy
changeset 46319 c248e4f1be74
parent 45970 b6d0cff57d96
child 46324 e4bccf5ec61e
     1.1 --- a/src/HOL/Nitpick.thy	Mon Jan 23 17:40:31 2012 +0100
     1.2 +++ b/src/HOL/Nitpick.thy	Mon Jan 23 17:40:31 2012 +0100
     1.3 @@ -23,11 +23,11 @@
     1.4       ("Tools/Nitpick/nitpick_model.ML")
     1.5       ("Tools/Nitpick/nitpick.ML")
     1.6       ("Tools/Nitpick/nitpick_isar.ML")
     1.7 +     ("Tools/Nitpick/nitpick_tptp.ML")
     1.8       ("Tools/Nitpick/nitpick_tests.ML")
     1.9 -     ("Tools/Nitpick/nitrox.ML")
    1.10  begin
    1.11  
    1.12 -typedecl iota (* for Nitrox *)
    1.13 +typedecl iota (* for TPTP *)
    1.14  typedecl bisim_iterator
    1.15  
    1.16  axiomatization unknown :: 'a
    1.17 @@ -223,8 +223,8 @@
    1.18  use "Tools/Nitpick/nitpick_model.ML"
    1.19  use "Tools/Nitpick/nitpick.ML"
    1.20  use "Tools/Nitpick/nitpick_isar.ML"
    1.21 +use "Tools/Nitpick/nitpick_tptp.ML"
    1.22  use "Tools/Nitpick/nitpick_tests.ML"
    1.23 -use "Tools/Nitpick/nitrox.ML"
    1.24  
    1.25  setup {*
    1.26    Nitpick_Isar.setup #>