# HG changeset patch
# User nipkow
# Date 1369979709 -7200
# Node ID d867812da48b10b88db52d0ffc67f43bcd6e58d3
# Parent  b28695e5a018c3deb7492bd38ed3d652c2a78501
more VC -> VCG

diff -r b28695e5a018 -r d867812da48b src/HOL/IMP/VCG.thy
--- a/src/HOL/IMP/VCG.thy	Fri May 31 07:26:31 2013 +0200
+++ b/src/HOL/IMP/VCG.thy	Fri May 31 07:55:09 2013 +0200
@@ -1,6 +1,6 @@
 (* Author: Tobias Nipkow *)
 
-theory VC imports Hoare begin
+theory VCG imports Hoare begin
 
 subsection "Verification Conditions"
 
diff -r b28695e5a018 -r d867812da48b src/HOL/ROOT
--- a/src/HOL/ROOT	Fri May 31 07:26:31 2013 +0200
+++ b/src/HOL/ROOT	Fri May 31 07:55:09 2013 +0200
@@ -129,7 +129,7 @@
     Live
     Live_True
     Hoare_Examples
-    VC
+    VCG
     HoareT
     Collecting1
     Collecting_Examples