isabelle: src/HOL/Word/Word.thy@d9294387ab0e (annotated)

29628 d9294387ab0e entry point for Word library now named Word haftmann parents: 27137 diff changeset	1	(* Title: HOL/Word/Word.thy
d9294387ab0e entry point for Word library now named Word haftmann parents: 27137 diff changeset	2	Author: Gerwin Klein, NICTA
24333 e77ea0ea7f2c * HOL-Word: kleing parents: diff changeset	3	*)
e77ea0ea7f2c * HOL-Word: kleing parents: diff changeset	4
29628 d9294387ab0e entry point for Word library now named Word haftmann parents: 27137 diff changeset	5	header {* Word Library interafce *}
24350 4d74f37c6367 headers for document generation huffman parents: 24333 diff changeset	6
29628 d9294387ab0e entry point for Word library now named Word haftmann parents: 27137 diff changeset	7	theory Word
26560 d2fc9a18ee8a tuned haftmann parents: 26086 diff changeset	8	imports WordGenLib
24333 e77ea0ea7f2c * HOL-Word: kleing parents: diff changeset	9	begin
e77ea0ea7f2c * HOL-Word: kleing parents: diff changeset	10
29628 d9294387ab0e entry point for Word library now named Word haftmann parents: 27137 diff changeset	11	text {* see @{text "Examples/WordExamples.thy"} for examples *}
24333 e77ea0ea7f2c * HOL-Word: kleing parents: diff changeset	12
e77ea0ea7f2c * HOL-Word: kleing parents: diff changeset	13	end

author	haftmann
	Mon, 26 Jan 2009 22:14:16 +0100
changeset 29628	d9294387ab0e
parent 27137	src/HOL/Word/WordMain.thy@d0070c32fdc1
child 35049	00f311c32444
permissions	-rw-r--r--