src/HOL/Nitpick.thy
changeset 46324 e4bccf5ec61e
parent 46319 c248e4f1be74
child 46950 d0181abdbdac
     1.1 --- a/src/HOL/Nitpick.thy	Mon Jan 23 17:40:32 2012 +0100
     1.2 +++ b/src/HOL/Nitpick.thy	Mon Jan 23 17:40:32 2012 +0100
     1.3 @@ -23,11 +23,9 @@
     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  begin
    1.10  
    1.11 -typedecl iota (* for TPTP *)
    1.12  typedecl bisim_iterator
    1.13  
    1.14  axiomatization unknown :: 'a
    1.15 @@ -223,7 +221,6 @@
    1.16  use "Tools/Nitpick/nitpick_model.ML"
    1.17  use "Tools/Nitpick/nitpick.ML"
    1.18  use "Tools/Nitpick/nitpick_isar.ML"
    1.19 -use "Tools/Nitpick/nitpick_tptp.ML"
    1.20  use "Tools/Nitpick/nitpick_tests.ML"
    1.21  
    1.22  setup {*
    1.23 @@ -240,8 +237,7 @@
    1.24      fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac Abs_Frac Rep_Frac zero_frac
    1.25      one_frac num denom norm_frac frac plus_frac times_frac uminus_frac
    1.26      number_of_frac inverse_frac less_frac less_eq_frac of_frac
    1.27 -hide_type (open) iota bisim_iterator fun_box pair_box unsigned_bit signed_bit
    1.28 -    word
    1.29 +hide_type (open) bisim_iterator fun_box pair_box unsigned_bit signed_bit word
    1.30  hide_fact (open) Ex1_unfold rtrancl_unfold rtranclp_unfold tranclp_unfold
    1.31      prod_def refl'_def wf'_def card'_def setsum'_def
    1.32      fold_graph'_def The_psimp Eps_psimp unit_case_unfold nat_case_unfold