adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

lib/Focus: 2015 update

This commit is contained in:
Gerwin Klein 2015-05-16 21:47:45 +10:00
parent f2cfeb2a0c
commit a09c92bdce
1 changed files with 3 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
lib/Focus.thy
View File

@ -17,8 +17,8 @@ ML {*
fun push_asms_to_concl ctxt nasms thm =
let
val cert = Thm.cterm_of (Proof_Context.theory_of ctxt)
val all_prems = Drule.strip_imp_prems (cprop_of thm)
val cert = Thm.cterm_of ctxt
val all_prems = Drule.strip_imp_prems (Thm.cprop_of thm)
val asms = take nasms all_prems
val B_names = map (fn i => "B" ^ Int.toString i) (1 upto (length all_prems - nasms))
@ -50,8 +50,6 @@ let
fun focus use_asms state =
let
val _ = Proof.assert_backward state
val thy = Proof.theory_of state;
val cert = Thm.cterm_of thy;
val {goal = goal, context = ctxt} = Proof.simple_goal state
@ -90,7 +88,7 @@ fun focus use_asms state =
val concl =
let
val concl = (Logic.unprotect (concl_of focused_goal'))
val concl = (Logic.unprotect (Thm.concl_of focused_goal'))
in
the_default concl (try HOLogic.dest_Trueprop concl) end
in