| Wed, 11 Jan 2023 11:38:01 +0100 |
eliminate use of Thy_Info 12: TermC partially
|
file | diff | annotate |
| Sun, 08 Jan 2023 10:30:58 +0100 |
eliminate use of Thy_Info 3> improved LItool.tac_from_prog
|
file | diff | annotate |
| Fri, 06 Jan 2023 11:32:57 +0100 |
eliminate thy-hierarchy 5, end: remove Thy_Write
|
file | diff | annotate |
| Thu, 22 Dec 2022 10:27:12 +0100 |
make Minisubplb/800-append-on-Frm.sml independent from Thy_Info
|
file | diff | annotate |
| Thu, 15 Dec 2022 13:03:51 +0100 |
proper indication of error-msg "Wrong descriptor" in problem/method
|
file | diff | annotate |
| Thu, 08 Dec 2022 10:33:27 +0100 |
tuned files, Test_Isac.thy works
|
file | diff | annotate |
| Sun, 04 Dec 2022 16:48:06 +0100 |
make Minisubplb/300-init-subpbl-NEXT_STEP.sml independent from Thy_Info
|
file | diff | annotate |
| Thu, 24 Nov 2022 18:07:17 +0100 |
follow-up Makarius #3: reorganise parse for proper error-reporting in problem/method
|
file | diff | annotate |
| Wed, 16 Nov 2022 10:29:52 +0100 |
make Minisubplb/200-start-method independent #2: Tactic.Rewrite_Set partially
|
file | diff | annotate |
| Thu, 10 Nov 2022 14:25:38 +0100 |
make Minisubplb/200-start-method independent from Thy_Info #1
|
file | diff | annotate |
| Mon, 07 Nov 2022 19:58:01 +0100 |
rename KEstore_Elems to Know_Store
|
file | diff | annotate |
| Tue, 25 Oct 2022 16:15:47 +0200 |
follow up 6: eliminate use of Thy_Info.get_theory, part 1
|
file | diff | annotate |
| Thu, 20 Oct 2022 10:23:38 +0200 |
followup 6a: tests run from @{context} without sessions
|
file | diff | annotate |
| Wed, 19 Oct 2022 10:43:04 +0200 |
eliminate term2str in src, Prog_Tac.*_adapt_to_type
|
file | diff | annotate |
| Fri, 07 Oct 2022 20:46:48 +0200 |
follow up 3: MethodC.adapt_to_typ on loading by CalcTree, CalcTreeTEST
|
file | diff | annotate |
| Mon, 26 Sep 2022 10:57:53 +0200 |
follow up 2: Problem.adapt_to_typ on loading by CalcTree, CalcTreeTEST
|
file | diff | annotate |
| Mon, 22 Aug 2022 11:26:20 +0200 |
cleanup test for: push ctxt through LI
|
file | diff | annotate |
| Sun, 21 Aug 2022 11:22:04 +0200 |
//prepare test 3 for: push ctxt through LI (only CAS_Cmd not OK)
|
file | diff | annotate |
| Fri, 05 Aug 2022 12:30:16 +0200 |
push Proof.context through Eval.adhoc_thm
|
file | diff | annotate |
| Thu, 04 Aug 2022 12:48:37 +0200 |
polish naming in Rewrite_Order
|
file | diff | annotate |
| Tue, 26 Jul 2022 22:01:40 +0200 |
test for stepwise input to ?Example?
|
file | diff | annotate |
| Sun, 19 Jun 2022 16:55:13 +0200 |
shifts tests to VSCode_Example.thy, vscode-example.sml
|
file | diff | annotate |
| Sat, 18 Jun 2022 12:34:29 +0200 |
adapth thy to Demo_Example
|
file | diff | annotate |
| Thu, 26 May 2022 12:44:51 +0200 |
unify parse 6': TermC.parse eliminated, Test_Isac ok
|
file | diff | annotate |
| Mon, 27 Sep 2021 20:24:24 +0200 |
cleanup; all relevant tests work again
|
file | diff | annotate |
| Tue, 14 Sep 2021 12:22:57 +0200 |
\\adopt Isabelles calculation of numerals, some cases are missing
|
file | diff | annotate |
| Mon, 13 Sep 2021 16:01:48 +0200 |
cleanup TOODOOs from eliminate ThmC.numerals_to_Free
|
file | diff | annotate |
| Mon, 13 Sep 2021 15:42:43 +0200 |
/----- eliminate ThmC.numerals_to_Free finished: all relevant tests work again
|
file | diff | annotate |
| Mon, 13 Sep 2021 15:33:46 +0200 |
relevant test/../biegelinie-4.sml works again
|
file | diff | annotate |
| Sun, 12 Sep 2021 16:18:03 +0200 |
recover test/../biegelinie-1.sml
|
file | diff | annotate |
| Sun, 12 Sep 2021 15:53:36 +0200 |
cleanup test/../eqsystem-2.sml
|
file | diff | annotate |
| Sun, 12 Sep 2021 15:40:15 +0200 |
cleanup
|
file | diff | annotate |
| Mon, 23 Aug 2021 14:24:06 +0200 |
repair rule-set reduce_0_1_2
|
file | diff | annotate |
| Sun, 22 Aug 2021 09:43:43 +0200 |
improvement in Rational.thy makes several testfiles run, breaks one.
|
file | diff | annotate |
| Wed, 18 Aug 2021 20:34:41 +0200 |
replace is_const with is_num, ERROR removed
|
file | diff | annotate |
| Wed, 18 Aug 2021 11:35:24 +0200 |
repair test/../root.sml, diff.sml; outcomment NEW errors TOODOO.1
|
file | diff | annotate |
| Fri, 06 Aug 2021 18:27:05 +0200 |
cleanup files on GCD/gcd
|
file | diff | annotate |
| Wed, 04 Aug 2021 17:34:47 +0200 |
remove comments from (*ML_file ?..?*) in Test_Isac_Short.thy
|
file | diff | annotate |
| Tue, 03 Aug 2021 19:40:02 +0200 |
outcomment test broken with "repair cancellation with zero polynomial"
|
file | diff | annotate |
| Tue, 03 Aug 2021 19:16:27 +0200 |
repair cancellation with zero polynomial
|
file | diff | annotate |
| Mon, 02 Aug 2021 15:25:49 +0200 |
reapir minus_mult_left, many tests work again
|
file | diff | annotate |
| Mon, 02 Aug 2021 11:38:40 +0200 |
repair thm real_mult_minus1_sym; many newly broken tests
|
file | diff | annotate |
| Sun, 01 Aug 2021 14:39:03 +0200 |
repair ord_make_polynomial_in, est/../integrate.sml works again
|
file | diff | annotate |
| Tue, 27 Jul 2021 12:32:43 +0200 |
//test/../diff.sml works again
|
file | diff | annotate |
| Tue, 27 Jul 2021 11:21:14 +0200 |
revert previous changeset
|
file | diff | annotate |
| Tue, 20 Jul 2021 14:37:56 +0200 |
//reduce the number of TermC.parse*; "//"means: tests broken .
|
file | diff | annotate |
| Mon, 19 Jul 2021 18:29:46 +0200 |
cleanup after "eliminate ThmC.numerals_to_Free"
|
file | diff | annotate |
| Mon, 19 Jul 2021 17:29:35 +0200 |
introduce ALL valid const_name in test/*
|
file | diff | annotate |
| Sun, 18 Jul 2021 16:20:32 +0200 |
eliminate ThmC.numerals_to_Free: Test_Isac_Short.thy works with TOODOO s
|
file | diff | annotate |
| Sat, 17 Jul 2021 14:05:28 +0200 |
replace "-*" by "- *" for numerals "*" in test/*
|
file | diff | annotate |
| Thu, 15 Jul 2021 20:09:44 +0200 |
cleanup Test_Isac_Short.thy
|
file | diff | annotate |
| Thu, 15 Jul 2021 20:02:16 +0200 |
rewrite.sml + poly.sml + rational.sml + polyminus.sml: ok
|
file | diff | annotate |
| Thu, 15 Jul 2021 14:10:18 +0200 |
ewrite.sml + poly.sml + rational.sml: ok, repair rewrite-orders
|
file | diff | annotate |
| Sat, 03 Jul 2021 16:21:07 +0200 |
//test/../rewrite.sml,poly.sml WORK
|
file | diff | annotate |
| Tue, 01 Jun 2021 15:41:23 +0200 |
Test_Some.thy with looping ML<>
|
file | diff | annotate |
| Fri, 07 May 2021 13:23:24 +0200 |
discontiune writing to file, keep XML hierarchies of MethodC and Model_Pattern,
|
file | diff | annotate |
| Tue, 27 Apr 2021 18:09:22 +0200 |
eliminate "handle _ => ..." from Rewrite.rewrite
|
file | diff | annotate |
| Thu, 22 Apr 2021 21:34:20 +0200 |
purge XML output from pbl- and met-hierarchies, coarse part
|
file | diff | annotate |
| Thu, 22 Apr 2021 16:49:41 +0200 |
purge code for input to Kernel
|
file | diff | annotate |
| Thu, 22 Apr 2021 16:21:23 +0200 |
purge code for theory hierarchy
|
file | diff | annotate |