src/Doc/Tutorial/Types/Numbers.thy
changeset 61694 6571c78c9667
parent 58860 fee7cfa69c50
child 64242 93c6f0da5c70
     1.1 --- a/src/Doc/Tutorial/Types/Numbers.thy	Tue Nov 17 12:01:19 2015 +0100
     1.2 +++ b/src/Doc/Tutorial/Types/Numbers.thy	Tue Nov 17 12:32:08 2015 +0000
     1.3 @@ -22,8 +22,8 @@
     1.4  *}
     1.5  
     1.6  text{*
     1.7 -@{thm[display] numeral_1_eq_1[no_vars]}
     1.8 -\rulename{numeral_1_eq_1}
     1.9 +@{thm[display] numeral_One[no_vars]}
    1.10 +\rulename{numeral_One}
    1.11  
    1.12  @{thm[display] add_2_eq_Suc[no_vars]}
    1.13  \rulename{add_2_eq_Suc}