| changeset 51272 | 9c8d63b4b6be |
| parent 47399 | b72fa7bf9a10 |
| child 52435 | 6646bb548c6b |
--- a/src/HOL/MicroJava/BV/BVExample.thy Mon Feb 25 12:17:11 2013 +0100 +++ b/src/HOL/MicroJava/BV/BVExample.thy Mon Feb 25 12:17:50 2013 +0100 @@ -480,7 +480,7 @@ definition test2 where "test2 = test_kil E test_name [] (PrimT Void) 3 2 [] make_list_ins" -ML {* +ML_val {* @{code test1}; @{code test2}; *}