# HG changeset patch
# User wenzelm
# Date 1159720171 -7200
# Node ID cc6b31c2b9a289d159a8d3ddd32e836ecf6d9b13
# Parent  eccbfaf2bc0ed8e77a066f34ac76fb64095e4d18
reactivated theory PER;
removed obsolete StringEx;

diff -r eccbfaf2bc0e -r cc6b31c2b9a2 src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Sun Oct 01 18:29:30 2006 +0200
+++ b/src/HOL/ex/ROOT.ML	Sun Oct 01 18:29:31 2006 +0200
@@ -20,12 +20,12 @@
 time_use_thy "Locales";
 time_use_thy "Records";
 time_use_thy "MonoidGroup";
-time_use_thy "StringEx";
 time_use_thy "BinEx";
 setmp proofs 2 time_use_thy "Hilbert_Classical";
 time_use_thy "Antiquote";
 time_use_thy "Multiquote";
 
+time_use_thy "PER";
 time_use_thy "NatSum";
 time_use_thy "ThreeDivides";
 time_use_thy "Intuitionistic";