| Sun, 12 Sep 2021 16:18:03 +0200 |
wneuper |
recover test/../biegelinie-1.sml
|
changeset |
files
|
| Sun, 12 Sep 2021 15:53:36 +0200 |
wneuper |
cleanup test/../eqsystem-2.sml
|
changeset |
files
|
| Sun, 12 Sep 2021 15:40:15 +0200 |
wneuper |
cleanup
|
changeset |
files
|
| Mon, 23 Aug 2021 14:24:06 +0200 |
wneuper |
repair rule-set reduce_0_1_2
|
changeset |
files
|
| Mon, 23 Aug 2021 12:33:10 +0200 |
wneuper |
repair fun eval_cancel finished
|
changeset |
files
|
| Sun, 22 Aug 2021 14:28:38 +0200 |
wneuper |
repair fun adhoc_thm + fun eval_cancel
|
changeset |
files
|
| Sun, 22 Aug 2021 11:42:55 +0200 |
wneuper |
improve error message for eval_fn
|
changeset |
files
|
| Sun, 22 Aug 2021 09:43:43 +0200 |
wneuper |
improvement in Rational.thy makes several testfiles run, breaks one.
|
changeset |
files
|
| Sat, 21 Aug 2021 18:58:33 +0200 |
wneuper |
improve usability of Rewrite.trace_on for HyperSearch on long traces
|
changeset |
files
|
| Wed, 18 Aug 2021 20:34:41 +0200 |
wneuper |
replace is_const with is_num, ERROR removed
|
changeset |
files
|
| Wed, 18 Aug 2021 16:46:22 +0200 |
wneuper |
\\re-establish is_const DOES NOT REMOVE THE STRANGE ERROR
|
changeset |
files
|
| Wed, 18 Aug 2021 16:03:08 +0200 |
wneuper |
\\replace is_const with is_num: STRANGE ERROR assoc_calc: 'Prog_Expr.is_num' not found in theory Poly
|
changeset |
files
|
| Wed, 18 Aug 2021 11:35:24 +0200 |
wneuper |
repair test/../root.sml, diff.sml; outcomment NEW errors TOODOO.1
|
changeset |
files
|
| Tue, 17 Aug 2021 22:50:20 +0200 |
wenzelm |
prefer existing signed_string_of_int;
|
changeset |
files
|
| Tue, 17 Aug 2021 22:39:48 +0200 |
wenzelm |
less TODO;
|
changeset |
files
|
| Tue, 17 Aug 2021 21:57:40 +0200 |
wenzelm |
make "sqrt" work by proper use of HOLogic.dest_number and its resulting type;
|
changeset |
files
|
| Tue, 17 Aug 2021 21:48:38 +0200 |
wenzelm |
function definition with explicit names, for the sake of "rule_thm" antiquotation;
|
changeset |
files
|
| Tue, 17 Aug 2021 14:47:12 +0200 |
wenzelm |
more TODO;
|
changeset |
files
|
| Sat, 14 Aug 2021 21:40:55 +0200 |
wneuper |
update TODO.md
|
changeset |
files
|
| Sat, 14 Aug 2021 20:38:23 +0200 |
wneuper |
eliminate some axiomatizations, error with \<^rule_thm>?filterVar.simps(1)?
|
changeset |
files
|
| Sat, 14 Aug 2021 18:59:30 +0200 |
wneuper |
question about merge KEStore_Elems
|
changeset |
files
|
| Sat, 14 Aug 2021 18:49:36 +0200 |
wneuper |
question on @{make_string}, @{print}, @{print tracing}
|
changeset |
files
|
| Sat, 14 Aug 2021 18:13:37 +0200 |
wneuper |
checked all CS from 650e49610bfd upto 63cecf440235
|
changeset |
files
|
| Sat, 14 Aug 2021 16:37:31 +0200 |
wneuper |
proper formal names for types, finished cf.908c760f0def
|
changeset |
files
|
| Sat, 14 Aug 2021 16:07:07 +0200 |
wneuper |
tuned cf.9b839d8ce74a
|
changeset |
files
|
| Sat, 14 Aug 2021 15:18:48 +0200 |
wneuper |
update TODO.md according to cf.a56ac28081a9
|
changeset |
files
|
| Sat, 14 Aug 2021 13:52:23 +0200 |
wneuper |
note on Thm.get_name_hint
|
changeset |
files
|
| Wed, 11 Aug 2021 11:54:07 +0200 |
wneuper |
note on Context.theory_name vs. Context.theory_long_name
|
changeset |
files
|
| Tue, 10 Aug 2021 19:05:59 +0200 |
wneuper |
make Integrate.add_new_c a proper constant
|
changeset |
files
|
| Tue, 10 Aug 2021 13:40:03 +0200 |
wneuper |
tuned
|
changeset |
files
|
| Tue, 10 Aug 2021 13:38:03 +0200 |
wneuper |
comment on filenames *-def.sml, analogous to cf. e587c45cae0f
|
changeset |
files
|
| Tue, 10 Aug 2021 12:58:33 +0200 |
wneuper |
explain "KEStore_Elems.add_thes" in TODO.md
|
changeset |
files
|
| Tue, 10 Aug 2021 12:56:06 +0200 |
wneuper |
cleanup MethodC.prep_input that used a different theory
|
changeset |
files
|
| Tue, 10 Aug 2021 11:55:24 +0200 |
wneuper |
tuned
|
changeset |
files
|
| Tue, 10 Aug 2021 11:54:12 +0200 |
wneuper |
relate note on planned improvements (cf.03dea0a179d0) to TODO.md
|
changeset |
files
|
| Tue, 10 Aug 2021 11:29:33 +0200 |
wneuper |
remove items already done
|
changeset |
files
|
| Tue, 10 Aug 2021 11:01:18 +0200 |
wneuper |
eliminate ThyC.to_ctxt, use Proof_Context.init_global inline
|
changeset |
files
|
| Tue, 10 Aug 2021 10:27:15 +0200 |
wneuper |
note on CS c7b1a99bcfd2 , \<^ML>?Thy_Info.get_theory?
|
changeset |
files
|
| Tue, 10 Aug 2021 09:43:07 +0200 |
wneuper |
complete replacement of Rule.Thm/Eval by \<^rule_thm> and \<^rule_eval> in src/*
|
changeset |
files
|
| Mon, 09 Aug 2021 14:20:20 +0200 |
wneuper |
eliminate ThyC.to_ctxt done except 1 error
|
changeset |
files
|
| Mon, 09 Aug 2021 11:19:25 +0200 |
wneuper |
remove TOODOOs
|
changeset |
files
|
| Sun, 08 Aug 2021 15:21:33 +0200 |
wneuper |
repair fun is_ratpolyexp
|
changeset |
files
|
| Fri, 06 Aug 2021 18:27:05 +0200 |
wneuper |
cleanup files on GCD/gcd
|
changeset |
files
|
| Fri, 06 Aug 2021 12:09:06 +0200 |
wneuper |
repair fun order overwritten by previous tests
|
changeset |
files
|
| Fri, 06 Aug 2021 11:13:20 +0200 |
wneuper |
repair (ad-hoc) order in PolyMinus.thy, finished
|
changeset |
files
|
| Thu, 05 Aug 2021 18:05:28 +0200 |
wneuper |
repair (ad-hoc) order in PolyMinus.thy
|
changeset |
files
|
| Wed, 04 Aug 2021 17:34:47 +0200 |
wneuper |
remove comments from (*ML_file ?..?*) in Test_Isac_Short.thy
|
changeset |
files
|
| Wed, 04 Aug 2021 10:15:55 +0200 |
wneuper |
repair test broken with "repair addition with zero polynomial"
|
changeset |
files
|
| Tue, 03 Aug 2021 19:40:02 +0200 |
wneuper |
outcomment test broken with "repair cancellation with zero polynomial"
|
changeset |
files
|
| Tue, 03 Aug 2021 19:16:27 +0200 |
wneuper |
repair cancellation with zero polynomial
|
changeset |
files
|
| Mon, 02 Aug 2021 15:30:41 +0200 |
wneuper |
tuned
|
changeset |
files
|
| Mon, 02 Aug 2021 15:27:47 +0200 |
wneuper |
tuned
|
changeset |
files
|
| Mon, 02 Aug 2021 15:25:49 +0200 |
wneuper |
reapir minus_mult_left, many tests work again
|
changeset |
files
|
| Mon, 02 Aug 2021 11:38:40 +0200 |
wneuper |
repair thm real_mult_minus1_sym; many newly broken tests
|
changeset |
files
|
| Sun, 01 Aug 2021 14:39:03 +0200 |
wneuper |
repair ord_make_polynomial_in, est/../integrate.sml works again
|
changeset |
files
|
| Tue, 27 Jul 2021 12:32:43 +0200 |
wneuper |
//test/../diff.sml works again
|
changeset |
files
|
| Tue, 27 Jul 2021 11:21:14 +0200 |
wneuper |
revert previous changeset
|
changeset |
files
|
| Tue, 20 Jul 2021 14:37:56 +0200 |
wneuper |
//reduce the number of TermC.parse*; "//"means: tests broken .
|
changeset |
files
|
| Mon, 19 Jul 2021 18:39:02 +0200 |
wneuper |
eliminate type float; was an early attempt overrun by Isabelle
|
changeset |
files
|
| Mon, 19 Jul 2021 18:29:46 +0200 |
wneuper |
cleanup after "eliminate ThmC.numerals_to_Free"
|
changeset |
files
|