isabelle: doc-src/IsarImplementation/Thy/Base.thy@ab0afd03a042 (annotated)

29755 d66b34e46bdf observe usual theory naming conventions; wenzelm parents: 26957 diff changeset	1	theory Base
39846 cb6634eb8926 examples in Isabelle/HOL; wenzelm parents: 30272 diff changeset	2	imports Main
21374 27ae6bc4102a common antiquote_setup.ML; wenzelm parents: 18537 diff changeset	3	uses "../../antiquote_setup.ML"
18537 2681f9e34390 "The Isabelle/Isar Implementation" manual; wenzelm parents: diff changeset	4	begin
30272 2d612824e642 regenerated document; wenzelm parents: 30270 diff changeset	5
39866 5ec01d5acd0c more robust examples: explicit @{assert} instead of unchecked output; wenzelm parents: 39846 diff changeset	6	(* FIXME move to src/Pure/ML/ml_antiquote.ML *)
5ec01d5acd0c more robust examples: explicit @{assert} instead of unchecked output; wenzelm parents: 39846 diff changeset	7	ML {*
5ec01d5acd0c more robust examples: explicit @{assert} instead of unchecked output; wenzelm parents: 39846 diff changeset	8	ML_Antiquote.inline "assert"
5ec01d5acd0c more robust examples: explicit @{assert} instead of unchecked output; wenzelm parents: 39846 diff changeset	9	(Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")")
5ec01d5acd0c more robust examples: explicit @{assert} instead of unchecked output; wenzelm parents: 39846 diff changeset	10	*}
5ec01d5acd0c more robust examples: explicit @{assert} instead of unchecked output; wenzelm parents: 39846 diff changeset	11
18537 2681f9e34390 "The Isabelle/Isar Implementation" manual; wenzelm parents: diff changeset	12	end

author	wenzelm
	Fri, 22 Oct 2010 19:03:31 +0100
changeset 39882	ab0afd03a042
parent 39866	5ec01d5acd0c
child 40110	93e7935d4cb5
permissions	-rw-r--r--