doc-src/IsarImplementation/Thy/ML.thy
author wenzelm
Tue, 12 Sep 2006 17:45:58 +0200
changeset 20520 05fd007bdeb9
parent 20491 98ba42f19995
child 21148 3a64d58a9f49
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
20520
wenzelm
parents: 20491
diff changeset
    16
text {* FIXME beyond the NJ basis library proposal *}
18538
88fe84d4d151 outline;
wenzelm
parents: 18537
diff changeset
    17
20489
a684fc70d04e tentative appendix C;
wenzelm
parents: 18554
diff changeset
    18
a684fc70d04e tentative appendix C;
wenzelm
parents: 18554
diff changeset
    19
chapter {* Cookbook *}
a684fc70d04e tentative appendix C;
wenzelm
parents: 18554
diff changeset
    20
20491
wenzelm
parents: 20489
diff changeset
    21
section {* A method that depends on declarations in the context *}
20489
a684fc70d04e tentative appendix C;
wenzelm
parents: 18554
diff changeset
    22
a684fc70d04e tentative appendix C;
wenzelm
parents: 18554
diff changeset
    23
text FIXME
a684fc70d04e tentative appendix C;
wenzelm
parents: 18554
diff changeset
    24
18538
88fe84d4d151 outline;
wenzelm
parents: 18537
diff changeset
    25
end