summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Library/ListVector.thy

changeset 66453 | cc19f7ca2ed6 |

parent 63882 | 018998c00003 |

child 67006 | b1278ed3cd46 |

equal
deleted
inserted
replaced

66452:450cefec7c11 | 66453:cc19f7ca2ed6 |
---|---|

1 (* Author: Tobias Nipkow, 2007 *) |
1 (* Author: Tobias Nipkow, 2007 *) |

2 |
2 |

3 section \<open>Lists as vectors\<close> |
3 section \<open>Lists as vectors\<close> |

4 |
4 |

5 theory ListVector |
5 theory ListVector |

6 imports List Main |
6 imports HOL.List Main |

7 begin |
7 begin |

8 |
8 |

9 text\<open>\noindent |
9 text\<open>\noindent |

10 A vector-space like structure of lists and arithmetic operations on them. |
10 A vector-space like structure of lists and arithmetic operations on them. |

11 Is only a vector space if restricted to lists of the same length.\<close> |
11 Is only a vector space if restricted to lists of the same length.\<close> |