nominal2: Attic/UnusedQuotMain.thy@fb201e383f1b

Attic/UnusedQuotMain.thy

author	Christian Urban <christian dot urban at kcl dot ac dot uk>
	Tue, 19 Feb 2013 05:38:46 +0000
branch	Nominal2-Isabelle2013
changeset 3206	fb201e383f1b
parent 2871	b58073719b06
permissions	-rw-r--r--

added Nominal2-Isabelle 2013 Branch


(* Could go in the programming tutorial *)

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

nominal2