equal
deleted
inserted
replaced
1054 eq_set(add_term_vars(t,[]), add_term_vars(u,[])) |
1054 eq_set(add_term_vars(t,[]), add_term_vars(u,[])) |
1055 |
1055 |
1056 (*simple test for looping rewrite*) |
1056 (*simple test for looping rewrite*) |
1057 fun loops sign prems (lhs,rhs) = |
1057 fun loops sign prems (lhs,rhs) = |
1058 is_Var(lhs) orelse |
1058 is_Var(lhs) orelse |
1059 (is_Free(lhs) andalso (lhs mem (foldr add_term_frees (prems,[])))) orelse |
1059 (is_Free(lhs) andalso (lhs mem (foldr add_term_frees (rhs::prems,[])))) orelse |
1060 (null(prems) andalso |
1060 (null(prems) andalso |
1061 Pattern.matches (#tsig(Sign.rep_sg sign)) (lhs,rhs)); |
1061 Pattern.matches (#tsig(Sign.rep_sg sign)) (lhs,rhs)); |
1062 |
1062 |
1063 fun mk_rrule (thm as Thm{hyps,sign,prop,maxidx,...}) = |
1063 fun mk_rrule (thm as Thm{hyps,sign,prop,maxidx,...}) = |
1064 let val prems = Logic.strip_imp_prems prop |
1064 let val prems = Logic.strip_imp_prems prop |