author | berghofe |
Mon, 23 Oct 2006 00:48:45 +0200 | |
changeset 21086 | fe9f43a1e5bd |
parent 21085 | 3cb13b06ad72 |
child 21087 | 3e56528a39f7 |
--- a/src/HOL/Nominal/Examples/ROOT.ML Mon Oct 23 00:47:25 2006 +0200 +++ b/src/HOL/Nominal/Examples/ROOT.ML Mon Oct 23 00:48:45 2006 +0200 @@ -7,7 +7,9 @@ use_thy "CR"; use_thy "Class"; -setmp quick_and_dirty true use_thy "Fsub"; (* FIXME *) +use_thy "Compile"; +use_thy "Fsub"; +use_thy "Height"; use_thy "Lambda_mu"; use_thy "Recursion"; use_thy "SN";