nominal2: Attic/UnusedQuotMain.thy@c4f31f1564b7

Attic/UnusedQuotMain.thy

author	Christian Urban <christian dot urban at kcl dot ac dot uk>
	Sat, 19 Mar 2016 21:06:48 +0000
branch	Nominal2-Isabelle2016
changeset 3243	c4f31f1564b7
parent 2871	b58073719b06
permissions	-rw-r--r--

updated to Isabelle 2016


(* Could go in the programming tutorial *)

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

nominal2