Goal "P & (P --> Q) --> Q" ; br impI 1; be conjE 1; be impCE 1; ba 2; swap; be swap 1; ba 1; val pf = save_proof () ; fun getgoals () = let val ps = prems_of (topthm ()) ; in (chop() ; ps :: getgoals ()) handle _ => [] end ; val gss = getgoals () ; val ctss = map (map (cterm_of Main.thy)) gss ; fun strip_imp (Const("==>", _) $ A $ B) = let val (ps, c) = strip_imp B in (A :: ps, c) end | strip_imp t = ([], t) ; fun mk_latex (Const ("Trueprop", _) $ t) = mk_latex t | mk_latex (Const ("op &", _) $ l $ r) = mk_latex l ^ " \\land " ^ mk_latex r | mk_latex (Const ("op |", _) $ l $ r) = mk_latex l ^ " \\lor " ^ mk_latex r | mk_latex (Const ("op -->", _) $ l $ r) = mk_latex l ^ " \\Rightarrow " ^ mk_latex r | mk_latex (Const ("Not", _) $ t) = " \\lnot " ^ mk_latex t | mk_latex (Free (str, _)) = str | mk_latex (tm as (Const("==>", _) $ _ $ _)) = let val (ps, c) = strip_imp tm ; val cl = mk_latex c ; val psl = separate "," (map mk_latex ps) ; val pslc = String.concat psl ; in pslc ^ " \\vdash " ^ cl end | mk_latex tm = raise TERM ("", [tm]) ; val lss = map (map mk_latex) gss ;