diff -r a6f3e1b08494 -r b6873d123f9b Attic/UnusedQuotMain.thy --- a/Attic/UnusedQuotMain.thy Sat May 12 21:05:59 2012 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,3 +0,0 @@ -(* Could go in the programming tutorial *) - -ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}