nominal2: Paper/Paper.thy@a728e199851d

Paper/Paper.thy

author	Cezary Kaliszyk <kaliszyk@in.tum.de>
	Wed, 24 Feb 2010 14:55:09 +0100
changeset 1247	a728e199851d
parent 754	b85875d65b10
child 1473	b4216d0e109a
permissions	-rw-r--r--

Factor-out 'prove_perm_empty'; I plan to use it in defining permutations on the lifted type.


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

section {* Introduction *}

text {*
  Here can come any text.

*}

(*<*)
end
(*>*)

nominal2