# HG changeset patch
# User wenzelm
# Date 963773373 -7200
# Node ID 4e7e0eb01a6c75a456287833e97267fbc414e765
# Parent  93cd32adc402f03fdb0f524501b9907aabb7fd58
added Tuple.thy;

diff -r 93cd32adc402 -r 4e7e0eb01a6c src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Sun Jul 16 20:49:13 2000 +0200
+++ b/src/HOL/ex/ROOT.ML	Sun Jul 16 20:49:33 2000 +0200
@@ -41,6 +41,7 @@
 time_use_thy "PiSets";
 time_use_thy "LocaleGroup";
 
-(*expressions with quote / antiquote syntax*)
+(*advanced concrete syntax*)
+time_use_thy "Tuple";
 time_use_thy "Antiquote";
 time_use_thy "Multiquote";