nominal2: Paper/Paper.thy@4e0b89d886ac

Paper/Paper.thy

author	Christian Urban <urbanc@in.tum.de>
	Sat, 16 Jan 2010 02:09:38 +0100
changeset 896	4e0b89d886ac
parent 754	b85875d65b10
child 1473	b4216d0e109a
permissions	-rw-r--r--

liftin and lifing_tac can now lift several "and"-separated goals at once; the raw-theorems have to be given in the order of goals


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

section {* Introduction *}

text {*
  Here can come any text.

*}

(*<*)
end
(*>*)

nominal2