isabelle: doc-src/IsarImplementation/Thy/ML.thy@c40ce2de2020 (annotated)

18537 2681f9e34390 "The Isabelle/Isar Implementation" manual; wenzelm parents: diff changeset	1
18538 88fe84d4d151 outline; wenzelm parents: 18537 diff changeset	2	(* $Id$ *)
88fe84d4d151 outline; wenzelm parents: 18537 diff changeset	3
88fe84d4d151 outline; wenzelm parents: 18537 diff changeset	4	theory "ML" imports base begin
88fe84d4d151 outline; wenzelm parents: 18537 diff changeset	5
88fe84d4d151 outline; wenzelm parents: 18537 diff changeset	6	chapter {* Aesthetics of ML programming *}
88fe84d4d151 outline; wenzelm parents: 18537 diff changeset	7
18554 bff7a1466fe4 more stuff; wenzelm parents: 18538 diff changeset	8	text {* FIXME style guide, see also
bff7a1466fe4 more stuff; wenzelm parents: 18538 diff changeset	9	\url{http://caml.inria.fr/resources/doc/guides/guidelines.en.html} and
bff7a1466fe4 more stuff; wenzelm parents: 18538 diff changeset	10	\url{http://www.cs.cornell.edu/Courses/cs312/2003sp/handouts/style.htm}
bff7a1466fe4 more stuff; wenzelm parents: 18538 diff changeset	11	*}
18538 88fe84d4d151 outline; wenzelm parents: 18537 diff changeset	12
88fe84d4d151 outline; wenzelm parents: 18537 diff changeset	13
88fe84d4d151 outline; wenzelm parents: 18537 diff changeset	14	chapter {* Basic library functions *}
88fe84d4d151 outline; wenzelm parents: 18537 diff changeset	15
88fe84d4d151 outline; wenzelm parents: 18537 diff changeset	16	text {* FIXME beyond the basis library definition *}
88fe84d4d151 outline; wenzelm parents: 18537 diff changeset	17
88fe84d4d151 outline; wenzelm parents: 18537 diff changeset	18	end

author	krauss
	Mon, 05 Jun 2006 14:22:58 +0200
changeset 19769	c40ce2de2020
parent 18554	bff7a1466fe4
child 20489	a684fc70d04e
permissions	-rw-r--r--