nominal2: Paper/Paper.thy@1e5dee9e6ae2

Paper/Paper.thy

author	Christian Urban <urbanc@in.tum.de>
	Tue, 09 Feb 2010 19:08:08 +0100
changeset 1110	1e5dee9e6ae2
parent 754	b85875d65b10
child 1473	b4216d0e109a
permissions	-rw-r--r--

proper declaration of types and terms during parsing (removes the varifyT when storing data)


(*<*)
theory Paper
imports "../Quot/QuotMain"
begin
(*>*)

section {* Introduction *}

text {*
  Here can come any text.

*}

(*<*)
end
(*>*)

nominal2