summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/PreList.thy

author | paulson |

Thu Mar 04 12:06:07 2004 +0100 (2004-03-04) | |

changeset 14430 | 5cb24165a2e1 |

parent 14125 | bf8edef6c1f1 |

child 14577 | dbb95b825244 |

permissions | -rw-r--r-- |

new material from Avigad, and simplified treatment of division by 0

1 (* Title: HOL/PreList.thy

2 ID: $Id$

3 Author: Tobias Nipkow and Markus Wenzel

4 Copyright 2000 TU Muenchen

5 *)

7 header{*A Basis for Building the Theory of Lists*}

9 (*Is defined separately to serve as a basis for theory ToyList in the

10 documentation.*)

12 theory PreList =

13 Wellfounded_Relations + Presburger + Recdef + Relation_Power + Parity:

15 (*belongs to theory Wellfounded_Recursion*)

16 lemmas wf_induct_rule = wf_induct [rule_format, case_names less, induct set: wf]

18 end