nominal2: Attic/UnusedQuotMain.thy@ece7f031708c

Attic/UnusedQuotMain.thy

author	Christian Urban <christian dot urban at kcl dot ac dot uk>
	Thu, 09 Jul 2015 09:13:23 +0100
branch	Nominal2-Isabelle2015
changeset 3241	ece7f031708c
parent 2871	b58073719b06
permissions	-rw-r--r--

updated branch


(* Could go in the programming tutorial *)

ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}

nominal2