summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Library/Code_Abstract_Nat.thy

changeset 56790 | f54097170704 |

parent 55757 | 9fc71814b8c1 |

child 57426 | 2cd2ccd81f93 |

1.1 --- a/src/HOL/Library/Code_Abstract_Nat.thy Tue Apr 29 16:00:34 2014 +0200 1.2 +++ b/src/HOL/Library/Code_Abstract_Nat.thy Tue Apr 29 16:02:02 2014 +0200 1.3 @@ -34,7 +34,7 @@ 1.4 The term @{term "Suc n"} is no longer a valid pattern. Therefore, 1.5 all occurrences of this term in a position where a pattern is 1.6 expected (i.e.~on the left-hand side of a code equation) must be 1.7 - eliminated. This can be accomplished – as far as possible – by 1.8 + eliminated. This can be accomplished -- as far as possible -- by 1.9 applying the following transformation rule: 1.10 *} 1.11