isabelle: src/HOL/Word/Word.thy@9d7cfae95b30 (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
35049 00f311c32444 tuned spelling haftmann parents: 29628 diff changeset	5	header {* Word Library interface *}
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
36899 bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable boehmes parents: 35049 diff changeset	9	uses "~~/src/HOL/Tools/SMT/smt_word.ML"
24333 e77ea0ea7f2c * HOL-Word: kleing parents: diff changeset	10	begin
e77ea0ea7f2c * HOL-Word: kleing parents: diff changeset	11
36899 bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable boehmes parents: 35049 diff changeset	12	setup {* SMT_Word.setup *}
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable boehmes parents: 35049 diff changeset	13
29628 d9294387ab0e entry point for Word library now named Word haftmann parents: 27137 diff changeset	14	text {* see @{text "Examples/WordExamples.thy"} for examples *}
24333 e77ea0ea7f2c * HOL-Word: kleing parents: diff changeset	15
e77ea0ea7f2c * HOL-Word: kleing parents: diff changeset	16	end

author	blanchet
	Wed, 02 Jun 2010 15:18:48 +0200
changeset 37321	9d7cfae95b30
parent 36899	bcd6fce5bf06
child 37660	56e3520b68b2
permissions	-rw-r--r--