author haftmann Thu, 17 Jun 2010 10:02:29 +0200 changeset 37443 68112e3d29e5 parent 37442 037ee7b712b2 (current diff) parent 37436 2d76997730a6 (diff) child 37444 2e7e7ff21e25 child 37454 9132a5955127
merged
```--- a/src/HOL/Algebra/README.html	Tue Jun 15 14:28:22 2010 +0200
+++ b/src/HOL/Algebra/README.html	Thu Jun 17 10:02:29 2010 +0200
@@ -20,7 +20,7 @@

<H2>GroupTheory, including Sylow's Theorem</H2>

-<P>These proofs are mainly by Florian Kammller.  (Later, Larry
+<P>These proofs are mainly by Florian Kamm&uuml;ller.  (Later, Larry
Paulson simplified some of the proofs.)  These theories were indeed
the original motivation for locales.
```
```--- a/src/HOL/Nitpick_Examples/Core_Nits.thy	Tue Jun 15 14:28:22 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Core_Nits.thy	Thu Jun 17 10:02:29 2010 +0200
@@ -1053,50 +1053,50 @@

nitpick_params [full_descrs, max_potential = 1]

-lemma "(THE j. j > Suc 10 \<and> j \<le> 11) \<noteq> 0"
-nitpick [card nat = 4, expect = potential]
-nitpick [card nat = 14, expect = potential] (* unfortunate *)
+lemma "(THE j. j > Suc 2 \<and> j \<le> 3) \<noteq> 0"
+nitpick [card nat = 2, expect = potential]
+nitpick [card nat = 6, expect = potential] (* unfortunate *)
oops

-lemma "(THE j. j > Suc 10 \<and> j \<le> 12) = x \<Longrightarrow> x \<noteq> 0"
-nitpick [card nat = 4, expect = potential]
-nitpick [card nat = 14, expect = none]
+lemma "(THE j. j > Suc 2 \<and> j \<le> 4) = x \<Longrightarrow> x \<noteq> 0"
+nitpick [card nat = 2, expect = potential]
+nitpick [card nat = 6, expect = none]
sorry

-lemma "(THE j. j > Suc 10 \<and> j \<le> 12) = x \<Longrightarrow> x = 12"
-nitpick [card nat = 4, expect = potential]
-nitpick [card nat = 14, expect = none]
+lemma "(THE j. j > Suc 2 \<and> j \<le> 4) = x \<Longrightarrow> x = 4"
+nitpick [card nat = 2, expect = potential]
+nitpick [card nat = 6, expect = none]
sorry

-lemma "(THE j. j > Suc 10 \<and> j \<le> 13) = x \<Longrightarrow> x = 12"
-nitpick [card nat = 14, expect = genuine]
+lemma "(THE j. j > Suc 2 \<and> j \<le> 5) = x \<Longrightarrow> x = 4"
+nitpick [card nat = 6, expect = genuine]
oops

-lemma "(THE j. j > Suc 10 \<and> j \<le> 13) = x \<Longrightarrow> x = 12 \<or> x = 13"
-nitpick [card nat = 14, expect = genuine]
+lemma "(THE j. j > Suc 2 \<and> j \<le> 5) = x \<Longrightarrow> x = 4 \<or> x = 5"
+nitpick [card nat = 6, expect = genuine]
oops

-lemma "(SOME j. j > Suc 10 \<and> j \<le> 11) \<noteq> 0"
-nitpick [card nat = 4, expect = potential]
-nitpick [card nat = 14, expect = genuine]
+lemma "(SOME j. j > Suc 2 \<and> j \<le> 3) \<noteq> 0"
+nitpick [card nat = 2, expect = potential]
+nitpick [card nat = 6, expect = genuine]
oops

-lemma "(SOME j. j > Suc 10 \<and> j \<le> 12) = x \<Longrightarrow> x \<noteq> 0"
-nitpick [card nat = 4, expect = potential]
-nitpick [card nat = 14, expect = none]
+lemma "(SOME j. j > Suc 2 \<and> j \<le> 4) = x \<Longrightarrow> x \<noteq> 0"
+nitpick [card nat = 2, expect = potential]
+nitpick [card nat = 6, expect = none]
oops

-lemma "(SOME j. j > Suc 10 \<and> j \<le> 12) = x \<Longrightarrow> x = 12"
-nitpick [card nat = 4, expect = potential]
-nitpick [card nat = 14, expect = none]
+lemma "(SOME j. j > Suc 2 \<and> j \<le> 4) = x \<Longrightarrow> x = 4"
+nitpick [card nat = 2, expect = potential]
+nitpick [card nat = 6, expect = none]
sorry

-lemma "(SOME j. j > Suc 10 \<and> j \<le> 13) = x \<Longrightarrow> x = 12"
-nitpick [card nat = 14, expect = genuine]
+lemma "(SOME j. j > Suc 2 \<and> j \<le> 5) = x \<Longrightarrow> x = 4"
+nitpick [card nat = 6, expect = genuine]
oops

-lemma "(SOME j. j > Suc 10 \<and> j \<le> 13) = x \<Longrightarrow> x = 12 \<or> x = 13"
-nitpick [card nat = 14, expect = none]
+lemma "(SOME j. j > Suc 2 \<and> j \<le> 5) = x \<Longrightarrow> x = 4 \<or> x = 5"
+nitpick [card nat = 6, expect = none]
sorry

nitpick_params [fast_descrs, max_potential = 0]```
```--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Tue Jun 15 14:28:22 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Thu Jun 17 10:02:29 2010 +0200
@@ -136,7 +136,9 @@
in dec_sko (prop_of th) ([], thy) end

fun mk_skolem_id t =
-  let val T = fastype_of t in Const (@{const_name skolem_id}, T --> T) \$ t end
+  let val T = fastype_of t in
+    Const (@{const_name skolem_id}, T --> T) \$ Envir.beta_eta_contract t
+  end

(*Traverse a theorem, accumulating Skolem function definitions.*)
fun assume_skolem_funs inline s th =
@@ -407,7 +409,6 @@
val ctxt0 = Variable.global_thm_context th
val (nnfth, ctxt) = to_nnf th ctxt0
val inline = exists_type (exists_subtype (can dest_TFree)) (prop_of nnfth)
-      val inline = false (* FIXME: temporary *)
val defs = skolem_theorems_of_assume inline s nnfth
val (cnfs, ctxt) = Meson.make_cnf defs nnfth ctxt
in```
```--- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Tue Jun 15 14:28:22 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Thu Jun 17 10:02:29 2010 +0200
@@ -173,7 +173,7 @@
(skolem_somes, @{const_name undefined})
else case AList.find (op aconv) skolem_somes t of
s :: _ => (skolem_somes, s)
-              | _ =>
+              | [] =>
let
val s = skolem_theory_name ^ "." ^
skolem_name i (length skolem_somes)```