merge
authorblanchet
Wed Sep 08 16:01:06 2010 +0200 (2010-09-08)
changeset 39223022f16801e4e
parent 39218 7f4fb691e4b6
parent 39222 decf607a5a67
child 39224 39e0d3b86112
child 39225 52960d359969
child 39257 eec61233dbad
merge
src/HOL/IsaMakefile
src/HOL/Nitpick.thy
src/HOL/Tools/Nitpick/minipick.ML
src/HOL/Tools/Sledgehammer/sledgehammer.ML
     1.1 --- a/doc-src/manual.bib	Wed Sep 08 14:46:21 2010 +0200
     1.2 +++ b/doc-src/manual.bib	Wed Sep 08 16:01:06 2010 +0200
     1.3 @@ -1372,7 +1372,7 @@
     1.4  @inproceedings{sutcliffe-2000,
     1.5    author = "Geoff Sutcliffe",
     1.6    title = "System Description: {SystemOnTPTP}",
     1.7 -  editor = "J. G. Carbonell and J. Siekmann",
     1.8 +  editor = "David McAllester",
     1.9    booktitle	= {Automated Deduction --- {CADE}-17 International Conference},
    1.10    series = "Lecture Notes in Artificial Intelligence",
    1.11    volume = {1831},
     2.1 --- a/src/HOL/IsaMakefile	Wed Sep 08 14:46:21 2010 +0200
     2.2 +++ b/src/HOL/IsaMakefile	Wed Sep 08 16:01:06 2010 +0200
     2.3 @@ -278,7 +278,6 @@
     2.4    Tools/nat_numeral_simprocs.ML \
     2.5    Tools/Nitpick/kodkod.ML \
     2.6    Tools/Nitpick/kodkod_sat.ML \
     2.7 -  Tools/Nitpick/minipick.ML \
     2.8    Tools/Nitpick/nitpick.ML \
     2.9    Tools/Nitpick/nitpick_hol.ML \
    2.10    Tools/Nitpick/nitpick_isar.ML \
    2.11 @@ -667,11 +666,10 @@
    2.12    Nitpick_Examples/Core_Nits.thy Nitpick_Examples/Datatype_Nits.thy \
    2.13    Nitpick_Examples/Hotel_Nits.thy Nitpick_Examples/Induct_Nits.thy \
    2.14    Nitpick_Examples/Integer_Nits.thy Nitpick_Examples/Manual_Nits.thy \
    2.15 -  Nitpick_Examples/Mini_Nits.thy Nitpick_Examples/Mono_Nits.thy \
    2.16 -  Nitpick_Examples/Nitpick_Examples.thy Nitpick_Examples/Pattern_Nits.thy \
    2.17 -  Nitpick_Examples/Record_Nits.thy Nitpick_Examples/Refute_Nits.thy \
    2.18 -  Nitpick_Examples/Special_Nits.thy Nitpick_Examples/Tests_Nits.thy \
    2.19 -  Nitpick_Examples/Typedef_Nits.thy
    2.20 +  Nitpick_Examples/Mono_Nits.thy Nitpick_Examples/Nitpick_Examples.thy \
    2.21 +  Nitpick_Examples/Pattern_Nits.thy Nitpick_Examples/Record_Nits.thy \
    2.22 +  Nitpick_Examples/Refute_Nits.thy Nitpick_Examples/Special_Nits.thy \
    2.23 +  Nitpick_Examples/Tests_Nits.thy Nitpick_Examples/Typedef_Nits.thy
    2.24  	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Nitpick_Examples
    2.25  
    2.26  
     3.1 --- a/src/HOL/Nitpick.thy	Wed Sep 08 14:46:21 2010 +0200
     3.2 +++ b/src/HOL/Nitpick.thy	Wed Sep 08 16:01:06 2010 +0200
     3.3 @@ -24,7 +24,6 @@
     3.4       ("Tools/Nitpick/nitpick.ML")
     3.5       ("Tools/Nitpick/nitpick_isar.ML")
     3.6       ("Tools/Nitpick/nitpick_tests.ML")
     3.7 -     ("Tools/Nitpick/minipick.ML")
     3.8  begin
     3.9  
    3.10  typedecl bisim_iterator
    3.11 @@ -237,7 +236,6 @@
    3.12  use "Tools/Nitpick/nitpick.ML"
    3.13  use "Tools/Nitpick/nitpick_isar.ML"
    3.14  use "Tools/Nitpick/nitpick_tests.ML"
    3.15 -use "Tools/Nitpick/minipick.ML"
    3.16  
    3.17  setup {* Nitpick_Isar.setup *}
    3.18  
     4.1 --- a/src/HOL/Nitpick_Examples/Core_Nits.thy	Wed Sep 08 14:46:21 2010 +0200
     4.2 +++ b/src/HOL/Nitpick_Examples/Core_Nits.thy	Wed Sep 08 16:01:06 2010 +0200
     4.3 @@ -32,44 +32,6 @@
     4.4  nitpick [card = 1\<midarrow>12, expect = none]
     4.5  by auto
     4.6  
     4.7 -lemma "(split o curry) f = f"
     4.8 -nitpick [card = 1\<midarrow>12, expect = none]
     4.9 -by auto
    4.10 -
    4.11 -lemma "(curry o split) f = f"
    4.12 -nitpick [card = 1\<midarrow>12, expect = none]
    4.13 -by auto
    4.14 -
    4.15 -lemma "(split o curry) f = (\<lambda>x. x) f"
    4.16 -nitpick [card = 1\<midarrow>12, expect = none]
    4.17 -by auto
    4.18 -
    4.19 -lemma "(curry o split) f = (\<lambda>x. x) f"
    4.20 -nitpick [card = 1\<midarrow>12, expect = none]
    4.21 -by auto
    4.22 -
    4.23 -lemma "((split o curry) f) p = ((\<lambda>x. x) f) p"
    4.24 -nitpick [card = 1\<midarrow>12, expect = none]
    4.25 -by auto
    4.26 -
    4.27 -lemma "((curry o split) f) x = ((\<lambda>x. x) f) x"
    4.28 -nitpick [card = 1\<midarrow>12, expect = none]
    4.29 -by auto
    4.30 -
    4.31 -lemma "((curry o split) f) x y = ((\<lambda>x. x) f) x y"
    4.32 -nitpick [card = 1\<midarrow>12, expect = none]
    4.33 -by auto
    4.34 -
    4.35 -lemma "split o curry = (\<lambda>x. x)"
    4.36 -nitpick [card = 1\<midarrow>12, expect = none]
    4.37 -apply (rule ext)+
    4.38 -by auto
    4.39 -
    4.40 -lemma "curry o split = (\<lambda>x. x)"
    4.41 -nitpick [card = 1\<midarrow>12, expect = none]
    4.42 -apply (rule ext)+
    4.43 -by auto
    4.44 -
    4.45  lemma "split (\<lambda>x y. f (x, y)) = f"
    4.46  nitpick [card = 1\<midarrow>12, expect = none]
    4.47  by auto
    4.48 @@ -150,31 +112,31 @@
    4.49  oops
    4.50  
    4.51  lemma "{a, b} = {b}"
    4.52 -nitpick [card = 100, expect = genuine]
    4.53 +nitpick [card = 50, expect = genuine]
    4.54  oops
    4.55  
    4.56  lemma "(a\<Colon>'a\<times>'a, a\<Colon>'a\<times>'a) \<in> R"
    4.57  nitpick [card = 1, expect = genuine]
    4.58 -nitpick [card = 20, expect = genuine]
    4.59 +nitpick [card = 10, expect = genuine]
    4.60  nitpick [card = 5, dont_box, expect = genuine]
    4.61  oops
    4.62  
    4.63  lemma "f (g\<Colon>'a\<Rightarrow>'a) = x"
    4.64  nitpick [card = 3, expect = genuine]
    4.65  nitpick [card = 3, dont_box, expect = genuine]
    4.66 -nitpick [card = 10, expect = genuine]
    4.67 +nitpick [card = 8, expect = genuine]
    4.68  oops
    4.69  
    4.70  lemma "f (a, b) = x"
    4.71 -nitpick [card = 12, expect = genuine]
    4.72 +nitpick [card = 10, expect = genuine]
    4.73  oops
    4.74  
    4.75  lemma "f (a, a) = f (c, d)"
    4.76 -nitpick [card = 12, expect = genuine]
    4.77 +nitpick [card = 10, expect = genuine]
    4.78  oops
    4.79  
    4.80  lemma "(x\<Colon>'a) = (\<lambda>a. \<lambda>b. \<lambda>c. if c then a else b) x x True"
    4.81 -nitpick [card = 1\<midarrow>12, expect = none]
    4.82 +nitpick [card = 1\<midarrow>10, expect = none]
    4.83  by auto
    4.84  
    4.85  lemma "\<exists>F. F a b = G a b"
    4.86 @@ -187,7 +149,7 @@
    4.87  oops
    4.88  
    4.89  lemma "(A\<Colon>'a\<times>'a, B\<Colon>'a\<times>'a) \<in> R \<Longrightarrow> (A, B) \<in> R"
    4.90 -nitpick [card = 20, expect = none]
    4.91 +nitpick [card = 15, expect = none]
    4.92  by auto
    4.93  
    4.94  lemma "(A, B) \<in> R \<or> (\<exists>C. (A, C) \<in> R \<and> (C, B) \<in> R) \<Longrightarrow> 
    4.95 @@ -204,30 +166,30 @@
    4.96  lemma "x = y"
    4.97  nitpick [card 'a = 1, expect = none]
    4.98  nitpick [card 'a = 2, expect = genuine]
    4.99 -nitpick [card 'a = 200, expect = genuine]
   4.100 +nitpick [card 'a = 100, expect = genuine]
   4.101  oops
   4.102  
   4.103  lemma "\<forall>x. x = y"
   4.104  nitpick [card 'a = 1, expect = none]
   4.105  nitpick [card 'a = 2, expect = genuine]
   4.106 -nitpick [card 'a = 200, expect = genuine]
   4.107 +nitpick [card 'a = 100, expect = genuine]
   4.108  oops
   4.109  
   4.110  lemma "\<forall>x\<Colon>'a \<Rightarrow> bool. x = y"
   4.111  nitpick [card 'a = 1, expect = genuine]
   4.112 -nitpick [card 'a = 200, expect = genuine]
   4.113 +nitpick [card 'a = 100, expect = genuine]
   4.114  oops
   4.115  
   4.116  lemma "\<exists>x\<Colon>'a \<Rightarrow> bool. x = y"
   4.117 -nitpick [card 'a = 1\<midarrow>20, expect = none]
   4.118 +nitpick [card 'a = 1\<midarrow>15, expect = none]
   4.119  by auto
   4.120  
   4.121  lemma "\<exists>x y\<Colon>'a \<Rightarrow> bool. x = y"
   4.122 -nitpick [card = 1\<midarrow>20, expect = none]
   4.123 +nitpick [card = 1\<midarrow>15, expect = none]
   4.124  by auto
   4.125  
   4.126  lemma "\<forall>x. \<exists>y. f x y = f x (g x)"
   4.127 -nitpick [card = 1\<midarrow>5, expect = none]
   4.128 +nitpick [card = 1\<midarrow>4, expect = none]
   4.129  by auto
   4.130  
   4.131  lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. f u v w x = f u (g u) w (h u w)"
   4.132 @@ -241,7 +203,6 @@
   4.133  lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. \<forall>y. \<exists>z.
   4.134         f u v w x y z = f u (g u) w (h u w) y (k u w y)"
   4.135  nitpick [card = 1\<midarrow>2, expect = none]
   4.136 -nitpick [card = 3, expect = none]
   4.137  sorry
   4.138  
   4.139  lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. \<forall>y. \<exists>z.
   4.140 @@ -288,18 +249,6 @@
   4.141  nitpick [expect = none]
   4.142  sorry
   4.143  
   4.144 -lemma "\<forall>x\<Colon>'a\<times>'b. if (\<exists>y. x = y) then True else False"
   4.145 -nitpick [expect = none]
   4.146 -sorry
   4.147 -
   4.148 -lemma "(\<not> (\<exists>x. P x)) \<longleftrightarrow> (\<forall>x. \<not> P x)"
   4.149 -nitpick [expect = none]
   4.150 -by auto
   4.151 -
   4.152 -lemma "(\<not> \<not> (\<exists>x. P x)) \<longleftrightarrow> (\<not> (\<forall>x. \<not> P x))"
   4.153 -nitpick [expect = none]
   4.154 -by auto
   4.155 -
   4.156  lemma "(\<exists>x\<Colon>'a. \<forall>y. P x y) \<or> (\<exists>x\<Colon>'a \<times> 'a. \<forall>y. P y x)"
   4.157  nitpick [card 'a = 1, expect = genuine]
   4.158  nitpick [card 'a = 5, expect = genuine]
   4.159 @@ -383,10 +332,6 @@
   4.160  nitpick [card = 20, expect = genuine]
   4.161  oops
   4.162  
   4.163 -lemma "I = (\<lambda>x. x) \<Longrightarrow> (op \<equiv> x) \<equiv> (\<lambda>y. (x \<equiv> I y))"
   4.164 -nitpick [expect = none]
   4.165 -by auto
   4.166 -
   4.167  lemma "P x \<equiv> P x"
   4.168  nitpick [card = 1\<midarrow>10, expect = none]
   4.169  by auto
   4.170 @@ -456,14 +401,12 @@
   4.171  oops
   4.172  
   4.173  lemma "\<exists>!x. x = undefined"
   4.174 -nitpick [card = 30, expect = none]
   4.175 +nitpick [card = 15, expect = none]
   4.176  by auto
   4.177  
   4.178  lemma "x = All \<Longrightarrow> False"
   4.179  nitpick [card = 1, dont_box, expect = genuine]
   4.180 -nitpick [card = 2, dont_box, expect = genuine]
   4.181 -nitpick [card = 8, dont_box, expect = genuine]
   4.182 -nitpick [card = 10, dont_box, expect = unknown]
   4.183 +nitpick [card = 5, dont_box, expect = genuine]
   4.184  oops
   4.185  
   4.186  lemma "\<forall>x. f x y = f x y"
   4.187 @@ -482,15 +425,9 @@
   4.188  nitpick [expect = genuine]
   4.189  oops
   4.190  
   4.191 -lemma "I = (\<lambda>x. x) \<Longrightarrow> All P = All (\<lambda>x. P (I x))"
   4.192 -nitpick [expect = none]
   4.193 -by auto
   4.194 -
   4.195  lemma "x = Ex \<Longrightarrow> False"
   4.196  nitpick [card = 1, dont_box, expect = genuine]
   4.197 -nitpick [card = 2, dont_box, expect = genuine]
   4.198 -nitpick [card = 6, dont_box, expect = genuine]
   4.199 -nitpick [card = 10, dont_box, expect = unknown]
   4.200 +nitpick [card = 5, dont_box, expect = genuine]
   4.201  oops
   4.202  
   4.203  lemma "\<exists>x. f x y = f x y"
   4.204 @@ -513,10 +450,6 @@
   4.205  nitpick [expect = genuine]
   4.206  oops
   4.207  
   4.208 -lemma "Ex (\<lambda>x. f x y = f y x) = False"
   4.209 -nitpick [expect = genuine]
   4.210 -oops
   4.211 -
   4.212  lemma "Ex (\<lambda>x. f x y \<noteq> f x y) = False"
   4.213  nitpick [expect = none]
   4.214  by auto
   4.215 @@ -525,11 +458,6 @@
   4.216  nitpick [expect = none]
   4.217  by auto
   4.218  
   4.219 -lemma "I = (\<lambda>x. x) \<Longrightarrow> (op =) = (\<lambda>x. (op= (I x)))"
   4.220 -      "I = (\<lambda>x. x) \<Longrightarrow> (op =) = (\<lambda>x y. x = (I y))"
   4.221 -nitpick [expect = none]
   4.222 -by auto
   4.223 -
   4.224  lemma "x = y \<Longrightarrow> y = x"
   4.225  nitpick [expect = none]
   4.226  by auto
   4.227 @@ -555,35 +483,10 @@
   4.228  nitpick [expect = none]
   4.229  by auto
   4.230  
   4.231 -lemma "\<not> a \<Longrightarrow> \<not> (a \<and> b)" "\<not> b \<Longrightarrow> \<not> (a \<and> b)"
   4.232 -nitpick [expect = none]
   4.233 -by auto
   4.234 -
   4.235 -lemma "I = (\<lambda>x. x) \<Longrightarrow> (op \<or>) = (\<lambda>x. op \<or> (I x))"
   4.236 -      "I = (\<lambda>x. x) \<Longrightarrow> (op \<or>) = (\<lambda>x y. x \<or> (I y))"
   4.237 -nitpick [expect = none]
   4.238 -by auto
   4.239 -
   4.240 -lemma "a \<Longrightarrow> a \<or> b" "b \<Longrightarrow> a \<or> b"
   4.241 -nitpick [expect = none]
   4.242 -by auto
   4.243 -
   4.244 -lemma "\<not> (a \<or> b) \<Longrightarrow> \<not> a" "\<not> (a \<or> b) \<Longrightarrow> \<not> b"
   4.245 -nitpick [expect = none]
   4.246 -by auto
   4.247 -
   4.248  lemma "(op \<longrightarrow>) = (\<lambda>x. op\<longrightarrow> x)" "(op\<longrightarrow> ) = (\<lambda>x y. x \<longrightarrow> y)"
   4.249  nitpick [expect = none]
   4.250  by auto
   4.251  
   4.252 -lemma "\<not>a \<Longrightarrow> a \<longrightarrow> b" "b \<Longrightarrow> a \<longrightarrow> b"
   4.253 -nitpick [expect = none]
   4.254 -by auto
   4.255 -
   4.256 -lemma "\<lbrakk>a; \<not> b\<rbrakk> \<Longrightarrow> \<not> (a \<longrightarrow> b)"
   4.257 -nitpick [expect = none]
   4.258 -by auto
   4.259 -
   4.260  lemma "((if a then b else c) = d) = ((a \<longrightarrow> (b = d)) \<and> (\<not> a \<longrightarrow> (c = d)))"
   4.261  nitpick [expect = none]
   4.262  by auto
   4.263 @@ -592,12 +495,6 @@
   4.264  nitpick [expect = none]
   4.265  by auto
   4.266  
   4.267 -lemma "I = (\<lambda>x. x) \<Longrightarrow> If = (\<lambda>x. If (I x))"
   4.268 -      "J = (\<lambda>x. x) \<Longrightarrow> If = (\<lambda>x y. If x (J y))"
   4.269 -      "K = (\<lambda>x. x) \<Longrightarrow> If = (\<lambda>x y z. If x y (K z))"
   4.270 -nitpick [expect = none]
   4.271 -by auto
   4.272 -
   4.273  lemma "fst (x, y) = x"
   4.274  nitpick [expect = none]
   4.275  by (simp add: fst_def)
   4.276 @@ -642,10 +539,6 @@
   4.277  nitpick [expect = none]
   4.278  by auto
   4.279  
   4.280 -lemma "I = (\<lambda>x. x) \<Longrightarrow> snd = (\<lambda>x. snd (I x))"
   4.281 -nitpick [expect = none]
   4.282 -by auto
   4.283 -
   4.284  lemma "fst (x, y) = snd (y, x)"
   4.285  nitpick [expect = none]
   4.286  by auto
   4.287 @@ -662,10 +555,6 @@
   4.288  nitpick [expect = none]
   4.289  by auto
   4.290  
   4.291 -lemma "I = (\<lambda>x. x) \<Longrightarrow> curry Id = (\<lambda>x y. Id (x, I y))"
   4.292 -nitpick [expect = none]
   4.293 -by (simp add: curry_def)
   4.294 -
   4.295  lemma "{} = (\<lambda>x. False)"
   4.296  nitpick [expect = none]
   4.297  by (metis Collect_def empty_def)
   4.298 @@ -722,10 +611,6 @@
   4.299  nitpick [expect = none]
   4.300  by (simp add: mem_def)
   4.301  
   4.302 -lemma "I = (\<lambda>x. x) \<Longrightarrow> insert = (\<lambda>x. insert (I x))"
   4.303 -nitpick [expect = none]
   4.304 -by simp
   4.305 -
   4.306  lemma "insert = (\<lambda>x y. insert x (y \<union> y))"
   4.307  nitpick [expect = none]
   4.308  by simp
   4.309 @@ -743,10 +628,6 @@
   4.310  nitpick [expect = none]
   4.311  by auto
   4.312  
   4.313 -lemma "I = (\<lambda>x. x) \<Longrightarrow> rtrancl = (\<lambda>x. rtrancl (I x))"
   4.314 -nitpick [card = 1\<midarrow>2, expect = none]
   4.315 -by auto
   4.316 -
   4.317  lemma "((x, x), (x, x)) \<in> rtrancl {}"
   4.318  nitpick [card = 1\<midarrow>5, expect = none]
   4.319  by auto
   4.320 @@ -755,42 +636,18 @@
   4.321  nitpick [card = 1\<midarrow>5, expect = none]
   4.322  by auto
   4.323  
   4.324 -lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<union> = (\<lambda>x y. op \<union> x (I y))"
   4.325 -nitpick [card = 1\<midarrow>5, expect = none]
   4.326 -by auto
   4.327 -
   4.328  lemma "a \<in> A \<Longrightarrow> a \<in> (A \<union> B)" "b \<in> B \<Longrightarrow> b \<in> (A \<union> B)"
   4.329  nitpick [expect = none]
   4.330  by auto
   4.331  
   4.332 -lemma "a \<in> (A \<union> B) \<Longrightarrow> a \<in> A \<or> a \<in> B"
   4.333 -nitpick [expect = none]
   4.334 -by auto
   4.335 -
   4.336  lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<inter> = (\<lambda>x. op \<inter> (I x))"
   4.337  nitpick [card = 1\<midarrow>5, expect = none]
   4.338  by auto
   4.339  
   4.340 -lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<inter> = (\<lambda>x y. op \<inter> x (I y))"
   4.341 -nitpick [card = 1\<midarrow>5, expect = none]
   4.342 -by auto
   4.343 -
   4.344  lemma "a \<notin> A \<Longrightarrow> a \<notin> (A \<inter> B)" "b \<notin> B \<Longrightarrow> b \<notin> (A \<inter> B)"
   4.345  nitpick [card = 1\<midarrow>5, expect = none]
   4.346  by auto
   4.347  
   4.348 -lemma "a \<notin> (A \<inter> B) \<Longrightarrow> a \<notin> A \<or> a \<notin> B"
   4.349 -nitpick [expect = none]
   4.350 -by auto
   4.351 -
   4.352 -lemma "I = (\<lambda>x. x) \<Longrightarrow> op - = (\<lambda>x\<Colon>'a set. op - (I x))"
   4.353 -nitpick [card = 1\<midarrow>5, expect = none]
   4.354 -by auto
   4.355 -
   4.356 -lemma "I = (\<lambda>x. x) \<Longrightarrow> op - = (\<lambda>x y\<Colon>'a set. op - x (I y))"
   4.357 -nitpick [card = 1\<midarrow>5, expect = none]
   4.358 -by auto
   4.359 -
   4.360  lemma "x \<in> ((A\<Colon>'a set) - B) \<longleftrightarrow> x \<in> A \<and> x \<notin> B"
   4.361  nitpick [card = 1\<midarrow>5, expect = none]
   4.362  by auto
   4.363 @@ -799,22 +656,10 @@
   4.364  nitpick [card = 1\<midarrow>5, expect = none]
   4.365  by auto
   4.366  
   4.367 -lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<subset> = (\<lambda>x y. op \<subset> x (I y))"
   4.368 -nitpick [card = 1\<midarrow>5, expect = none]
   4.369 -by auto
   4.370 -
   4.371  lemma "A \<subset> B \<Longrightarrow> (\<forall>a \<in> A. a \<in> B) \<and> (\<exists>b \<in> B. b \<notin> A)"
   4.372  nitpick [card = 1\<midarrow>5, expect = none]
   4.373  by auto
   4.374  
   4.375 -lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<subseteq> = (\<lambda>x. op \<subseteq> (I x))"
   4.376 -nitpick [card = 1\<midarrow>5, expect = none]
   4.377 -by auto
   4.378 -
   4.379 -lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<subseteq> = (\<lambda>x y. op \<subseteq> x (I y))"
   4.380 -nitpick [card = 1\<midarrow>5, expect = none]
   4.381 -by auto
   4.382 -
   4.383  lemma "A \<subseteq> B \<Longrightarrow> \<forall>a \<in> A. a \<in> B"
   4.384  nitpick [card = 1\<midarrow>5, expect = none]
   4.385  by auto
   4.386 @@ -843,10 +688,6 @@
   4.387  nitpick [card 'a = 10, expect = genuine]
   4.388  oops
   4.389  
   4.390 -lemma "I = (\<lambda>x. x) \<Longrightarrow> finite = (\<lambda>x. finite (I x))"
   4.391 -nitpick [card = 1\<midarrow>7, expect = none]
   4.392 -oops
   4.393 -
   4.394  lemma "finite A"
   4.395  nitpick [expect = none]
   4.396  oops
     5.1 --- a/src/HOL/Nitpick_Examples/Nitpick_Examples.thy	Wed Sep 08 14:46:21 2010 +0200
     5.2 +++ b/src/HOL/Nitpick_Examples/Nitpick_Examples.thy	Wed Sep 08 16:01:06 2010 +0200
     5.3 @@ -7,7 +7,7 @@
     5.4  
     5.5  theory Nitpick_Examples
     5.6  imports Core_Nits Datatype_Nits Hotel_Nits Induct_Nits Integer_Nits Manual_Nits
     5.7 -        Mini_Nits Mono_Nits Pattern_Nits Record_Nits Refute_Nits Special_Nits
     5.8 -        Tests_Nits Typedef_Nits
     5.9 +        Mono_Nits Pattern_Nits Record_Nits Refute_Nits Special_Nits Tests_Nits
    5.10 +        Typedef_Nits
    5.11  begin
    5.12  end
     6.1 --- a/src/HOL/Tools/Nitpick/kodkod_sat.ML	Wed Sep 08 14:46:21 2010 +0200
     6.2 +++ b/src/HOL/Tools/Nitpick/kodkod_sat.ML	Wed Sep 08 16:01:06 2010 +0200
     6.3 @@ -71,7 +71,7 @@
     6.4                       [if null markers then "External" else "ExternalV2",
     6.5                        dir ^ dir_sep ^ exec, base ^ ".cnf",
     6.6                        if dev = ToFile then out_file else ""] @ markers @
     6.7 -                      (if dev = ToFile then [out_file] else []) @ args
     6.8 +                     (if dev = ToFile then [out_file] else []) @ args
     6.9                     end)
    6.10  fun dynamic_entry_for_info incremental (name, Internal (Java, mode, ss)) =
    6.11      if incremental andalso mode = Batch then NONE else SOME (name, K ss)
     7.1 --- a/src/HOL/Tools/Nitpick/minipick.ML	Wed Sep 08 14:46:21 2010 +0200
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,327 +0,0 @@
     7.4 -(*  Title:      HOL/Tools/Nitpick/minipick.ML
     7.5 -    Author:     Jasmin Blanchette, TU Muenchen
     7.6 -    Copyright   2009, 2010
     7.7 -
     7.8 -Finite model generation for HOL formulas using Kodkod, minimalistic version.
     7.9 -*)
    7.10 -
    7.11 -signature MINIPICK =
    7.12 -sig
    7.13 -  datatype rep = SRep | RRep
    7.14 -  type styp = Nitpick_Util.styp
    7.15 -
    7.16 -  val vars_for_bound_var :
    7.17 -    (typ -> int) -> rep -> typ list -> int -> Kodkod.rel_expr list
    7.18 -  val rel_expr_for_bound_var :
    7.19 -    (typ -> int) -> rep -> typ list -> int -> Kodkod.rel_expr
    7.20 -  val decls_for : rep -> (typ -> int) -> typ list -> typ -> Kodkod.decl list
    7.21 -  val false_atom : Kodkod.rel_expr
    7.22 -  val true_atom : Kodkod.rel_expr
    7.23 -  val formula_from_atom : Kodkod.rel_expr -> Kodkod.formula
    7.24 -  val atom_from_formula : Kodkod.formula -> Kodkod.rel_expr
    7.25 -  val kodkod_problem_from_term :
    7.26 -    Proof.context -> (typ -> int) -> term -> Kodkod.problem
    7.27 -  val solve_any_kodkod_problem : theory -> Kodkod.problem list -> string
    7.28 -end;
    7.29 -
    7.30 -structure Minipick : MINIPICK =
    7.31 -struct
    7.32 -
    7.33 -open Kodkod
    7.34 -open Nitpick_Util
    7.35 -open Nitpick_HOL
    7.36 -open Nitpick_Peephole
    7.37 -open Nitpick_Kodkod
    7.38 -
    7.39 -datatype rep = SRep | RRep
    7.40 -
    7.41 -fun check_type ctxt (Type (@{type_name fun}, Ts)) =
    7.42 -    List.app (check_type ctxt) Ts
    7.43 -  | check_type ctxt (Type (@{type_name prod}, Ts)) =
    7.44 -    List.app (check_type ctxt) Ts
    7.45 -  | check_type _ @{typ bool} = ()
    7.46 -  | check_type _ (TFree (_, @{sort "{}"})) = ()
    7.47 -  | check_type _ (TFree (_, @{sort HOL.type})) = ()
    7.48 -  | check_type ctxt T =
    7.49 -    raise NOT_SUPPORTED ("type " ^ quote (Syntax.string_of_typ ctxt T))
    7.50 -
    7.51 -fun atom_schema_of SRep card (Type (@{type_name fun}, [T1, T2])) =
    7.52 -    replicate_list (card T1) (atom_schema_of SRep card T2)
    7.53 -  | atom_schema_of RRep card (Type (@{type_name fun}, [T1, @{typ bool}])) =
    7.54 -    atom_schema_of SRep card T1
    7.55 -  | atom_schema_of RRep card (Type (@{type_name fun}, [T1, T2])) =
    7.56 -    atom_schema_of SRep card T1 @ atom_schema_of RRep card T2
    7.57 -  | atom_schema_of _ card (Type (@{type_name prod}, Ts)) =
    7.58 -    maps (atom_schema_of SRep card) Ts
    7.59 -  | atom_schema_of _ card T = [card T]
    7.60 -val arity_of = length ooo atom_schema_of
    7.61 -
    7.62 -fun index_for_bound_var _ [_] 0 = 0
    7.63 -  | index_for_bound_var card (_ :: Ts) 0 =
    7.64 -    index_for_bound_var card Ts 0 + arity_of SRep card (hd Ts)
    7.65 -  | index_for_bound_var card Ts n = index_for_bound_var card (tl Ts) (n - 1)
    7.66 -fun vars_for_bound_var card R Ts j =
    7.67 -  map (curry Var 1) (index_seq (index_for_bound_var card Ts j)
    7.68 -                               (arity_of R card (nth Ts j)))
    7.69 -val rel_expr_for_bound_var = foldl1 Product oooo vars_for_bound_var
    7.70 -fun decls_for R card Ts T =
    7.71 -  map2 (curry DeclOne o pair 1)
    7.72 -       (index_seq (index_for_bound_var card (T :: Ts) 0)
    7.73 -                  (arity_of R card (nth (T :: Ts) 0)))
    7.74 -       (map (AtomSeq o rpair 0) (atom_schema_of R card T))
    7.75 -
    7.76 -val atom_product = foldl1 Product o map Atom
    7.77 -
    7.78 -val false_atom = Atom 0
    7.79 -val true_atom = Atom 1
    7.80 -
    7.81 -fun formula_from_atom r = RelEq (r, true_atom)
    7.82 -fun atom_from_formula f = RelIf (f, true_atom, false_atom)
    7.83 -
    7.84 -fun kodkod_formula_from_term ctxt card frees =
    7.85 -  let
    7.86 -    fun R_rep_from_S_rep (Type (@{type_name fun}, [T1, @{typ bool}])) r =
    7.87 -        let
    7.88 -          val jss = atom_schema_of SRep card T1 |> map (rpair 0)
    7.89 -                    |> all_combinations
    7.90 -        in
    7.91 -          map2 (fn i => fn js =>
    7.92 -                   RelIf (formula_from_atom (Project (r, [Num i])),
    7.93 -                          atom_product js, empty_n_ary_rel (length js)))
    7.94 -               (index_seq 0 (length jss)) jss
    7.95 -          |> foldl1 Union
    7.96 -        end
    7.97 -      | R_rep_from_S_rep (Type (@{type_name fun}, [T1, T2])) r =
    7.98 -        let
    7.99 -          val jss = atom_schema_of SRep card T1 |> map (rpair 0)
   7.100 -                    |> all_combinations
   7.101 -          val arity2 = arity_of SRep card T2
   7.102 -        in
   7.103 -          map2 (fn i => fn js =>
   7.104 -                   Product (atom_product js,
   7.105 -                            Project (r, num_seq (i * arity2) arity2)
   7.106 -                            |> R_rep_from_S_rep T2))
   7.107 -               (index_seq 0 (length jss)) jss
   7.108 -          |> foldl1 Union
   7.109 -        end
   7.110 -      | R_rep_from_S_rep _ r = r
   7.111 -    fun S_rep_from_R_rep Ts (T as Type (@{type_name fun}, _)) r =
   7.112 -        Comprehension (decls_for SRep card Ts T,
   7.113 -            RelEq (R_rep_from_S_rep T
   7.114 -                       (rel_expr_for_bound_var card SRep (T :: Ts) 0), r))
   7.115 -      | S_rep_from_R_rep _ _ r = r
   7.116 -    fun to_F Ts t =
   7.117 -      (case t of
   7.118 -         @{const Not} $ t1 => Not (to_F Ts t1)
   7.119 -       | @{const False} => False
   7.120 -       | @{const True} => True
   7.121 -       | Const (@{const_name All}, _) $ Abs (_, T, t') =>
   7.122 -         All (decls_for SRep card Ts T, to_F (T :: Ts) t')
   7.123 -       | (t0 as Const (@{const_name All}, _)) $ t1 =>
   7.124 -         to_F Ts (t0 $ eta_expand Ts t1 1)
   7.125 -       | Const (@{const_name Ex}, _) $ Abs (_, T, t') =>
   7.126 -         Exist (decls_for SRep card Ts T, to_F (T :: Ts) t')
   7.127 -       | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
   7.128 -         to_F Ts (t0 $ eta_expand Ts t1 1)
   7.129 -       | Const (@{const_name HOL.eq}, _) $ t1 $ t2 =>
   7.130 -         RelEq (to_R_rep Ts t1, to_R_rep Ts t2)
   7.131 -       | Const (@{const_name ord_class.less_eq},
   7.132 -                Type (@{type_name fun},
   7.133 -                      [Type (@{type_name fun}, [_, @{typ bool}]), _]))
   7.134 -         $ t1 $ t2 =>
   7.135 -         Subset (to_R_rep Ts t1, to_R_rep Ts t2)
   7.136 -       | @{const HOL.conj} $ t1 $ t2 => And (to_F Ts t1, to_F Ts t2)
   7.137 -       | @{const HOL.disj} $ t1 $ t2 => Or (to_F Ts t1, to_F Ts t2)
   7.138 -       | @{const HOL.implies} $ t1 $ t2 => Implies (to_F Ts t1, to_F Ts t2)
   7.139 -       | t1 $ t2 => Subset (to_S_rep Ts t2, to_R_rep Ts t1)
   7.140 -       | Free _ => raise SAME ()
   7.141 -       | Term.Var _ => raise SAME ()
   7.142 -       | Bound _ => raise SAME ()
   7.143 -       | Const (s, _) => raise NOT_SUPPORTED ("constant " ^ quote s)
   7.144 -       | _ => raise TERM ("Minipick.kodkod_formula_from_term.to_F", [t]))
   7.145 -      handle SAME () => formula_from_atom (to_R_rep Ts t)
   7.146 -    and to_S_rep Ts t =
   7.147 -      case t of
   7.148 -        Const (@{const_name Pair}, _) $ t1 $ t2 =>
   7.149 -        Product (to_S_rep Ts t1, to_S_rep Ts t2)
   7.150 -      | Const (@{const_name Pair}, _) $ _ => to_S_rep Ts (eta_expand Ts t 1)
   7.151 -      | Const (@{const_name Pair}, _) => to_S_rep Ts (eta_expand Ts t 2)
   7.152 -      | Const (@{const_name fst}, _) $ t1 =>
   7.153 -        let val fst_arity = arity_of SRep card (fastype_of1 (Ts, t)) in
   7.154 -          Project (to_S_rep Ts t1, num_seq 0 fst_arity)
   7.155 -        end
   7.156 -      | Const (@{const_name fst}, _) => to_S_rep Ts (eta_expand Ts t 1)
   7.157 -      | Const (@{const_name snd}, _) $ t1 =>
   7.158 -        let
   7.159 -          val pair_arity = arity_of SRep card (fastype_of1 (Ts, t1))
   7.160 -          val snd_arity = arity_of SRep card (fastype_of1 (Ts, t))
   7.161 -          val fst_arity = pair_arity - snd_arity
   7.162 -        in Project (to_S_rep Ts t1, num_seq fst_arity snd_arity) end
   7.163 -      | Const (@{const_name snd}, _) => to_S_rep Ts (eta_expand Ts t 1)
   7.164 -      | Bound j => rel_expr_for_bound_var card SRep Ts j
   7.165 -      | _ => S_rep_from_R_rep Ts (fastype_of1 (Ts, t)) (to_R_rep Ts t)
   7.166 -    and to_R_rep Ts t =
   7.167 -      (case t of
   7.168 -         @{const Not} => to_R_rep Ts (eta_expand Ts t 1)
   7.169 -       | Const (@{const_name All}, _) => to_R_rep Ts (eta_expand Ts t 1)
   7.170 -       | Const (@{const_name Ex}, _) => to_R_rep Ts (eta_expand Ts t 1)
   7.171 -       | Const (@{const_name HOL.eq}, _) $ _ => to_R_rep Ts (eta_expand Ts t 1)
   7.172 -       | Const (@{const_name HOL.eq}, _) => to_R_rep Ts (eta_expand Ts t 2)
   7.173 -       | Const (@{const_name ord_class.less_eq},
   7.174 -                Type (@{type_name fun},
   7.175 -                      [Type (@{type_name fun}, [_, @{typ bool}]), _])) $ _ =>
   7.176 -         to_R_rep Ts (eta_expand Ts t 1)
   7.177 -       | Const (@{const_name ord_class.less_eq}, _) =>
   7.178 -         to_R_rep Ts (eta_expand Ts t 2)
   7.179 -       | @{const HOL.conj} $ _ => to_R_rep Ts (eta_expand Ts t 1)
   7.180 -       | @{const HOL.conj} => to_R_rep Ts (eta_expand Ts t 2)
   7.181 -       | @{const HOL.disj} $ _ => to_R_rep Ts (eta_expand Ts t 1)
   7.182 -       | @{const HOL.disj} => to_R_rep Ts (eta_expand Ts t 2)
   7.183 -       | @{const HOL.implies} $ _ => to_R_rep Ts (eta_expand Ts t 1)
   7.184 -       | @{const HOL.implies} => to_R_rep Ts (eta_expand Ts t 2)
   7.185 -       | Const (@{const_name bot_class.bot},
   7.186 -                T as Type (@{type_name fun}, [_, @{typ bool}])) =>
   7.187 -         empty_n_ary_rel (arity_of RRep card T)
   7.188 -       | Const (@{const_name insert}, _) $ t1 $ t2 =>
   7.189 -         Union (to_S_rep Ts t1, to_R_rep Ts t2)
   7.190 -       | Const (@{const_name insert}, _) $ _ => to_R_rep Ts (eta_expand Ts t 1)
   7.191 -       | Const (@{const_name insert}, _) => to_R_rep Ts (eta_expand Ts t 2)
   7.192 -       | Const (@{const_name trancl}, _) $ t1 =>
   7.193 -         if arity_of RRep card (fastype_of1 (Ts, t1)) = 2 then
   7.194 -           Closure (to_R_rep Ts t1)
   7.195 -         else
   7.196 -           raise NOT_SUPPORTED "transitive closure for function or pair type"
   7.197 -       | Const (@{const_name trancl}, _) => to_R_rep Ts (eta_expand Ts t 1)
   7.198 -       | Const (@{const_name semilattice_inf_class.inf},
   7.199 -                Type (@{type_name fun},
   7.200 -                      [Type (@{type_name fun}, [_, @{typ bool}]), _]))
   7.201 -         $ t1 $ t2 =>
   7.202 -         Intersect (to_R_rep Ts t1, to_R_rep Ts t2)
   7.203 -       | Const (@{const_name semilattice_inf_class.inf}, _) $ _ =>
   7.204 -         to_R_rep Ts (eta_expand Ts t 1)
   7.205 -       | Const (@{const_name semilattice_inf_class.inf}, _) =>
   7.206 -         to_R_rep Ts (eta_expand Ts t 2)
   7.207 -       | Const (@{const_name semilattice_sup_class.sup},
   7.208 -                Type (@{type_name fun},
   7.209 -                      [Type (@{type_name fun}, [_, @{typ bool}]), _]))
   7.210 -         $ t1 $ t2 =>
   7.211 -         Union (to_R_rep Ts t1, to_R_rep Ts t2)
   7.212 -       | Const (@{const_name semilattice_sup_class.sup}, _) $ _ =>
   7.213 -         to_R_rep Ts (eta_expand Ts t 1)
   7.214 -       | Const (@{const_name semilattice_sup_class.sup}, _) =>
   7.215 -         to_R_rep Ts (eta_expand Ts t 2)
   7.216 -       | Const (@{const_name minus_class.minus},
   7.217 -                Type (@{type_name fun},
   7.218 -                      [Type (@{type_name fun}, [_, @{typ bool}]), _]))
   7.219 -         $ t1 $ t2 =>
   7.220 -         Difference (to_R_rep Ts t1, to_R_rep Ts t2)
   7.221 -       | Const (@{const_name minus_class.minus},
   7.222 -                Type (@{type_name fun},
   7.223 -                      [Type (@{type_name fun}, [_, @{typ bool}]), _])) $ _ =>
   7.224 -         to_R_rep Ts (eta_expand Ts t 1)
   7.225 -       | Const (@{const_name minus_class.minus},
   7.226 -                Type (@{type_name fun},
   7.227 -                      [Type (@{type_name fun}, [_, @{typ bool}]), _])) =>
   7.228 -         to_R_rep Ts (eta_expand Ts t 2)
   7.229 -       | Const (@{const_name Pair}, _) $ _ $ _ => raise SAME ()
   7.230 -       | Const (@{const_name Pair}, _) $ _ => raise SAME ()
   7.231 -       | Const (@{const_name Pair}, _) => raise SAME ()
   7.232 -       | Const (@{const_name fst}, _) $ _ => raise SAME ()
   7.233 -       | Const (@{const_name fst}, _) => raise SAME ()
   7.234 -       | Const (@{const_name snd}, _) $ _ => raise SAME ()
   7.235 -       | Const (@{const_name snd}, _) => raise SAME ()
   7.236 -       | Const (_, @{typ bool}) => atom_from_formula (to_F Ts t)
   7.237 -       | Free (x as (_, T)) =>
   7.238 -         Rel (arity_of RRep card T, find_index (curry (op =) x) frees)
   7.239 -       | Term.Var _ => raise NOT_SUPPORTED "schematic variables"
   7.240 -       | Bound _ => raise SAME ()
   7.241 -       | Abs (_, T, t') =>
   7.242 -         (case fastype_of1 (T :: Ts, t') of
   7.243 -            @{typ bool} => Comprehension (decls_for SRep card Ts T,
   7.244 -                                          to_F (T :: Ts) t')
   7.245 -          | T' => Comprehension (decls_for SRep card Ts T @
   7.246 -                                 decls_for RRep card (T :: Ts) T',
   7.247 -                                 Subset (rel_expr_for_bound_var card RRep
   7.248 -                                                              (T' :: T :: Ts) 0,
   7.249 -                                         to_R_rep (T :: Ts) t')))
   7.250 -       | t1 $ t2 =>
   7.251 -         (case fastype_of1 (Ts, t) of
   7.252 -            @{typ bool} => atom_from_formula (to_F Ts t)
   7.253 -          | T =>
   7.254 -            let val T2 = fastype_of1 (Ts, t2) in
   7.255 -              case arity_of SRep card T2 of
   7.256 -                1 => Join (to_S_rep Ts t2, to_R_rep Ts t1)
   7.257 -              | arity2 =>
   7.258 -                let val res_arity = arity_of RRep card T in
   7.259 -                  Project (Intersect
   7.260 -                      (Product (to_S_rep Ts t2,
   7.261 -                                atom_schema_of RRep card T
   7.262 -                                |> map (AtomSeq o rpair 0) |> foldl1 Product),
   7.263 -                       to_R_rep Ts t1),
   7.264 -                      num_seq arity2 res_arity)
   7.265 -                end
   7.266 -            end)
   7.267 -       | _ => raise NOT_SUPPORTED ("term " ^
   7.268 -                                   quote (Syntax.string_of_term ctxt t)))
   7.269 -      handle SAME () => R_rep_from_S_rep (fastype_of1 (Ts, t)) (to_S_rep Ts t)
   7.270 -  in to_F [] end
   7.271 -
   7.272 -fun bound_for_free card i (s, T) =
   7.273 -  let val js = atom_schema_of RRep card T in
   7.274 -    ([((length js, i), s)],
   7.275 -     [TupleSet [], atom_schema_of RRep card T |> map (rpair 0)
   7.276 -                   |> tuple_set_from_atom_schema])
   7.277 -  end
   7.278 -
   7.279 -fun declarative_axiom_for_rel_expr card Ts (Type (@{type_name fun}, [T1, T2]))
   7.280 -                                   r =
   7.281 -    if body_type T2 = bool_T then
   7.282 -      True
   7.283 -    else
   7.284 -      All (decls_for SRep card Ts T1,
   7.285 -           declarative_axiom_for_rel_expr card (T1 :: Ts) T2
   7.286 -               (List.foldl Join r (vars_for_bound_var card SRep (T1 :: Ts) 0)))
   7.287 -  | declarative_axiom_for_rel_expr _ _ _ r = One r
   7.288 -fun declarative_axiom_for_free card i (_, T) =
   7.289 -  declarative_axiom_for_rel_expr card [] T (Rel (arity_of RRep card T, i))
   7.290 -
   7.291 -fun kodkod_problem_from_term ctxt raw_card t =
   7.292 -  let
   7.293 -    val thy = ProofContext.theory_of ctxt
   7.294 -    fun card (Type (@{type_name fun}, [T1, T2])) =
   7.295 -        reasonable_power (card T2) (card T1)
   7.296 -      | card (Type (@{type_name prod}, [T1, T2])) = card T1 * card T2
   7.297 -      | card @{typ bool} = 2
   7.298 -      | card T = Int.max (1, raw_card T)
   7.299 -    val neg_t = @{const Not} $ Object_Logic.atomize_term thy t
   7.300 -    val _ = fold_types (K o check_type ctxt) neg_t ()
   7.301 -    val frees = Term.add_frees neg_t []
   7.302 -    val bounds = map2 (bound_for_free card) (index_seq 0 (length frees)) frees
   7.303 -    val declarative_axioms =
   7.304 -      map2 (declarative_axiom_for_free card) (index_seq 0 (length frees)) frees
   7.305 -    val formula = kodkod_formula_from_term ctxt card frees neg_t
   7.306 -                  |> fold_rev (curry And) declarative_axioms
   7.307 -    val univ_card = univ_card 0 0 0 bounds formula
   7.308 -  in
   7.309 -    {comment = "", settings = [], univ_card = univ_card, tuple_assigns = [],
   7.310 -     bounds = bounds, int_bounds = [], expr_assigns = [], formula = formula}
   7.311 -  end
   7.312 -
   7.313 -fun solve_any_kodkod_problem thy problems =
   7.314 -  let
   7.315 -    val {overlord, ...} = Nitpick_Isar.default_params thy []
   7.316 -    val max_threads = 1
   7.317 -    val max_solutions = 1
   7.318 -  in
   7.319 -    case solve_any_problem overlord NONE max_threads max_solutions problems of
   7.320 -      JavaNotInstalled => "unknown"
   7.321 -    | JavaTooOld => "unknown"
   7.322 -    | KodkodiNotInstalled => "unknown"
   7.323 -    | Normal ([], _, _) => "none"
   7.324 -    | Normal _ => "genuine"
   7.325 -    | TimedOut _ => "unknown"
   7.326 -    | Interrupted _ => "unknown"
   7.327 -    | Error (s, _) => error ("Kodkod error: " ^ s)
   7.328 -  end
   7.329 -
   7.330 -end;
     8.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Sep 08 14:46:21 2010 +0200
     8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Sep 08 16:01:06 2010 +0200
     8.3 @@ -452,8 +452,7 @@
     8.4              else
     8.5                ()
     8.6            end
     8.7 -      (* FIXME no threads in user-space *)
     8.8 -      in if blocking then run () else Toplevel.thread true (tap run) |> K () end
     8.9 +      in if blocking then run () else Future.fork run |> K () end
    8.10  
    8.11  val setup =
    8.12    dest_dir_setup
     9.1 --- a/src/HOL/Tools/try.ML	Wed Sep 08 14:46:21 2010 +0200
     9.2 +++ b/src/HOL/Tools/try.ML	Wed Sep 08 16:01:06 2010 +0200
     9.3 @@ -51,9 +51,9 @@
     9.4                        else "")) I (#goal o Proof.goal)
     9.5               (apply_named_method_on_first_goal name (Proof.context_of st)) st
     9.6  
     9.7 -val all_goals_named_methods = ["auto", "safe"]
     9.8 +val all_goals_named_methods = ["auto"]
     9.9  val first_goal_named_methods =
    9.10 -  ["simp", "fast", "fastsimp", "force", "best", "blast"]
    9.11 +  ["simp", "fast", "fastsimp", "force", "best", "blast", "arith"]
    9.12  val do_methods =
    9.13    map do_named_method_on_first_goal all_goals_named_methods @
    9.14    map do_named_method first_goal_named_methods