Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/MicroJava/BV/BVSpecTypeSafe.thy
changeset 32960 69916a850301
parent 28524 644b62cf678f
child 40928 ace26e2cee91 
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Sat Oct 17 01:05:59 2009 +0200
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Sat Oct 17 14:43:18 2009 +0200
@@ -1,5 +1,4 @@
 (*  Title:      HOL/MicroJava/BV/BVSpecTypeSafe.thy
-    ID:         $Id$
     Author:     Cornelia Pusch, Gerwin Klein
     Copyright   1999 Technische Universitaet Muenchen
 *)
@@ -1332,7 +1331,7 @@
   apply (auto simp add: fun_upd_apply blank_def oconf_def split: split_if_asm)
   apply (simp add: fields_is_type 
           [OF _ wf [THEN wf_prog_ws_prog] 
-	        is_class_xcpt [OF wf [THEN wf_prog_ws_prog]]])+
+                is_class_xcpt [OF wf [THEN wf_prog_ws_prog]]])+
   done
     
 lemma
isabelle