equal
deleted
inserted
replaced
24 | Calculate' of Rule.theory' * string * term * (term * Celem.thm') |
24 | Calculate' of Rule.theory' * string * term * (term * Celem.thm') |
25 | Check_Postcond' of Celem.pblID * term |
25 | Check_Postcond' of Celem.pblID * term |
26 | Check_elementwise' of term * Rule.cterm' * Selem.result |
26 | Check_elementwise' of term * Rule.cterm' * Selem.result |
27 | Del_Find' of Rule.cterm' | Del_Given' of Rule.cterm' | Del_Relation' of Rule.cterm' |
27 | Del_Find' of Rule.cterm' | Del_Given' of Rule.cterm' | Del_Relation' of Rule.cterm' |
28 |
28 |
29 | Derive' of Rule.rls |
29 | Derive' of Rule.rls |
30 | Detail_Set' of Rule.theory' * bool * Rule.rls * term * Selem.result |
30 | Detail_Set' of Rule.theory' * bool * Rule.rls * term * Selem.result |
31 | Detail_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule.rls * term * Selem.result |
31 | Detail_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule.rls * term * Selem.result |
32 | End_Detail' of Selem.result |
32 | End_Detail' of Selem.result |
33 |
33 |
34 | Empty_Tac_ |
34 | Empty_Tac_ |