equal
deleted
inserted
replaced
1 (* Title: HOL/Library/Sublist_Order.thy |
1 (* Title: HOL/Library/Sublist_Order.thy |
2 ID: $Id$ |
|
3 Authors: Peter Lammich, Uni Muenster <peter.lammich@uni-muenster.de> |
2 Authors: Peter Lammich, Uni Muenster <peter.lammich@uni-muenster.de> |
4 Florian Haftmann, TU München |
3 Florian Haftmann, TU Muenchen |
5 *) |
4 *) |
6 |
5 |
7 header {* Sublist Ordering *} |
6 header {* Sublist Ordering *} |
8 |
7 |
9 theory Sublist_Order |
8 theory Sublist_Order |
10 imports Plain "~~/src/HOL/List" |
9 imports Main |
11 begin |
10 begin |
12 |
11 |
13 text {* |
12 text {* |
14 This theory defines sublist ordering on lists. |
13 This theory defines sublist ordering on lists. |
15 A list @{text ys} is a sublist of a list @{text xs}, |
14 A list @{text ys} is a sublist of a list @{text xs}, |