isabelle: src/Doc/Tutorial/Setup.thy@664c1a6cc8c1 (annotated)

72991 d0a0b74f0ad7 avoid multiple uses of the same ML file; wenzelm parents: diff changeset	1	(:maxLineLen=78:)
d0a0b74f0ad7 avoid multiple uses of the same ML file; wenzelm parents: diff changeset	2
d0a0b74f0ad7 avoid multiple uses of the same ML file; wenzelm parents: diff changeset	3	theory Setup
d0a0b74f0ad7 avoid multiple uses of the same ML file; wenzelm parents: diff changeset	4	imports Main
d0a0b74f0ad7 avoid multiple uses of the same ML file; wenzelm parents: diff changeset	5	begin
d0a0b74f0ad7 avoid multiple uses of the same ML file; wenzelm parents: diff changeset	6
d0a0b74f0ad7 avoid multiple uses of the same ML file; wenzelm parents: diff changeset	7	ML_file \<open>../antiquote_setup.ML\<close>
d0a0b74f0ad7 avoid multiple uses of the same ML file; wenzelm parents: diff changeset	8	ML_file \<open>../more_antiquote.ML\<close>
d0a0b74f0ad7 avoid multiple uses of the same ML file; wenzelm parents: diff changeset	9
d0a0b74f0ad7 avoid multiple uses of the same ML file; wenzelm parents: diff changeset	10	end

author	Thomas Lindae <thomas.lindae@in.tum.de>
	Wed, 17 Jul 2024 21:02:30 +0200
changeset 81077	664c1a6cc8c1
parent 72991	d0a0b74f0ad7
permissions	-rw-r--r--