reactivated theory PER;
authorwenzelm
Sun, 01 Oct 2006 18:29:31 +0200
changeset 20812 cc6b31c2b9a2
parent 20811 eccbfaf2bc0e
child 20813 379ce56e5dc2
reactivated theory PER; removed obsolete StringEx;
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";