isabelle: src/HOL/PreList.thy@0382f6877b98 (annotated)

10519 ade64af4c57c hide many names from Datatype_Universe. nipkow parents: 10261 diff changeset	1	(* Title: HOL/PreList.thy
8563 2746bc9a7ef2 comments nipkow parents: 8490 diff changeset	2	ID: $Id$
10733 59f82484e000 hide type node item; wenzelm parents: 10680 diff changeset	3	Author: Tobias Nipkow and Markus Wenzel
8563 2746bc9a7ef2 comments nipkow parents: 8490 diff changeset	4	Copyright 2000 TU Muenchen
2746bc9a7ef2 comments nipkow parents: 8490 diff changeset	5	*)
8490 6e0f23304061 added HOL/PreLIst.thy; wenzelm parents: diff changeset	6
14125 bf8edef6c1f1 tidied paulson parents: 13878 diff changeset	7	header{A Basis for Building the Theory of Lists}
12020 a24373086908 theory Calculation move to Set; wenzelm parents: 11955 diff changeset	8
15131 c69542757a4d New theory header syntax. nipkow parents: 14577 diff changeset	9	theory PreList
16760 5c5f051aaaaa changed imports due to new GCD.thy nipkow parents: 15298 diff changeset	10	imports Wellfounded_Relations Presburger Relation_Power GCD
15131 c69542757a4d New theory header syntax. nipkow parents: 14577 diff changeset	11	begin
12397 6766aa05e4eb less_induct, wf_induct_rule; wenzelm parents: 12304 diff changeset	12
14577 dbb95b825244 tuned document; wenzelm parents: 14430 diff changeset	13	text {*
dbb95b825244 tuned document; wenzelm parents: 14430 diff changeset	14	Is defined separately to serve as a basis for theory ToyList in the
dbb95b825244 tuned document; wenzelm parents: 14430 diff changeset	15	documentation. *}
dbb95b825244 tuned document; wenzelm parents: 14430 diff changeset	16
8490 6e0f23304061 added HOL/PreLIst.thy; wenzelm parents: diff changeset	17	end

author	paulson
	Thu, 15 Sep 2005 17:45:17 +0200
changeset 17421	0382f6877b98
parent 17042	da5cfaa258f7
child 17508	c84af7f39a6b
permissions	-rw-r--r--