Attic/UnusedQuotMain.thy
author Christian Urban <urbanc@in.tum.de>
Mon, 27 Jun 2011 22:51:42 +0100
changeset 2911 567967bc94cc
parent 2871 b58073719b06
permissions -rw-r--r--
streamlined the fcb-proof and made fcb1 a special case of fcb

(* Could go in the programming tutorial *)

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