diff -r fd4fa6df22d1 -r a95a497e1f4f Nominal/Ex/SFT/Utils.thy --- a/Nominal/Ex/SFT/Utils.thy Fri Jun 24 11:15:22 2011 +0900 +++ b/Nominal/Ex/SFT/Utils.thy Fri Jun 24 11:18:18 2011 +0900 @@ -1,4 +1,5 @@ header {* Utilities for defining constants and functions *} + theory Utils imports Lambda begin lemma beta_app: