--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal-General/nominal_library.ML	Wed Apr 14 14:41:54 2010 +0200
@@ -0,0 +1,31 @@
+(*  Title:      nominal_library.ML
+    Author:     Christian Urban
+
+  Basic function for nominal.
+*)
+
+signature NOMINAL_LIBRARY =
+sig
+  val mk_minus: term -> term
+  val mk_perm: term -> term -> term
+end
+
+
+structure Nominal_Library: NOMINAL_LIBRARY =
+struct
+
+fun mk_minus p = 
+ Const (@{const_name "uminus"}, @{typ "perm => perm"}) $ p
+
+fun mk_perm p trm =
+let
+  val ty = fastype_of trm
+in
+  Const (@{const_name "permute"}, @{typ "perm"} --> ty --> ty) $ p $ trm
+end
+
+
+
+end (* structure *)
+
+open Nominal_Library;
\ No newline at end of file