Nominal-General/nominal_library.ML
changeset 2398 1e6160690546
parent 2397 c670a849af65
child 2399 107c06267f33
--- a/Nominal-General/nominal_library.ML	Sat Aug 14 16:54:41 2010 +0800
+++ b/Nominal-General/nominal_library.ML	Sat Aug 14 23:33:23 2010 +0800
@@ -58,6 +58,7 @@
 
   (* transformation into the object logic *)
   val atomize: thm -> thm
+
 end
 
 
@@ -262,7 +263,6 @@
 (* transformes a theorem into one of the object logic *)
 val atomize = Conv.fconv_rule Object_Logic.atomize o forall_intr_vars
 
-
 end (* structure *)
 
 open Nominal_Library;
\ No newline at end of file