author | wenzelm |
Tue, 31 Jul 2007 00:56:29 +0200 | |
changeset 24076 | ae946f751c44 |
parent 23708 | b5eb0b4dd17d |
child 24616 | fac3dd4ade83 |
permissions | -rw-r--r-- |
10519 | 1 |
(* Title: HOL/PreList.thy |
8563 | 2 |
ID: $Id$ |
10733 | 3 |
Author: Tobias Nipkow and Markus Wenzel |
8563 | 4 |
Copyright 2000 TU Muenchen |
5 |
*) |
|
8490 | 6 |
|
20591 | 7 |
header {* A Basis for Building the Theory of Lists *} |
12020 | 8 |
|
15131 | 9 |
theory PreList |
23708 | 10 |
imports Presburger Relation_Power SAT Recdef Extraction Record |
15131 | 11 |
begin |
12397 | 12 |
|
14577 | 13 |
text {* |
20591 | 14 |
This is defined separately to serve as a basis for |
15 |
theory ToyList in the documentation. |
|
16 |
*} |
|
14577 | 17 |
|
8490 | 18 |
end |
23708 | 19 |