equal
deleted
inserted
replaced
73 |
73 |
74 fun forall_intr_rename (n, cv) thm = |
74 fun forall_intr_rename (n, cv) thm = |
75 let |
75 let |
76 val allthm = Thm.forall_intr cv thm |
76 val allthm = Thm.forall_intr cv thm |
77 val (_ $ abs) = prop_of allthm |
77 val (_ $ abs) = prop_of allthm |
78 in |
78 in Thm.rename_boundvars abs (Abs (n, dummyT, Term.dummy)) allthm end |
79 Thm.rename_boundvars abs (Abs (n, dummyT, Term.dummy_pattern dummyT)) allthm |
|
80 end |
|
81 |
79 |
82 |
80 |
83 datatype proof_attempt = Solved of thm | Stuck of thm | Fail |
81 datatype proof_attempt = Solved of thm | Stuck of thm | Fail |
84 |
82 |
85 fun try_proof cgoal tac = |
83 fun try_proof cgoal tac = |