# HG changeset patch
# User berghofe
# Date 1034252627 -7200
# Node ID 993576f4de3007954957f5f5b9722850e6508d8a
# Parent  8ee6ea6627e11b808887f06d1abadfe5f1b66f13
Added list_all.

diff -r 8ee6ea6627e1 -r 993576f4de30 src/HOL/hologic.ML
--- a/src/HOL/hologic.ML	Thu Oct 10 14:23:19 2002 +0200
+++ b/src/HOL/hologic.ML	Thu Oct 10 14:23:47 2002 +0200
@@ -36,6 +36,7 @@
   val mk_eq: term * term -> term
   val dest_eq: term -> term * term
   val mk_all: string * typ * term -> term
+  val list_all: (string * typ) list * term -> term
   val mk_exists: string * typ * term -> term
   val mk_Collect: string * typ * term -> term
   val mk_mem: term * term -> term
@@ -139,6 +140,7 @@
 
 fun all_const T = Const ("All", [T --> boolT] ---> boolT);
 fun mk_all (x, T, P) = all_const T $ absfree (x, T, P);
+val list_all = foldr (fn ((x, T), P) => all_const T $ Abs (x, T, P));
 
 fun exists_const T = Const ("Ex", [T --> boolT] ---> boolT);
 fun mk_exists (x, T, P) = exists_const T $ absfree (x, T, P);