nominal2: Paper/Paper.thy@f0a78fda343f

Paper/Paper.thy

author	Christian Urban <urbanc@in.tum.de>
	Sat, 26 Dec 2009 20:45:37 +0100
changeset 794	f0a78fda343f
parent 754	b85875d65b10
child 1473	b4216d0e109a
permissions	-rw-r--r--

added an item about when the same quotient constant is defined twice (throws a bind exception in quoteint_def.ML)


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

section {* Introduction *}

text {*
  Here can come any text.

*}

(*<*)
end
(*>*)

nominal2