--- a/src/HOL/ex/ROOT.ML Fri Oct 23 19:40:00 1998 +0200
+++ b/src/HOL/ex/ROOT.ML Fri Oct 23 20:28:33 1998 +0200
@@ -11,7 +11,7 @@
writeln "Root file for HOL examples";
set proof_timing;
-(**Some examples of recursive function definitions: the TFL package**)
+(*some examples of recursive function definitions: the TFL package*)
time_use_thy "Recdefs";
time_use_thy "Primes";
time_use_thy "Fib";
@@ -35,14 +35,15 @@
time_use_thy "StringEx";
time_use_thy "BinEx";
-(*Monoids and Groups as predicates over record schemes*)
+(*basic use of extensible records*)
time_use_thy "MonoidGroup";
+time_use_thy "Points";
-(*Groups via locales*)
+(*groups via locales*)
time_use_thy "PiSets";
time_use_thy "LocaleGroup";
-(*Expressions with quote / antiquote*)
+(*expressions with quote / antiquote syntax*)
time_use_thy "Antiquote";