tuned

--- a/src/HOL/Tools/Qelim/qelim.ML	Sun Jul 22 17:53:48 2007 +0200
+++ b/src/HOL/Tools/Qelim/qelim.ML	Sun Jul 22 17:53:50 2007 +0200
@@ -1,17 +1,16 @@
 (*  Title:      HOL/Tools/Qelim/qelim.ML
     ID:         $Id$
-    Author:     Amine Chaieb and Tobias Nipkow, TU Muenchen
+    Author:     Amine Chaieb, TU Muenchen
 
-Proof protocolling and proof generation for multiple quantified formulae.
+Generic quantifier elimination conversions for HOL formulae.
 *)
 
 signature QELIM =
 sig
- val gen_qelim_conv: conv -> conv -> conv ->
-   (cterm -> 'a -> 'a) -> 'a -> ('a -> cterm -> thm) ->
-   ('a -> conv) -> ('a -> cterm -> thm) -> conv
- val standard_qelim_conv: (cterm list -> cterm -> thm) ->
-   (cterm list -> conv) -> (cterm list -> cterm -> thm) -> cterm -> thm
+ val gen_qelim_conv: conv -> conv -> conv -> (cterm -> 'a -> 'a) -> 'a 
+                     -> ('a -> conv) -> ('a -> conv) -> ('a -> conv) -> conv
+ val standard_qelim_conv: (cterm list -> conv) -> (cterm list -> conv) 
+                          -> (cterm list -> conv) -> conv
 end;
 
 structure Qelim: QELIM =
@@ -19,18 +18,17 @@
 
 open Conv;
 
-
-(* gen_qelim_conv *)
-
 val all_not_ex = mk_meta_eq @{thm "all_not_ex"};
 
 fun gen_qelim_conv precv postcv simpex_conv ins env atcv ncv qcv =
  let
   fun conv env p =
    case (term_of p) of
-    Const(s,T)$_$_ => if domain_type T = HOLogic.boolT
-                         andalso s mem ["op &","op |","op -->","op ="]
-                     then binop_conv (conv env) p else atcv env p
+    Const(s,T)$_$_ => 
+       if domain_type T = HOLogic.boolT
+          andalso s mem ["op &","op |","op -->","op ="]
+       then binop_conv (conv env) p 
+       else atcv env p
   | Const("Not",_)$_ => arg_conv (conv env) p
   | Const("Ex",_)$Abs(s,_,_) =>
     let
@@ -54,14 +52,15 @@
   | _ => atcv env p
  in precv then_conv (conv env) then_conv postcv end
 
+(* Instantiation of some parameter for most common cases *)
 
-(* standard_qelim_conv *)
-
+local
 val pcv = Simplifier.rewrite
                  (HOL_basic_ss addsimps (simp_thms @ ex_simps @ all_simps)
                      @ [@{thm "all_not_ex"}, not_all, ex_disj_distrib]);
 
-fun standard_qelim_conv atcv ncv qcv p =
-  gen_qelim_conv pcv pcv pcv cons (Thm.add_cterm_frees p []) atcv ncv qcv p;
+in fun standard_qelim_conv atcv ncv qcv p =
+      gen_qelim_conv pcv pcv pcv cons (Thm.add_cterm_frees p []) atcv ncv qcv p
+end;
 
 end;