# HG changeset patch
# User nipkow
# Date 997106069 -7200
# Node ID d64ccdeaf9ae1bd92d1b6412cd2ee3b23a988a73
# Parent  45d156ede468b1e520ff4e319865787290a87d39
1 -> 1'

diff -r 45d156ede468 -r d64ccdeaf9ae src/HOL/MicroJava/BV/Step.thy
--- a/src/HOL/MicroJava/BV/Step.thy	Mon Aug 06 15:46:20 2001 +0200
+++ b/src/HOL/MicroJava/BV/Step.thy	Mon Aug 06 15:54:29 2001 +0200
@@ -124,12 +124,12 @@
 proof -;
   assume "\<not>(2 < length a)"
   hence "length a < (Suc 2)" by simp
-  hence * : "length a = 0 \<or> length a = 1 \<or> length a = 2" 
+  hence * : "length a = 0 \<or> length a = 1' \<or> length a = 2" 
     by (auto simp add: less_Suc_eq)
 
   { 
     fix x 
-    assume "length x = 1"
+    assume "length x = 1'"
     hence "\<exists> l. x = [l]"  by - (cases x, auto)
   } note 0 = this