Attic/UnusedQuotMain.thy
author Cezary Kaliszyk <kaliszyk@in.tum.de>
Tue, 05 Jul 2011 09:26:20 +0900
changeset 2940 cc0605102f95
parent 2871 b58073719b06
permissions -rw-r--r--
Move If / Let with 'True' to the end of Lambda

(* Could go in the programming tutorial *)

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