isabelle: src/HOL/PreList.thy@18b76c137c41 (annotated)

8563 2746bc9a7ef2 comments nipkow parents: 8490 diff changeset	1	(* Title: HOL/List.thy
2746bc9a7ef2 comments nipkow parents: 8490 diff changeset	2	ID: $Id$
2746bc9a7ef2 comments nipkow parents: 8490 diff changeset	3	Author: Tobias Nipkow
2746bc9a7ef2 comments nipkow parents: 8490 diff changeset	4	Copyright 2000 TU Muenchen
2746bc9a7ef2 comments nipkow parents: 8490 diff changeset	5
2746bc9a7ef2 comments nipkow parents: 8490 diff changeset	6	A basis for building theory List on. Is defined separately to serve as a
2746bc9a7ef2 comments nipkow parents: 8490 diff changeset	7	basis for theory ToyList in the documentation.
2746bc9a7ef2 comments nipkow parents: 8490 diff changeset	8	*)
8490 6e0f23304061 added HOL/PreLIst.thy; wenzelm parents: diff changeset	9
6e0f23304061 added HOL/PreLIst.thy; wenzelm parents: diff changeset	10	theory PreList =
8840 18b76c137c41 moved theory Sexp to Induct examples; wenzelm parents: 8756 diff changeset	11	Option + WF_Rel + NatBin + Recdef + Record + RelPow + Calculation + SVC_Oracle
8756 b03a0b219139 new file Integ/NatSimprocs.ML paulson parents: 8563 diff changeset	12	files "Integ/NatSimprocs.ML":
8490 6e0f23304061 added HOL/PreLIst.thy; wenzelm parents: diff changeset	13
6e0f23304061 added HOL/PreLIst.thy; wenzelm parents: diff changeset	14	end