changeset 11908 | 82f68fd05094 |
parent 11701 | 3d51fbf81c17 |
child 12338 | de0f4a63baa5 |
--- a/src/HOL/MicroJava/J/Value.thy Tue Oct 23 22:51:30 2001 +0200 +++ b/src/HOL/MicroJava/J/Value.thy Tue Oct 23 22:52:31 2001 +0200 @@ -40,7 +40,7 @@ primrec "defpval Void = Unit" "defpval Boolean = Bool False" - "defpval Integer = Intg (Numeral0)" + "defpval Integer = Intg 0" primrec "default_val (PrimT pt) = defpval pt"