* Support for raw latex output in control symbols: \<^raw...>
* Symbols may only start with one backslash: \<...>. \\<...> is no longer
accepted by the scanner.
- Adapted some Isar-theories to fit to this policy
(* Title: HOL/PreList.thy
ID: $Id$
Author: Tobias Nipkow and Markus Wenzel
Copyright 2000 TU Muenchen
*)
header{*A Basis for Building the Theory of Lists*}
(*Is defined separately to serve as a basis for theory ToyList in the
documentation.*)
theory PreList = Wellfounded_Relations + Presburger + Recdef + Relation_Power:
(*belongs to theory Wellfounded_Recursion*)
lemmas wf_induct_rule = wf_induct [rule_format, case_names less, induct set: wf]
end