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