equal
deleted
inserted
replaced
48 val g = Thm.capply (Thm.capply @{cterm "op ==>"} (Thm.capply @{cterm "Trueprop"} ng)) p' |
48 val g = Thm.capply (Thm.capply @{cterm "op ==>"} (Thm.capply @{cterm "Trueprop"} ng)) p' |
49 val ntac = (case qs of [] => q aconvc @{cterm "False"} |
49 val ntac = (case qs of [] => q aconvc @{cterm "False"} |
50 | _ => false) |
50 | _ => false) |
51 in |
51 in |
52 if ntac then no_tac st |
52 if ntac then no_tac st |
53 else rtac (Goal.prove_raw [] g (K (blast_tac HOL_cs 1))) i st |
53 else rtac (Goal.prove_internal [] g (K (blast_tac HOL_cs 1))) i st |
54 end; |
54 end; |
55 |
55 |
56 local |
56 local |
57 fun ty cts t = |
57 fun ty cts t = |
58 if not (typ_of (ctyp_of_term t) mem [HOLogic.intT, HOLogic.natT]) then false |
58 if not (typ_of (ctyp_of_term t) mem [HOLogic.intT, HOLogic.natT]) then false |