val ax3t = prove_goal T3.thy "$I |- wbx (wbx A -> B) v wbx (wbx B -> A)" (fn _ => [ glob_tac (tfpr pr_intr) 1, disp_tac "-r" 1, glob_tac (tfpr pr_id) 1, d_b_tac "|*@r" (rtac (md2 ssS)) 1, d_b_tac "|*@" (rtac (md1 cbdists)) 1, rtac (md2 blob) 1, rtac threea 1, keep_tac ["|r", "-r"] 1, rtac (wbxa RS TS) 1, rtac idf 1, keep_tac ["|@r", "-r"] 1, rtac wbxA 1, rtac idf 1, keep_tac ["|*@*l", "-l"] 1, glob_tac (tfpr pr_ss) 1, rtac (md1 dcp) 1, rtac wbxa 1, rtac idf 1]) ;