equal
deleted
inserted
replaced
898 if RealArith.is_ratconst (Thm.dest_arg1 tm) andalso |
898 if RealArith.is_ratconst (Thm.dest_arg1 tm) andalso |
899 not (member (op aconvc) fvs (Thm.dest_arg tm)) |
899 not (member (op aconvc) fvs (Thm.dest_arg tm)) |
900 then (RealArith.dest_ratconst (Thm.dest_arg1 tm), Thm.dest_arg tm) |
900 then (RealArith.dest_ratconst (Thm.dest_arg1 tm), Thm.dest_arg tm) |
901 else raise Failure "substitutable_monomial" |
901 else raise Failure "substitutable_monomial" |
902 | @{term "op + :: real => _"}$_$_ => |
902 | @{term "op + :: real => _"}$_$_ => |
903 (substitutable_monomial (Thm.add_cterm_frees (Thm.dest_arg tm) fvs) (Thm.dest_arg1 tm) |
903 (substitutable_monomial (Drule.cterm_add_frees (Thm.dest_arg tm) fvs) (Thm.dest_arg1 tm) |
904 handle Failure _ => |
904 handle Failure _ => |
905 substitutable_monomial (Thm.add_cterm_frees (Thm.dest_arg1 tm) fvs) (Thm.dest_arg tm)) |
905 substitutable_monomial (Drule.cterm_add_frees (Thm.dest_arg1 tm) fvs) (Thm.dest_arg tm)) |
906 | _ => raise Failure "substitutable_monomial") |
906 | _ => raise Failure "substitutable_monomial") |
907 |
907 |
908 fun isolate_variable v th = |
908 fun isolate_variable v th = |
909 let |
909 let |
910 val w = Thm.dest_arg1 (Thm.cprop_of th) |
910 val w = Thm.dest_arg1 (Thm.cprop_of th) |