# 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";