isabelle: src/HOL/PreList.thy@73b8b42a36b6 (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
20591 7cbb224598b2 text cleanup haftmann parents: 17508 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
24742 73b8b42a36b6 removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering paulson parents: 24699 diff changeset	10	imports ATP_Linkup
24616 fac3dd4ade83 sorting nipkow parents: 23708 diff changeset	11	uses "Tools/function_package/lexicographic_order.ML"
fac3dd4ade83 sorting nipkow parents: 23708 diff changeset	12	"Tools/function_package/fundef_datatype.ML"
15131 c69542757a4d New theory header syntax. nipkow parents: 14577 diff changeset	13	begin
12397 6766aa05e4eb less_induct, wf_induct_rule; wenzelm parents: 12304 diff changeset	14
14577 dbb95b825244 tuned document; wenzelm parents: 14430 diff changeset	15	text {*
20591 7cbb224598b2 text cleanup haftmann parents: 17508 diff changeset	16	This is defined separately to serve as a basis for
7cbb224598b2 text cleanup haftmann parents: 17508 diff changeset	17	theory ToyList in the documentation.
7cbb224598b2 text cleanup haftmann parents: 17508 diff changeset	18	*}
14577 dbb95b825244 tuned document; wenzelm parents: 14430 diff changeset	19
24616 fac3dd4ade83 sorting nipkow parents: 23708 diff changeset	20	(* The lexicographic_order method and the "fun" command *)
fac3dd4ade83 sorting nipkow parents: 23708 diff changeset	21	setup LexicographicOrder.setup
fac3dd4ade83 sorting nipkow parents: 23708 diff changeset	22	setup FundefDatatype.setup
fac3dd4ade83 sorting nipkow parents: 23708 diff changeset	23
8490 6e0f23304061 added HOL/PreLIst.thy; wenzelm parents: diff changeset	24	end

author	paulson
	Thu, 27 Sep 2007 17:55:28 +0200
changeset 24742	73b8b42a36b6
parent 24699	c6674504103f
child 25517	36d710d1dbce
permissions	-rw-r--r--