| 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 |
| Wed, 21 Apr 2021 10:04:17 +0200 |
done TODO caused by ac7426ab0491
|
file | diff | annotate |
| Tue, 20 Apr 2021 16:58:44 +0200 |
replace power ^^^ by \<up>
|
file | diff | annotate |
| Mon, 19 Apr 2021 20:44:18 +0200 |
less ambitious ML_print_depth: 20 instead of 999;
|
file | diff | annotate |
| Mon, 19 Apr 2021 20:33:04 +0200 |
obsolete;
|
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 |
| Mon, 19 Apr 2021 15:02:00 +0200 |
long identifiers for occurences in test/../termC.sml
|
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 18:30:31 +0200 |
proper test sessions, but with remaining failures;
|
file | diff | annotate |
| Fri, 16 Apr 2021 22:29:23 +0200 |
prefer symbolic directories $ISABELLE_ISAC and $ISABELLE_ISAC_TEST, instead of re-using ~~ for $ISABELLE_HOME;
|
file | diff | annotate |
| Sun, 04 Apr 2021 12:29:42 +0200 |
separate session Specify
|
file | diff | annotate |
| Sun, 17 Jan 2021 15:25:27 +0100 |
step 5.1: separate code for keyword Example to preliminary file
|
file | diff | annotate |
| Wed, 09 Dec 2020 14:37:10 +0100 |
step 3.2: prep.data for start of specify-phase
|
file | diff | annotate |
| Wed, 09 Dec 2020 14:22:24 +0100 |
adopt new theory identifier also in comments
|
file | diff | annotate |
| Mon, 07 Dec 2020 17:39:21 +0100 |
step 2 of integration: interrupted
|
file | diff | annotate |
| Mon, 26 Oct 2020 13:52:26 +0100 |
copy Outer_Syntax.command..spark_open as model for Isac Calculation
|
file | diff | annotate |
| Thu, 22 Oct 2020 15:40:41 +0200 |
complete imports to Test_Isac*
|
file | diff | annotate |
| Wed, 07 Oct 2020 10:02:42 +0200 |
/----- finish update Isabelle2019 --> Isabelle2020 for Test_Isac_Short.thy
|
file | diff | annotate |
| Wed, 23 Sep 2020 14:54:38 +0200 |
final isabisac19 on Isabelle2019
|
file | diff | annotate |
| Sun, 02 Aug 2020 12:32:34 +0200 |
shift code from Test_Parse_Isac to src/
|
file | diff | annotate |