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