isabelle: src/Doc/Isar_Ref/Base.thy@4cfe65cfd369 (annotated)

61656 cfabbc083977 more uniform jEdit properties; wenzelm parents: 56451 diff changeset	1	(:maxLineLen=78:)
cfabbc083977 more uniform jEdit properties; wenzelm parents: 56451 diff changeset	2
42651 e3fdb7c96be5 formal Base theory; wenzelm parents: diff changeset	3	theory Base
e3fdb7c96be5 formal Base theory; wenzelm parents: diff changeset	4	imports Pure
62270 77e3ffb5aeb3 misc tuning and updates; wenzelm parents: 61656 diff changeset	5	keywords "\<proof>" :: "qed" % "proof"
42651 e3fdb7c96be5 formal Base theory; wenzelm parents: diff changeset	6	begin
e3fdb7c96be5 formal Base theory; wenzelm parents: diff changeset	7
62270 77e3ffb5aeb3 misc tuning and updates; wenzelm parents: 61656 diff changeset	8	ML \<open>
77e3ffb5aeb3 misc tuning and updates; wenzelm parents: 61656 diff changeset	9	Outer_Syntax.command @{command_keyword "\<proof>"} "dummy proof"
77e3ffb5aeb3 misc tuning and updates; wenzelm parents: 61656 diff changeset	10	(Scan.succeed Isar_Cmd.skip_proof);
77e3ffb5aeb3 misc tuning and updates; wenzelm parents: 61656 diff changeset	11	\<close>
77e3ffb5aeb3 misc tuning and updates; wenzelm parents: 61656 diff changeset	12
48958 12afbf6eb7f9 more standard document preparation within session context; wenzelm parents: 48956 diff changeset	13	ML_file "../antiquote_setup.ML"
42651 e3fdb7c96be5 formal Base theory; wenzelm parents: diff changeset	14
e3fdb7c96be5 formal Base theory; wenzelm parents: diff changeset	15	end