isabelle: src/HOL/PreList.thy@5cb24165a2e1 (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
14125 bf8edef6c1f1 tidied paulson parents: 13878 diff changeset	9	(*Is defined separately to serve as a basis for theory ToyList in the
bf8edef6c1f1 tidied paulson parents: 13878 diff changeset	10	documentation.*)
8490 6e0f23304061 added HOL/PreLIst.thy; wenzelm parents: diff changeset	11
14430 5cb24165a2e1 new material from Avigad, and simplified treatment of division by 0 paulson parents: 14125 diff changeset	12	theory PreList =
5cb24165a2e1 new material from Avigad, and simplified treatment of division by 0 paulson parents: 14125 diff changeset	13	Wellfounded_Relations + Presburger + Recdef + Relation_Power + Parity:
12397 6766aa05e4eb less_induct, wf_induct_rule; wenzelm parents: 12304 diff changeset	14
10261 bb2f1e859177 tuned declarations; wenzelm parents: 10212 diff changeset	15	(belongs to theory Wellfounded_Recursion)
12397 6766aa05e4eb less_induct, wf_induct_rule; wenzelm parents: 12304 diff changeset	16	lemmas wf_induct_rule = wf_induct [rule_format, case_names less, induct set: wf]
9066 b1e874e38dab theorems [cases type: bool] = case_split; wenzelm parents: 8862 diff changeset	17
8490 6e0f23304061 added HOL/PreLIst.thy; wenzelm parents: diff changeset	18	end

author	paulson
	Thu, 04 Mar 2004 12:06:07 +0100
changeset 14430	5cb24165a2e1
parent 14125	bf8edef6c1f1
child 14577	dbb95b825244
permissions	-rw-r--r--