--- a/src/HOL/Enum.thy Sun Dec 16 18:44:27 2012 +0100
+++ b/src/HOL/Enum.thy Sun Dec 16 19:13:19 2012 +0100
@@ -60,6 +60,10 @@
"Collect P = set (filter P enum)"
by (simp add: enum_UNIV)
+lemma vimage_code [code]:
+ "f -` B = set (filter (%x. f x : B) enum_class.enum)"
+ unfolding vimage_def Collect_code ..
+
definition card_UNIV :: "'a itself \<Rightarrow> nat"
where
[code del]: "card_UNIV TYPE('a) = card (UNIV :: 'a set)"
--- a/src/HOL/ROOT Sun Dec 16 18:44:27 2012 +0100
+++ b/src/HOL/ROOT Sun Dec 16 19:13:19 2012 +0100
@@ -804,8 +804,8 @@
Quickcheck_Narrowing_Examples
session "HOL-Quickcheck_Benchmark" in Quickcheck_Benchmark = HOL +
- theories [condition = ISABELLE_FULL_TEST, quick_and_dirty]
- (* Find_Unused_Assms_Examples FIXME *)
+ theories [condition = ISABELLE_FULL_TEST, timeout = 5400, quick_and_dirty]
+ Find_Unused_Assms_Examples
Needham_Schroeder_No_Attacker_Example
Needham_Schroeder_Guided_Attacker_Example
Needham_Schroeder_Unguided_Attacker_Example