equal
deleted
inserted
replaced
26 setsubgoaler asm_simp_tac |
26 setsubgoaler asm_simp_tac |
27 setmksimps (mksimps []) |
27 setmksimps (mksimps []) |
28 |
28 |
29 (* composition of two theorems, used in maps *) |
29 (* composition of two theorems, used in maps *) |
30 fun OF1 thm1 thm2 = thm2 RS thm1 |
30 fun OF1 thm1 thm2 = thm2 RS thm1 |
31 |
|
32 (* FIXME --- now in Isabelle *) |
|
33 fun SOLVED' tac i st = |
|
34 tac i st |> Seq.filter (fn st' => nprems_of st' < nprems_of st) |
|
35 |
31 |
36 (* prints a warning, if the subgoal is not solved *) |
32 (* prints a warning, if the subgoal is not solved *) |
37 fun WARN (tac, msg) i st = |
33 fun WARN (tac, msg) i st = |
38 case Seq.pull ((SOLVED' tac) i st) of |
34 case Seq.pull ((SOLVED' tac) i st) of |
39 NONE => (warning msg; Seq.single st) |
35 NONE => (warning msg; Seq.single st) |