| Mon, 09 Aug 2021 14:20:20 +0200 |
eliminate ThyC.to_ctxt done except 1 error
|
file | diff | annotate |
| Mon, 09 Aug 2021 11:19:25 +0200 |
remove TOODOOs
|
file | diff | annotate |
| Tue, 03 Aug 2021 19:16:27 +0200 |
repair cancellation with zero polynomial
|
file | diff | annotate |
| Mon, 02 Aug 2021 15:30:41 +0200 |
tuned
|
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 21:19:25 +0200 |
Test_Some.the works, too
|
file | diff | annotate |
| Sun, 18 Jul 2021 21:15:21 +0200 |
Test_Isac_Short.thy, Test_Some.the work on new src, new TOODOOs
|
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 |
| 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 |
| Tue, 13 Jul 2021 15:28:43 +0200 |
Test_Some.thy + rewrite.sml + poly.sml + rational.sml: ok
|
file | diff | annotate |
| Tue, 13 Jul 2021 10:43:21 +0200 |
Test_Some.thy + rewrite.sml + poly.sml ok: improve eval_is_atom
|
file | diff | annotate |
| Tue, 13 Jul 2021 09:49:45 +0200 |
Test_Some.thy + rewrite.sml + poly.sml ok: shift code Test_Some.thy --> Poly.thy
|
file | diff | annotate |
| Tue, 13 Jul 2021 08:52:35 +0200 |
Test_Some.thy + rewrite.sml + poly.sml ok: real_mult_minus1_sym works with is_atom
|
file | diff | annotate |
| Mon, 12 Jul 2021 17:21:37 +0200 |
Test_Some.thy + rewrite.sml + poly.sml ok: repair poly_of_term
|
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 |
| Tue, 27 Apr 2021 18:09:22 +0200 |
eliminate "handle _ => ..." from Rewrite.rewrite
|
file | diff | annotate |
| Mon, 26 Apr 2021 14:16:35 +0200 |
prep.eliminate "handle _ => ..." from Rewrite.rewrite
|
file | diff | annotate |
| Sun, 25 Apr 2021 12:49:37 +0200 |
cleanup remaining ^^^ in comments, finished (?)
|
file | diff | annotate |
| Sat, 24 Apr 2021 15:59:54 +0200 |
purge XML output from pbl- and met-hierarchies, finished
|
file | diff | annotate |
| Mon, 19 Apr 2021 19:55:31 +0200 |
no \<^isac_test> guard for test material: thus the Prover IDE does not have to switch the option "isac_test";
|
file | diff | annotate |
| Sun, 18 Apr 2021 23:37:59 +0200 |
conditional compilation via system option "isac_test" and antiquotation \<^isac_test>CARTOUCHE:
|
file | diff | annotate |
| Sun, 18 Apr 2021 22:27:43 +0200 |
retain thm name_hint: more close imitation of former oracles (amending 07bf9c88f2c3, afcde49beb65);
|
file | diff | annotate |
| Sun, 18 Apr 2021 18:56:43 +0200 |
2 broken tests in Test_Some.thy, thus Test_Isac_Short.thy ok
|
file | diff | annotate |
| Fri, 22 Jan 2021 16:03:15 +0100 |
step 5.5: for devel. make test-example independent from session Isac
|
file | diff | annotate |
| Fri, 22 Jan 2021 11:27:47 +0100 |
step 5.2: shift tests from Test_Parse_Isac.thy to test/../parseC.sml
|
file | diff | annotate |
| Sun, 17 Jan 2021 13:16:25 +0100 |
step 5: cleanup previous steps; status quo
|
file | diff | annotate |
| Thu, 17 Dec 2020 11:45:12 +0100 |
tuned
|
file | diff | annotate |
| Thu, 17 Dec 2020 11:42:18 +0100 |
step 4.3: parse Problem + Specification; this is inappropriate..
|
file | diff | annotate |
| Thu, 17 Dec 2020 11:22:53 +0100 |
cleanup
|
file | diff | annotate |
| Tue, 15 Dec 2020 15:10:38 +0100 |
step 4: use Naproche as a model for checking input
|
file | diff | annotate |
| Wed, 09 Dec 2020 14:37:10 +0100 |
step 3.2: prep.data for start of specify-phase
|
file | diff | annotate |
| Tue, 08 Dec 2020 17:10:18 +0100 |
step 3.1: transfer data from Example to Problem
|
file | diff | annotate |
| Tue, 08 Dec 2020 13:39:52 +0100 |
step 3: use spark_vc as model for starting work on SpecificationC.T
|
file | diff | annotate |
| Sat, 28 Nov 2020 17:47:43 +0100 |
Test_Some Example reports no error and no <Output>
|
file | diff | annotate |
| Fri, 27 Nov 2020 18:19:04 +0100 |
Test_Some Example still reports the result from g_c_d
|
file | diff | annotate |
| Sun, 14 Jun 2020 15:39:55 +0200 |
unify code (and replace Specify.by_tactic_input' by Specify.by_Add_)
|
file | diff | annotate |
| Fri, 12 Jun 2020 11:41:57 +0200 |
unify signatures of Step's (Step_Specify.by_tactic_input)
|
file | diff | annotate |
| Mon, 01 Jun 2020 16:11:05 +0200 |
remove Specify.find_next_step'
|
file | diff | annotate |
| Mon, 01 Jun 2020 11:49:37 +0200 |
unify code
|
file | diff | annotate |
| Sat, 30 May 2020 15:20:22 +0200 |
cleanup code after resolve hacks
|
file | diff | annotate |
| Sat, 30 May 2020 14:10:58 +0200 |
resolve hacks finished
|
file | diff | annotate |
| Fri, 29 May 2020 12:43:41 +0200 |
[errors 4, Test_Isac_Short] resolve hacks, part 4: reapired O_Model.complete_for
|
file | diff | annotate |
| Thu, 28 May 2020 13:24:47 +0200 |
[errors 3, Short] resolve hacks, part 3: remove hack in Step_Specify.by_tactic
|
file | diff | annotate |
| Thu, 28 May 2020 12:52:25 +0200 |
resolve hacks, part 2: Specify.find_next_step, Specify.by_tactic_input
|
file | diff | annotate |
| Wed, 27 May 2020 16:20:06 +0200 |
now Test_Some is OK with NEW code
|
file | diff | annotate |
| Wed, 27 May 2020 16:14:14 +0200 |
resolve hacks, part 1: NEW O_Model.complete_for_from
|
file | diff | annotate |
| Wed, 27 May 2020 13:42:37 +0200 |
Test_Isac_Short OK with OLD code, Test_Some OK with NEW
|
file | diff | annotate |
| Tue, 26 May 2020 11:53:43 +0200 |
prep.resolve hacks introduced with funpack, part 4
|
file | diff | annotate |
| Mon, 25 May 2020 16:52:38 +0200 |
prep.resolve hacks introduced with funpack, part 3
|
file | diff | annotate |
| Mon, 25 May 2020 11:14:51 +0200 |
prep.resolve hacks introduced with funpack, part 2
|
file | diff | annotate |