# HG changeset patch
# User bulwahn
# Date 1349858935 -7200
# Node ID 3ecfba7e731dd64067707dee0a1aa823c9e981a3
# Parent  2a1dcc962005687a17132f154f54b4cf62cfba17
adding necessary syntactic functions in set_comprehension_pointfree simproc as a first step to integrate an improved simproc

diff -r 2a1dcc962005 -r 3ecfba7e731d src/HOL/Tools/set_comprehension_pointfree.ML
--- a/src/HOL/Tools/set_comprehension_pointfree.ML	Wed Oct 10 10:48:33 2012 +0200
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Wed Oct 10 10:48:55 2012 +0200
@@ -26,6 +26,20 @@
     Const (@{const_name Lattices.inf_class.inf}, T --> T --> T) $ t1 $ t2
   end
 
+fun mk_sup (t1, t2) =
+  let
+    val T = fastype_of t1
+  in
+    Const (@{const_name Lattices.sup_class.sup}, T --> T --> T) $ t1 $ t2
+  end
+
+fun mk_Compl t =
+  let
+    val T = fastype_of t
+  in
+    Const (@{const_name "Groups.uminus_class.uminus"}, T --> T) $ t
+  end
+
 fun mk_image t1 t2 =
   let
     val T as Type (@{type_name fun}, [_ , R]) = fastype_of t1