src/HOL/MicroJava/BV/BVExample.thy
changeset 13006 51c5f3f11d16
parent 12972 da7345ff18e1
child 13043 ad1828b479b7
--- a/src/HOL/MicroJava/BV/BVExample.thy	Sat Mar 02 12:09:23 2002 +0100
+++ b/src/HOL/MicroJava/BV/BVExample.thy	Sun Mar 03 16:59:08 2002 +0100
@@ -276,8 +276,7 @@
   apply simp
   done
 
-text {* Some shorthands to make the welltyping of method @{term
-makelist_name} easier to read *} 
+text {* Some abbreviations for readability *} 
 syntax
   list :: ty 
   test :: ty
@@ -382,4 +381,4 @@
   apply (simp add: conf_def start_heap_def)
   done
 
-end
\ No newline at end of file
+end