src/HOL/Isar_examples/ROOT.ML
changeset 8675 a2ff2301d65e
parent 8137 fb6fe34060ca
child 8782 86b6b6e712ee
--- a/src/HOL/Isar_examples/ROOT.ML	Wed Apr 05 21:06:37 2000 +0200
+++ b/src/HOL/Isar_examples/ROOT.ML	Wed Apr 05 21:06:52 2000 +0200
@@ -17,3 +17,4 @@
 with_path "../W0" time_use_thy "W_correct";
 with_path "../ex" time_use_thy "Fibonacci";
 time_use_thy "Puzzle";
+time_use_thy "NestedDatatype";