changeset 23144 | 4a9c9e260abf |
parent 23098 | 11e1a67fbfe8 |
child 23145 | 5d8faadf3ecf |
--- a/src/HOL/Nominal/Examples/ROOT.ML Thu May 31 09:48:20 2007 +0200 +++ b/src/HOL/Nominal/Examples/ROOT.ML Thu May 31 10:17:23 2007 +0200 @@ -15,4 +15,5 @@ use_thy "SN"; use_thy "Weakening"; use_thy "Crary"; -use_thy "SOS"; \ No newline at end of file +use_thy "SOS"; +use_thy "LocalWeakening.thy"; \ No newline at end of file