src/HOL/MicroJava/BV/BVExample.thy
changeset 13006 51c5f3f11d16
parent 12972 da7345ff18e1
child 13043 ad1828b479b7
equal deleted inserted replaced
13005:42a54d6cec15 13006:51c5f3f11d16
   274   apply (simp add: match_exception_entry_def)
   274   apply (simp add: match_exception_entry_def)
   275   apply simp
   275   apply simp
   276   apply simp
   276   apply simp
   277   done
   277   done
   278 
   278 
   279 text {* Some shorthands to make the welltyping of method @{term
   279 text {* Some abbreviations for readability *} 
   280 makelist_name} easier to read *} 
       
   281 syntax
   280 syntax
   282   list :: ty 
   281   list :: ty 
   283   test :: ty
   282   test :: ty
   284 translations
   283 translations
   285   "list" == "Class list_name"
   284   "list" == "Class list_name"