isabelle: src/HOL/PreList.thy@6ed42bcba707 (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 =
8862 78643f8449c6 NatSimprocs is now a theory, not a file paulson parents: 8840 diff changeset	11	Option + WF_Rel + NatSimprocs + Recdef + Record + RelPow + Calculation +
9619 6125cc9efc18 fixed deps; wenzelm parents: 9066 diff changeset	12	SVC_Oracle + While:
8490 6e0f23304061 added HOL/PreLIst.thy; wenzelm parents: diff changeset	13
9066 b1e874e38dab theorems [cases type: bool] = case_split; wenzelm parents: 8862 diff changeset	14	theorems [cases type: bool] = case_split
b1e874e38dab theorems [cases type: bool] = case_split; wenzelm parents: 8862 diff changeset	15
8490 6e0f23304061 added HOL/PreLIst.thy; wenzelm parents: diff changeset	16	end

author	paulson
	Thu, 14 Sep 2000 11:34:13 +0200
changeset 9955	6ed42bcba707
parent 9619	6125cc9efc18
child 10212	33fe2d701ddd
permissions	-rw-r--r--