| 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
|
| Mon, 19 Jul 2021 17:29:35 +0200 |
wneuper |
introduce ALL valid const_name in test/*
|
changeset |
files
|
| Mon, 19 Jul 2021 15:34:54 +0200 |
wneuper |
ALL const_name replaces (others cannot be replaced)
|
changeset |
files
|
| Sun, 18 Jul 2021 21:19:25 +0200 |
wneuper |
Test_Some.the works, too
|
changeset |
files
|
| Sun, 18 Jul 2021 21:15:21 +0200 |
wneuper |
Test_Isac_Short.thy, Test_Some.the work on new src, new TOODOOs
|
changeset |
files
|
| Sun, 18 Jul 2021 18:30:09 +0200 |
wneuper |
Test_Isac_Short.thy works again (ndefined ML antiquotation: "rule_thm_sym", "rule_thm")
|
changeset |
files
|
| Sun, 18 Jul 2021 18:15:27 +0200 |
wneuper |
merged
|
changeset |
files
|
| Sun, 18 Jul 2021 16:20:32 +0200 |
wneuper |
eliminate ThmC.numerals_to_Free: Test_Isac_Short.thy works with TOODOO s
|
changeset |
files
|
| Sat, 17 Jul 2021 14:05:28 +0200 |
wneuper |
replace "-*" by "- *" for numerals "*" in test/*
|
changeset |
files
|
| Fri, 16 Jul 2021 07:45:06 +0200 |
wneuper |
separate poly-1 /-2.sml
|
changeset |
files
|
| Fri, 16 Jul 2021 06:57:34 +0200 |
wneuper |
separate rational-1 /-2.sml
|
changeset |
files
|
| Thu, 15 Jul 2021 20:09:44 +0200 |
wneuper |
cleanup Test_Isac_Short.thy
|
changeset |
files
|
| Thu, 15 Jul 2021 20:02:16 +0200 |
wneuper |
rewrite.sml + poly.sml + rational.sml + polyminus.sml: ok
|
changeset |
files
|
| Thu, 15 Jul 2021 14:10:18 +0200 |
wneuper |
ewrite.sml + poly.sml + rational.sml: ok, repair rewrite-orders
|
changeset |
files
|
| Tue, 13 Jul 2021 15:28:43 +0200 |
wneuper |
Test_Some.thy + rewrite.sml + poly.sml + rational.sml: ok
|
changeset |
files
|
| Tue, 13 Jul 2021 10:43:21 +0200 |
wneuper |
Test_Some.thy + rewrite.sml + poly.sml ok: improve eval_is_atom
|
changeset |
files
|
| Tue, 13 Jul 2021 09:49:45 +0200 |
wneuper |
Test_Some.thy + rewrite.sml + poly.sml ok: shift code Test_Some.thy --> Poly.thy
|
changeset |
files
|
| Tue, 13 Jul 2021 08:52:35 +0200 |
wneuper |
Test_Some.thy + rewrite.sml + poly.sml ok: real_mult_minus1_sym works with is_atom
|
changeset |
files
|
| Mon, 12 Jul 2021 17:21:37 +0200 |
wneuper |
Test_Some.thy + rewrite.sml + poly.sml ok: repair poly_of_term
|
changeset |
files
|
| Sat, 03 Jul 2021 16:21:07 +0200 |
wneuper |
//test/../rewrite.sml,poly.sml WORK
|
changeset |
files
|
| Tue, 01 Jun 2021 15:41:23 +0200 |
wneuper |
Test_Some.thy with looping ML<>
|
changeset |
files
|
| Mon, 21 Jun 2021 22:08:01 +0200 |
wenzelm |
updated TODO;
|
changeset |
files
|
| Mon, 21 Jun 2021 21:59:10 +0200 |
wenzelm |
updated TODO;
|
changeset |
files
|
| Mon, 21 Jun 2021 21:53:23 +0200 |
wenzelm |
Isar command 'cas' as front-end for KEStore_Elems.add_cas, without change of semantics;
|
changeset |
files
|
| Mon, 21 Jun 2021 20:06:12 +0200 |
wenzelm |
Isar command 'calculation' as front-end for KEStore_Elems.add_calcs, without change of semantics;
|
changeset |
files
|
| Mon, 21 Jun 2021 16:18:27 +0200 |
wenzelm |
more antiquotations, without change of semantics;
|
changeset |
files
|
| Mon, 21 Jun 2021 15:50:58 +0200 |
wenzelm |
updated TODO;
|
changeset |
files
|
| Mon, 21 Jun 2021 15:42:53 +0200 |
wenzelm |
proper formal names for consts/types, *with* change of semantics;
|
changeset |
files
|
| Mon, 21 Jun 2021 15:36:09 +0200 |
wenzelm |
more antiquotations for Isabelle/HOL consts/types, without change of semantics;
|
changeset |
files
|
| Mon, 21 Jun 2021 14:39:52 +0200 |
wenzelm |
proper UTF-8;
|
changeset |
files
|
| Sun, 20 Jun 2021 16:30:56 +0200 |
wenzelm |
tuned --- adapted to problem.sml;
|
changeset |
files
|
| Sun, 20 Jun 2021 16:26:18 +0200 |
wenzelm |
Isar command 'problem' as combination of KEStore_Elems.add_pbts + Problem.prep_import, without change of semantics;
|
changeset |
files
|
| Sun, 20 Jun 2021 12:45:03 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 16 Jun 2021 12:56:09 +0200 |
wenzelm |
updated TODO;
|
changeset |
files
|
| Tue, 15 Jun 2021 22:24:20 +0200 |
wenzelm |
Isar command 'method' as combination of KEStore_Elems.add_mets + MethodC.prep_import, without change of semantics;
|
changeset |
files
|
| Sat, 12 Jun 2021 18:33:15 +0200 |
wenzelm |
updated TODO;
|
changeset |
files
|
| Sat, 12 Jun 2021 18:30:31 +0200 |
wenzelm |
updated TODO;
|
changeset |
files
|
| Sat, 12 Jun 2021 18:30:17 +0200 |
wenzelm |
removed junk;
|
changeset |
files
|
| Sat, 12 Jun 2021 18:27:30 +0200 |
wenzelm |
use more antiquotations;
|
changeset |
files
|
| Sat, 12 Jun 2021 18:22:07 +0200 |
wenzelm |
use more antiquotations;
|
changeset |
files
|
| Sat, 12 Jun 2021 18:06:27 +0200 |
wenzelm |
use more antiquotations;
|
changeset |
files
|
| Sat, 12 Jun 2021 14:29:10 +0200 |
wenzelm |
ML antiquotations for Rule.Thm, with special treatment of symmetric rule;
|
changeset |
files
|
| Sat, 12 Jun 2021 14:27:03 +0200 |
wenzelm |
updated TODO;
|
changeset |
files
|
| Fri, 11 Jun 2021 11:49:34 +0200 |
wenzelm |
ML antiquotation for formally checked Rule.Eval;
|
changeset |
files
|
| Thu, 10 Jun 2021 17:06:32 +0200 |
wenzelm |
tuned signatures (SML'97 allows type abbreviations);
|
changeset |
files
|
| Thu, 10 Jun 2021 12:53:02 +0200 |
wenzelm |
more TODO;
|
changeset |
files
|
| Thu, 10 Jun 2021 12:48:50 +0200 |
wenzelm |
clarified theory context: avoid global "val thy = ..." hanging around (left-over from Isabelle2005), which is apt to various pitfalls;
|
changeset |
files
|
| Thu, 10 Jun 2021 12:23:57 +0200 |
wenzelm |
clarified theory context: from current command instead of earlier state;
|
changeset |
files
|