# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1310767277 -7200
# Node ID 16f2fd9103bda139690439a1d04039dd254a25aa
# Parent  f035d867fb41f54c175eab20bc3a27b355d0d25f
HOL/Import: Fix errors with _mk_list

diff -r f035d867fb41 -r 16f2fd9103bd src/HOL/Import/Generate-HOLLight/GenHOLLight.thy
--- a/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Fri Jul 15 16:51:01 2011 +0200
+++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Sat Jul 16 00:01:17 2011 +0200
@@ -30,15 +30,18 @@
 
   (* list_of_set uses Isabelle lists with HOLLight CARD *)
   DEF_list_of_set LIST_OF_SET_PROPERTIES SET_OF_LIST_OF_SET LENGTH_LIST_OF_SET
-  MEM_LIST_OF_SET FINITE_SET_OF_LIST
+  MEM_LIST_OF_SET HAS_SIZE_SET_OF_LIST FINITE_SET_OF_LIST
   (* UNIV *)
-  DIMINDEX_FINITE_SUM  DIMINDEX_HAS_SIZE_FINITE_SUM
-  FSTCART_PASTECART SNDCART_PASTECART PASTECART_FST_SND PASTECART_EQ FORALL_PASTECART EXISTS_PASTECART
+  DIMINDEX_FINITE_SUM  DIMINDEX_HAS_SIZE_FINITE_SUM FSTCART_PASTECART
+  SNDCART_PASTECART PASTECART_FST_SND PASTECART_EQ FORALL_PASTECART EXISTS_PASTECART
   (* Reals *)
   (* TYDEF_real DEF_real_of_num DEF_real_neg DEF_real_add DEF_real_mul DEF_real_le
   DEF_real_inv REAL_HREAL_LEMMA1 REAL_HREAL_LEMMA2 *)
   (* Integers *)
   (* TYDEF_int DEF_int_divides DEF_int_coprime*)
+  (* HOLLight CARD and CASEWISE with Isabelle lists *)
+  CARD_SET_OF_LIST_LE CASEWISE CASEWISE_CASES RECURSION_CASEWISE CASEWISE_WORKS
+  WF_REC_CASES RECURSION_CASEWISE_PAIRWISE
 
 ;type_maps
   bool > HOL.bool
diff -r f035d867fb41 -r 16f2fd9103bd src/HOL/Import/HOLLight/HOLLight.thy
--- a/src/HOL/Import/HOLLight/HOLLight.thy	Fri Jul 15 16:51:01 2011 +0200
+++ b/src/HOL/Import/HOLLight/HOLLight.thy	Sat Jul 16 00:01:17 2011 +0200
@@ -3857,9 +3857,6 @@
 lemma EQ_UNIV: "(ALL x::'A. x : (s::'A => bool)) = (s = UNIV)"
   by (import hollight EQ_UNIV)
 
-lemma UNIV_SUBSET: "(UNIV <= (x::'A => bool)) = (x = UNIV)"
-  by (import hollight UNIV_SUBSET)
-
 lemma SING_SUBSET: "({xa::'q_44493} <= (x::'q_44493 => bool)) = (xa : x)"
   by (import hollight SING_SUBSET)
 
@@ -5205,25 +5202,25 @@
   by (import hollight FINITE_SUPPORT)
 
 lemma SUPPORT_CLAUSES: "(ALL x::'q_60297 => 'q_60530.
