|
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 |
|
|
14125
|
7 |
header{*A Basis for Building the Theory of Lists*}
|
|
12020
|
8 |
|
|
14125
|
9 |
(*Is defined separately to serve as a basis for theory ToyList in the
|
|
|
10 |
documentation.*)
|
|
8490
|
11 |
|
|
14125
|
12 |
theory PreList = Wellfounded_Relations + Presburger + Recdef + Relation_Power:
|
|
12397
|
13 |
|
|
10261
|
14 |
(*belongs to theory Wellfounded_Recursion*)
|
|
12397
|
15 |
lemmas wf_induct_rule = wf_induct [rule_format, case_names less, induct set: wf]
|
|
9066
|
16 |
|
|
8490
|
17 |
end
|