isabelle: src/Doc/Tutorial/ToyList/ToyList1.txt@35d85fd89fc1 (annotated)

15136 1275417e3930 Adapted text to new theory header syntax. nipkow parents: 9541 diff changeset	1	theory ToyList
58926 baf5a3c28f0c proper import of Main: BNF_Least_Fixpoint does not "contain pretty much everything", especially it lacks the 'value' command, which is defined after theory List; wenzelm parents: 58372 diff changeset	2	imports Main
15136 1275417e3930 Adapted text to new theory header syntax. nipkow parents: 9541 diff changeset	3	begin
8751 9ed0548177fb * empty log message * nipkow parents: diff changeset	4
58926 baf5a3c28f0c proper import of Main: BNF_Least_Fixpoint does not "contain pretty much everything", especially it lacks the 'value' command, which is defined after theory List; wenzelm parents: 58372 diff changeset	5	no_notation Nil ("[]") and Cons (infixr "#" 65) and append (infixr "@" 65)
baf5a3c28f0c proper import of Main: BNF_Least_Fixpoint does not "contain pretty much everything", especially it lacks the 'value' command, which is defined after theory List; wenzelm parents: 58372 diff changeset	6	hide_type list
baf5a3c28f0c proper import of Main: BNF_Least_Fixpoint does not "contain pretty much everything", especially it lacks the 'value' command, which is defined after theory List; wenzelm parents: 58372 diff changeset	7	hide_const rev
baf5a3c28f0c proper import of Main: BNF_Least_Fixpoint does not "contain pretty much everything", especially it lacks the 'value' command, which is defined after theory List; wenzelm parents: 58372 diff changeset	8
8751 9ed0548177fb * empty log message * nipkow parents: diff changeset	9	datatype 'a list = Nil ("[]")
9541 d17c0b34d5c8 * empty log message * nipkow parents: 8846 diff changeset	10	\| Cons 'a "'a list" (infixr "#" 65)
8751 9ed0548177fb * empty log message * nipkow parents: diff changeset	11
38430 254a021ed66e tuned text about "value" and added note on comments. nipkow parents: 27015 diff changeset	12	(* This is the append function: *)
27015 f8537d69f514 * empty log message * nipkow parents: 26729 diff changeset	13	primrec app :: "'a list => 'a list => 'a list" (infixr "@" 65)
f8537d69f514 * empty log message * nipkow parents: 26729 diff changeset	14	where
f8537d69f514 * empty log message * nipkow parents: 26729 diff changeset	15	"[] @ ys = ys" \|
9541 d17c0b34d5c8 * empty log message * nipkow parents: 8846 diff changeset	16	"(x # xs) @ ys = x # (xs @ ys)"
8751 9ed0548177fb * empty log message * nipkow parents: diff changeset	17
27015 f8537d69f514 * empty log message * nipkow parents: 26729 diff changeset	18	primrec rev :: "'a list => 'a list" where
f8537d69f514 * empty log message * nipkow parents: 26729 diff changeset	19	"rev [] = []" \|
9541 d17c0b34d5c8 * empty log message * nipkow parents: 8846 diff changeset	20	"rev (x # xs) = (rev xs) @ (x # [])"

author	wenzelm
	Tue, 11 Aug 2015 13:50:59 +0200
changeset 60888	35d85fd89fc1
parent 58926	baf5a3c28f0c
permissions	-rw-r--r--