summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Tue, 16 Jan 2001 00:25:00 +0100 | |

changeset 10902 | 0f512daadbd5 |

parent 10901 | bf131ef38495 |

child 10903 | ad1fb17361e4 |

split_conv;

--- a/doc-src/TutorialI/Types/Pairs.thy Tue Jan 16 00:24:36 2001 +0100 +++ b/doc-src/TutorialI/Types/Pairs.thy Tue Jan 16 00:25:00 2001 +0100 @@ -71,7 +71,7 @@ first place, we quickly realize that what we would like is to replace @{term p} with some concrete pair @{term"(a,b)"}, in which case both sides of the equation would simplify to @{term a} because of the simplification rules -@{thm Product_Type.split[no_vars]} and @{thm fst_conv[no_vars]}. This is the +@{thm split_conv[no_vars]} and @{thm fst_conv[no_vars]}. This is the key problem one faces when reasoning about pattern matching with pairs: how to convert some atomic term into a pair.