Added Compile and Height examples.
authorberghofe
Mon, 23 Oct 2006 00:48:45 +0200
changeset 21086 fe9f43a1e5bd
parent 21085 3cb13b06ad72
child 21087 3e56528a39f7
Added Compile and Height examples.
src/HOL/Nominal/Examples/ROOT.ML
--- 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";