# HG changeset patch
# User nipkow
# Date 1118057405 -7200
# Node ID 928e95c867d631e947ea2e98d5cc16fbe26fa832
# Parent  f05c81817ec686822009f42e4ebfac438be73d10
update -> use

diff -r f05c81817ec6 -r 928e95c867d6 src/HOL/Bali/ROOT.ML
--- a/src/HOL/Bali/ROOT.ML	Mon Jun 06 12:17:59 2005 +0200
+++ b/src/HOL/Bali/ROOT.ML	Mon Jun 06 13:30:05 2005 +0200
@@ -6,7 +6,7 @@
 The Hoare logic for Bali
 *)
 
-update_thy "AxExample";
-update_thy "AxSound";
-update_thy "AxCompl";
-update_thy "Trans";
+use_thy "AxExample";
+use_thy "AxSound";
+use_thy "AxCompl";
+use_thy "Trans";