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

author | haftmann |

Sat, 18 Feb 2012 20:06:59 +0100 | |

changeset 46516 | 92f981f4a61b |

parent 46515 | 2a0e1bcf713c |

child 46517 | 9d2e682a68eb |

dropped references to obsolete theories

--- a/doc-src/Codegen/Thy/Refinement.thy Sat Feb 18 20:06:43 2012 +0100 +++ b/doc-src/Codegen/Thy/Refinement.thy Sat Feb 18 20:06:59 2012 +0100 @@ -265,12 +265,10 @@ text {* Typical data structures implemented by representations involving - invariants are available in the library, e.g.~theories @{theory - Cset} and @{theory Mapping} specify sets (type @{typ "'a Cset.set"}) and - key-value-mappings (type @{typ "('a, 'b) mapping"}) respectively; - these can be implemented by distinct lists as presented here as - example (theory @{theory Dlist}) and red-black-trees respectively - (theory @{theory RBT}). + invariants are available in the library, theory @{theory Mapping} + specifies key-value-mappings (type @{typ "('a, 'b) mapping"}); + these can be implemented by red-black-trees (theory @{theory RBT}). *} end +