isabelle: 4acc029f69e9 tip afp: c0882468fab2 tip > HOL-ODE-Numerics FAILED > (see also > /home/haftmann/.isabelle/heaps/polyml-5.7.1_x86_64-linux/log/HOL-ODE-Numerics) > thm -> > int -> > int -> > int -> > int -> > (int * int * string) list -> > string -> Proof.context -> int -> tactic > val poincare'_bnds_tac = fn: > thm -> > int -> > int -> > int -> > int -> > (int * int * string) list -> > string -> Proof.context -> int -> tactic > ### Rule already declared as elimination (elim) > ### \<lbrakk>(?f has_derivative ?f') ?F; > ### bounded_linear ?f' \<Longrightarrow> PROP ?W\<rbrakk> > ### \<Longrightarrow> PROP ?W > ### theory "HOL-ODE-Numerics.Example_Utilities" > ### 52.579s elapsed time, 113.340s cpu time, 12.052s GC time > Loading theory "HOL-ODE-Numerics.ODE_Numerics" > ### Introduced fixed type variable(s): 'b in "X__" > ### theory "HOL-ODE-Numerics.ODE_Numerics" > ### 0.056s elapsed time, 0.168s cpu time, 0.000s GC time > *** Failed to apply initial proof method (line 985 of > "~/data/tum/afp/master/thys/Ordinary_Differential_Equations/Numerics/Runge_Kutta.thy"): > *** using this: > *** convex (T \<times> X) > *** \<forall>x\<in>T \<times> X. > *** ((\<lambda>(t, x). f t x) has_derivative f' x) > *** (at x within T \<times> X) > *** \<forall>x\<in>T \<times> X. onorm (f' x) \<le> B' > *** (t, x) \<in> T \<times> X > *** (t, y) \<in> T \<times> X > *** goal (1 subgoal): > *** 1. norm > *** ((case (t, x) of (t, x) \<Rightarrow> f t x) - > *** (case (t, y) of (t, x) \<Rightarrow> f t x)) > *** \<le> B' * norm ((t, x) - (t, y)) > *** At command "by" (line 985 of > "~/data/tum/afp/master/thys/Ordinary_Differential_Equations/Numerics/Runge_Kutta.thy")
-- PGP available: http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