-    support (u_4372::'q_60530 => 'q_60530 => 'q_60530) x {} = {}) &
+    support (u_4371::'q_60530 => 'q_60530 => 'q_60530) x {} = {}) &
 (ALL (x::'q_60345 => 'q_60530) (xa::'q_60345) xb::'q_60345 => bool.
-    support u_4372 x (insert xa xb) =
-    (if x xa = neutral u_4372 then support u_4372 x xb
-     else insert xa (support u_4372 x xb))) &
+    support u_4371 x (insert xa xb) =
+    (if x xa = neutral u_4371 then support u_4371 x xb
+     else insert xa (support u_4371 x xb))) &
 (ALL (x::'q_60378 => 'q_60530) (xa::'q_60378) xb::'q_60378 => bool.
-    support u_4372 x (xb - {xa}) = support u_4372 x xb - {xa}) &
+    support u_4371 x (xb - {xa}) = support u_4371 x xb - {xa}) &
 (ALL (x::'q_60416 => 'q_60530) (xa::'q_60416 => bool) xb::'q_60416 => bool.
-    support u_4372 x (xa Un xb) =
-    support u_4372 x xa Un support u_4372 x xb) &
+    support u_4371 x (xa Un xb) =
+    support u_4371 x xa Un support u_4371 x xb) &
 (ALL (x::'q_60454 => 'q_60530) (xa::'q_60454 => bool) xb::'q_60454 => bool.
-    support u_4372 x (xa Int xb) =
-    support u_4372 x xa Int support u_4372 x xb) &
+    support u_4371 x (xa Int xb) =
+    support u_4371 x xa Int support u_4371 x xb) &
 (ALL (x::'q_60492 => 'q_60530) (xa::'q_60492 => bool) xb::'q_60492 => bool.
-    support u_4372 x (xa - xb) =
-    support u_4372 x xa - support u_4372 x xb) &
+    support u_4371 x (xa - xb) =
+    support u_4371 x xa - support u_4371 x xb) &
 (ALL (x::'q_60529 => 'q_60520) (xa::'q_60520 => 'q_60530)
     xb::'q_60529 => bool.
-    support u_4372 xa (x ` xb) = x ` support u_4372 (xa o x) xb)"
+    support u_4371 xa (x ` xb) = x ` support u_4371 (xa o x) xb)"
   by (import hollight SUPPORT_CLAUSES)
 
 lemma SUPPORT_DELTA: "support (x::'q_60556 => 'q_60556 => 'q_60556)
@@ -5253,13 +5250,13 @@
  else neutral x)"
   by (import hollight ITERATE_EXPAND_CASES)
 
-lemma ITERATE_CLAUSES_GEN: "monoidal (u_4372::'B => 'B => 'B)
-==> (ALL f::'A => 'B. iterate u_4372 {} f = neutral u_4372) &
+lemma ITERATE_CLAUSES_GEN: "monoidal (u_4371::'B => 'B => 'B)
+==> (ALL f::'A => 'B. iterate u_4371 {} f = neutral u_4371) &
     (ALL (f::'A => 'B) (x::'A) s::'A => bool.
-        monoidal u_4372 & finite (support u_4372 f s) -->
-        iterate u_4372 (insert x s) f =
-        (if x : s then iterate u_4372 s f
-         else u_4372 (f x) (iterate u_4372 s f)))"
+        monoidal u_4371 & finite (support u_4371 f s) -->
+        iterate u_4371 (insert x s) f =
+        (if x : s then iterate u_4371 s f
+         else u_4371 (f x) (iterate u_4371 s f)))"
   by (import hollight ITERATE_CLAUSES_GEN)
 
 lemma ITERATE_CLAUSES: "monoidal (x::'q_60857 => 'q_60857 => 'q_60857)
@@ -5270,11 +5267,11 @@
         (if xa : s then iterate x s f else x (f xa) (iterate x s f)))"
   by (import hollight ITERATE_CLAUSES)
 
-lemma ITERATE_UNION: "[| monoidal (u_4372::'q_60945 => 'q_60945 => 'q_60945);
+lemma ITERATE_UNION: "[| monoidal (u_4371::'q_60945 => 'q_60945 => 'q_60945);
    finite (s::'q_60930 => bool) &
    finite (x::'q_60930 => bool) & s Int x = {} |]
-==> iterate u_4372 (s Un x) (f::'q_60930 => 'q_60945) =
-    u_4372 (iterate u_4372 s f) (iterate u_4372 x f)"
+==> iterate u_4371 (s Un x) (f::'q_60930 => 'q_60945) =
+    u_4371 (iterate u_4371 s f) (iterate u_4371 x f)"
   by (import hollight ITERATE_UNION)
 
 lemma ITERATE_UNION_GEN: "[| monoidal (x::'B => 'B => 'B);
@@ -5296,33 +5293,33 @@
 ==> x (iterate x (xb - xc) xa) (iterate x xc xa) = iterate x xb xa"
   by (import hollight ITERATE_DIFF_GEN)
 
-lemma ITERATE_INCL_EXCL: "[| monoidal (u_4372::'q_61316 => 'q_61316 => 'q_61316);
+lemma ITERATE_INCL_EXCL: "[| monoidal (u_4371::'q_61316 => 'q_61316 => 'q_61316);
    finite (s::'q_61298 => bool) & finite (t::'q_61298 => bool) |]
-==> u_4372 (iterate u_4372 s (f::'q_61298 => 'q_61316))
-     (iterate u_4372 t f) =
-    u_4372 (iterate u_4372 (s Un t) f) (iterate u_4372 (s Int t) f)"
+==> u_4371 (iterate u_4371 s (f::'q_61298 => 'q_61316))
+     (iterate u_4371 t f) =
+    u_4371 (iterate u_4371 (s Un t) f) (iterate u_4371 (s Int t) f)"
   by (import hollight ITERATE_INCL_EXCL)
 
-lemma ITERATE_CLOSED: "[| monoidal (u_4372::'B => 'B => 'B);
-   (P::'B => bool) (neutral u_4372) &
-   (ALL (x::'B) y::'B. P x & P y --> P (u_4372 x y));
+lemma ITERATE_CLOSED: "[| monoidal (u_4371::'B => 'B => 'B);
+   (P::'B => bool) (neutral u_4371) &
+   (ALL (x::'B) y::'B. P x & P y --> P (u_4371 x y));
    !!x::'A.
-      x : (s::'A => bool) & (f::'A => 'B) x ~= neutral u_4372 ==> P (f x) |]
-==> P (iterate u_4372 s f)"
+      x : (s::'A => bool) & (f::'A => 'B) x ~= neutral u_4371 ==> P (f x) |]
+==> P (iterate u_4371 s f)"
   by (import hollight ITERATE_CLOSED)
 
-lemma ITERATE_RELATED: "[| monoidal (u_4372::'B => 'B => 'B);
-   (R::'B => 'B => bool) (neutral u_4372) (neutral u_4372) &
+lemma ITERATE_RELATED: "[| monoidal (u_4371::'B => 'B => 'B);
+   (R::'B => 'B => bool) (neutral u_4371) (neutral u_4371) &
    (ALL (x1::'B) (y1::'B) (x2::'B) y2::'B.
-       R x1 x2 & R y1 y2 --> R (u_4372 x1 y1) (u_4372 x2 y2));
+       R x1 x2 & R y1 y2 --> R (u_4371 x1 y1) (u_4371 x2 y2));
    finite (x::'A => bool) &
    (ALL xa::'A. xa : x --> R ((f::'A => 'B) xa) ((g::'A => 'B) xa)) |]
-==> R (iterate u_4372 x f) (iterate u_4372 x g)"
+==> R (iterate u_4371 x f) (iterate u_4371 x g)"
   by (import hollight ITERATE_RELATED)
 
-lemma ITERATE_EQ_NEUTRAL: "[| monoidal (u_4372::'B => 'B => 'B);
-   !!x::'A. x : (s::'A => bool) ==> (f::'A => 'B) x = neutral u_4372 |]
-==> iterate u_4372 s f = neutral u_4372"
+lemma ITERATE_EQ_NEUTRAL: "[| monoidal (u_4371::'B => 'B => 'B);
+   !!x::'A. x : (s::'A => bool) ==> (f::'A => 'B) x = neutral u_4371 |]
+==> iterate u_4371 s f = neutral u_4371"
   by (import hollight ITERATE_EQ_NEUTRAL)
 
 lemma ITERATE_SING: "monoidal (x::'B => 'B => 'B) ==> iterate x {xa::'A} (f::'A => 'B) = f xa"
@@ -5332,110 +5329,110 @@
 ==> u ((f::'A => 'B) a) (iterate u (s - {a}) f) = iterate u s f"
   by (import hollight ITERATE_DELETE)
 
-lemma ITERATE_DELTA: "monoidal (u_4372::'q_61672 => 'q_61672 => 'q_61672)
-==> iterate u_4372 (xb::'q_61691 => bool)
+lemma ITERATE_DELTA: "monoidal (u_4371::'q_61672 => 'q_61672 => 'q_61672)
+==> iterate u_4371 (xb::'q_61691 => bool)
      (%xb::'q_61691.
          if xb = (xa::'q_61691) then (x::'q_61691 => 'q_61672) xb
-         else neutral u_4372) =
-    (if xa : xb then x xa else neutral u_4372)"
+         else neutral u_4371) =
+    (if xa : xb then x xa else neutral u_4371)"
   by (import hollight ITERATE_DELTA)
 
-lemma ITERATE_IMAGE: "[| monoidal (u_4372::'C => 'C => 'C);
+lemma ITERATE_IMAGE: "[| monoidal (u_4371::'C => 'C => 'C);
    !!(x::'A) y::'A.
       x : (s::'A => bool) & y : s & (f::'A => 'B) x = f y ==> x = y |]
-==> iterate u_4372 (f ` s) (g::'B => 'C) = iterate u_4372 s (g o f)"
+==> iterate u_4371 (f ` s) (g::'B => 'C) = iterate u_4371 s (g o f)"
   by (import hollight ITERATE_IMAGE)
 
-lemma ITERATE_BIJECTION: "[| monoidal (u_4372::'B => 'B => 'B);
+lemma ITERATE_BIJECTION: "[| monoidal (u_4371::'B => 'B => 'B);
    (ALL x::'A. x : (s::'A => bool) --> (p::'A => 'A) x : s) &
    (ALL y::'A. y : s --> (EX! x::'A. x : s & p x = y)) |]
-==> iterate u_4372 s (f::'A => 'B) = iterate u_4372 s (f o p)"
+==> iterate u_4371 s (f::'A => 'B) = iterate u_4371 s (f o p)"
   by (import hollight ITERATE_BIJECTION)
 
-lemma ITERATE_ITERATE_PRODUCT: "[| monoidal (u_4372::'C => 'C => 'C);
+lemma ITERATE_ITERATE_PRODUCT: "[| monoidal (u_4371::'C => 'C => 'C);
    finite (x::'A => bool) &
    (ALL i::'A. i : x --> finite ((xa::'A => 'B => bool) i)) |]
-==> iterate u_4372 x
-     (%i::'A. iterate u_4372 (xa i) ((xb::'A => 'B => 'C) i)) =
-    iterate u_4372
+==> iterate u_4371 x
+     (%i::'A. iterate u_4371 (xa i) ((xb::'A => 'B => 'C) i)) =
+    iterate u_4371
      {u::'A * 'B. EX (i::'A) j::'B. (i : x & j : xa i) & u = (i, j)}
      (SOME f::'A * 'B => 'C. ALL (i::'A) j::'B. f (i, j) = xb i j)"
   by (import hollight ITERATE_ITERATE_PRODUCT)
 
-lemma ITERATE_EQ: "[| monoidal (u_4372::'B => 'B => 'B);
+lemma ITERATE_EQ: "[| monoidal (u_4371::'B => 'B => 'B);
    !!x::'A. x : (s::'A => bool) ==> (f::'A => 'B) x = (g::'A => 'B) x |]
-==> iterate u_4372 s f = iterate u_4372 s g"
+==> iterate u_4371 s f = iterate u_4371 s g"
   by (import hollight ITERATE_EQ)
 
-lemma ITERATE_EQ_GENERAL: "[| monoidal (u_4372::'C => 'C => 'C);
+lemma ITERATE_EQ_GENERAL: "[| monoidal (u_4371::'C => 'C => 'C);
    (ALL y::'B.
        y : (t::'B => bool) -->
        (EX! x::'A. x : (s::'A => bool) & (h::'A => 'B) x = y)) &
    (ALL x::'A. x : s --> h x : t & (g::'B => 'C) (h x) = (f::'A => 'C) x) |]
-==> iterate u_4372 s f = iterate u_4372 t g"
+==> iterate u_4371 s f = iterate u_4371 t g"
   by (import hollight ITERATE_EQ_GENERAL)
 
-lemma ITERATE_EQ_GENERAL_INVERSES: "[| monoidal (u_4372::'C => 'C => 'C);
+lemma ITERATE_EQ_GENERAL_INVERSES: "[| monoidal (u_4371::'C => 'C => 'C);
    (ALL y::'B.
        y : (t::'B => bool) -->
        (k::'B => 'A) y : (s::'A => bool) & (h::'A => 'B) (k y) = y) &
    (ALL x::'A.
        x : s -->
        h x : t & k (h x) = x & (g::'B => 'C) (h x) = (f::'A => 'C) x) |]
-==> iterate u_4372 s f = iterate u_4372 t g"
+==> iterate u_4371 s f = iterate u_4371 t g"
   by (import hollight ITERATE_EQ_GENERAL_INVERSES)
 
-lemma ITERATE_INJECTION: "[| monoidal (u_4372::'B => 'B => 'B);
+lemma ITERATE_INJECTION: "[| monoidal (u_4371::'B => 'B => 'B);
    finite (s::'A => bool) &
    (ALL x::'A. x : s --> (p::'A => 'A) x : s) &
    (ALL (x::'A) y::'A. x : s & y : s & p x = p y --> x = y) |]
-==> iterate u_4372 s ((f::'A => 'B) o p) = iterate u_4372 s f"
+==> iterate u_4371 s ((f::'A => 'B) o p) = iterate u_4371 s f"
   by (import hollight ITERATE_INJECTION)
 
-lemma ITERATE_UNION_NONZERO: "[| monoidal (u_4372::'B => 'B => 'B);
+lemma ITERATE_UNION_NONZERO: "[| monoidal (u_4371::'B => 'B => 'B);
    finite (s::'A => bool) &
    finite (t::'A => bool) &
-   (ALL x::'A. x : s Int t --> (f::'A => 'B) x = neutral u_4372) |]
-==> iterate u_4372 (s Un t) f =
-    u_4372 (iterate u_4372 s f) (iterate u_4372 t f)"
+   (ALL x::'A. x : s Int t --> (f::'A => 'B) x = neutral u_4371) |]
+==> iterate u_4371 (s Un t) f =
+    u_4371 (iterate u_4371 s f) (iterate u_4371 t f)"
   by (import hollight ITERATE_UNION_NONZERO)
 
-lemma ITERATE_OP: "[| monoidal (u_4372::'q_62649 => 'q_62649 => 'q_62649);
+lemma ITERATE_OP: "[| monoidal (u_4371::'q_62649 => 'q_62649 => 'q_62649);
    finite (s::'q_62648 => bool) |]
-==> iterate u_4372 s
+==> iterate u_4371 s
      (%x::'q_62648.
-         u_4372 ((f::'q_62648 => 'q_62649) x)
+         u_4371 ((f::'q_62648 => 'q_62649) x)
           ((g::'q_62648 => 'q_62649) x)) =
-    u_4372 (iterate u_4372 s f) (iterate u_4372 s g)"
+    u_4371 (iterate u_4371 s f) (iterate u_4371 s g)"
   by (import hollight ITERATE_OP)
 
-lemma ITERATE_SUPERSET: "[| monoidal (u_4372::'B => 'B => 'B);
+lemma ITERATE_SUPERSET: "[| monoidal (u_4371::'B => 'B => 'B);
    (u::'A => bool) <= (v::'A => bool) &
-   (ALL x::'A. x : v & x ~: u --> (f::'A => 'B) x = neutral u_4372) |]
-==> iterate u_4372 v f = iterate u_4372 u f"
+   (ALL x::'A. x : v & x ~: u --> (f::'A => 'B) x = neutral u_4371) |]
+==> iterate u_4371 v f = iterate u_4371 u f"
   by (import hollight ITERATE_SUPERSET)
 
-lemma ITERATE_IMAGE_NONZERO: "[| monoidal (u_4372::'C => 'C => 'C);
+lemma ITERATE_IMAGE_NONZERO: "[| monoidal (u_4371::'C => 'C => 'C);
    finite (x::'A => bool) &
    (ALL (xa::'A) y::'A.
        xa : x & y : x & xa ~= y & (f::'A => 'B) xa = f y -->
-       (g::'B => 'C) (f xa) = neutral u_4372) |]
-==> iterate u_4372 (f ` x) g = iterate u_4372 x (g o f)"
+       (g::'B => 'C) (f xa) = neutral u_4371) |]
+==> iterate u_4371 (f ` x) g = iterate u_4371 x (g o f)"
   by (import hollight ITERATE_IMAGE_NONZERO)
 
-lemma ITERATE_CASES: "[| monoidal (u_4372::'B => 'B => 'B); finite (s::'A => bool) |]
-==> iterate u_4372 s
+lemma ITERATE_CASES: "[| monoidal (u_4371::'B => 'B => 'B); finite (s::'A => bool) |]
+==> iterate u_4371 s
      (%x::'A.
          if (P::'A => bool) x then (f::'A => 'B) x else (g::'A => 'B) x) =
-    u_4372 (iterate u_4372 {u::'A. EX x::'A. (x : s & P x) & u = x} f)
-     (iterate u_4372 {u::'A. EX x::'A. (x : s & ~ P x) & u = x} g)"
+    u_4371 (iterate u_4371 {u::'A. EX x::'A. (x : s & P x) & u = x} f)
+     (iterate u_4371 {u::'A. EX x::'A. (x : s & ~ P x) & u = x} g)"
   by (import hollight ITERATE_CASES)
 
-lemma ITERATE_OP_GEN: "[| monoidal (u_4372::'B => 'B => 'B);
-   finite (support u_4372 (f::'A => 'B) (s::'A => bool)) &
-   finite (support u_4372 (g::'A => 'B) s) |]
-==> iterate u_4372 s (%x::'A. u_4372 (f x) (g x)) =
-    u_4372 (iterate u_4372 s f) (iterate u_4372 s g)"
+lemma ITERATE_OP_GEN: "[| monoidal (u_4371::'B => 'B => 'B);
+   finite (support u_4371 (f::'A => 'B) (s::'A => bool)) &
+   finite (support u_4371 (g::'A => 'B) s) |]
+==> iterate u_4371 s (%x::'A. u_4371 (f x) (g x)) =
+    u_4371 (iterate u_4371 s f) (iterate u_4371 s g)"
   by (import hollight ITERATE_OP_GEN)
 
 lemma ITERATE_CLAUSES_NUMSEG: "monoidal (x::'q_63246 => 'q_63246 => 'q_63246)
@@ -5448,11 +5445,11 @@
          else iterate x {xa..xb} f))"
   by (import hollight ITERATE_CLAUSES_NUMSEG)
 
-lemma ITERATE_PAIR: "monoidal (u_4372::'q_63421 => 'q_63421 => 'q_63421)
-==> iterate u_4372 {(2::nat) * (m::nat)..(2::nat) * (n::nat) + (1::nat)}
+lemma ITERATE_PAIR: "monoidal (u_4371::'q_63421 => 'q_63421 => 'q_63421)
+==> iterate u_4371 {(2::nat) * (m::nat)..(2::nat) * (n::nat) + (1::nat)}
      (f::nat => 'q_63421) =
-    iterate u_4372 {m..n}
-     (%i::nat. u_4372 (f ((2::nat) * i)) (f ((2::nat) * i + (1::nat))))"
+    iterate u_4371 {m..n}
+     (%i::nat. u_4371 (f ((2::nat) * i)) (f ((2::nat) * i + (1::nat))))"
   by (import hollight ITERATE_PAIR)
 
 definition
diff -r f035d867fb41 -r 16f2fd9103bd src/HOL/Import/HOLLight/hollight.imp
--- a/src/HOL/Import/HOLLight/hollight.imp	Fri Jul 15 16:51:01 2011 +0200
+++ b/src/HOL/Import/HOLLight/hollight.imp	Sat Jul 16 00:01:17 2011 +0200
@@ -572,7 +572,7 @@
   "WF_DCHAIN" > "HOLLight.hollight.WF_DCHAIN"
   "UNWIND_THM2" > "HOL.simp_thms_39"
   "UNWIND_THM1" > "HOL.simp_thms_40"
-  "UNIV_SUBSET" > "HOLLight.hollight.UNIV_SUBSET"
+  "UNIV_SUBSET" > "Orderings.top_class.top_unique"
   "UNIV_NOT_EMPTY" > "Set.UNIV_not_empty"
   "UNIQUE_SKOLEM_THM" > "HOL.choice_eq"
   "UNIQUE_SKOLEM_ALT" > "HOLLight.hollight.UNIQUE_SKOLEM_ALT"
@@ -791,7 +791,7 @@
   "SUBSET_INSERT_DELETE" > "HOLLight.hollight.SUBSET_INSERT_DELETE"
   "SUBSET_INSERT" > "Set.subset_insert"
   "SUBSET_IMAGE" > "Set.subset_image_iff"
-  "SUBSET_EMPTY" > "Set.subset_empty"
+  "SUBSET_EMPTY" > "Orderings.bot_class.bot_unique"
   "SUBSET_DIFF" > "Set.Diff_subset"
   "SUBSET_DELETE" > "HOLLight.hollight.SUBSET_DELETE"
   "SUBSET_CARD_EQ" > "HOLLight.hollight.SUBSET_CARD_EQ"
@@ -1547,6 +1547,7 @@
   "IN_UNION" > "Complete_Lattice.mem_simps_3"
   "IN_SUPPORT" > "HOLLight.hollight.IN_SUPPORT"
   "IN_SING" > "Set.singleton_iff"
+  "IN_SET_OF_LIST" > "HOLLightList.IN_SET_OF_LIST"
   "IN_REST" > "HOLLight.hollight.IN_REST"
   "IN_NUMSEG_0" > "HOLLight.hollight.IN_NUMSEG_0"
   "IN_NUMSEG" > "SetInterval.ord_class.atLeastAtMost_iff"
@@ -2278,6 +2279,7 @@
   "$_def" > "HOLLight.hollight.$_def"
 
 ignore_thms
+  "WF_REC_CASES"
   "TYDEF_sum"
   "TYDEF_prod"
   "TYDEF_option"
@@ -2287,12 +2289,15 @@
   "SNDCART_PASTECART"
   "SET_OF_LIST_OF_SET"
   "REP_ABS_PAIR"
+  "RECURSION_CASEWISE_PAIRWISE"
+  "RECURSION_CASEWISE"
   "PASTECART_FST_SND"
   "PASTECART_EQ"
   "MEM_LIST_OF_SET"
   "MEM_ASSOC"
   "LIST_OF_SET_PROPERTIES"
   "LENGTH_LIST_OF_SET"
+  "HAS_SIZE_SET_OF_LIST"
   "FSTCART_PASTECART"
   "FORALL_PASTECART"
   "FINITE_SET_OF_LIST"
@@ -2321,6 +2326,10 @@
   "DEF_CONS"
   "DEF_ASSOC"
   "DEF_,"
+  "CASEWISE_WORKS"
+  "CASEWISE_CASES"
+  "CASEWISE"
+  "CARD_SET_OF_LIST_LE"
   "ALL_MAP"
 
 end
diff -r f035d867fb41 -r 16f2fd9103bd src/HOL/Import/HOLLightList.thy
--- a/src/HOL/Import/HOLLightList.thy	Fri Jul 15 16:51:01 2011 +0200
+++ b/src/HOL/Import/HOLLightList.thy	Sat Jul 16 00:01:17 2011 +0200
@@ -8,6 +8,10 @@
 imports List
 begin
 
+lemma FINITE_SET_OF_LIST:
+  "finite (set l)"
+  by simp
+
 lemma AND_ALL2:
   "(list_all2 P l m \<and> list_all2 Q l m) = list_all2 (\<lambda>x y. P x y \<and> Q x y) l m"
   by (induct l m rule: list_induct2') auto
@@ -298,8 +302,8 @@
   done
 
 lemma IN_SET_OF_LIST:
-  "ALL x l. (x\<in>set l) = list_mem x l"
-  by (simp add: member_def)
+  "(x : set l) = (x : set l)"
+  by simp
 
 lemma DEF_BUTLAST:
   "butlast = (SOME B. B [] = [] \<and> (\<forall>h t. B (h # t) = (if t = [] then [] else h # B t)))"