| Wed, 01 Jun 2022 09:28:56 +0200 |
wneuper |
Calculation 4: refine representations of Demo_Example
|
changeset |
files
|
| Tue, 31 May 2022 19:24:28 +0200 |
wneuper |
Calculation 3': Demo_Example stores values to Theory_Data
|
changeset |
files
|
| Tue, 31 May 2022 17:33:02 +0200 |
wneuper |
Calculation 3: Demo_Example stored in Theory_Data
|
changeset |
files
|
| Tue, 31 May 2022 16:21:22 +0200 |
wneuper |
cleanup
|
changeset |
files
|
| Tue, 31 May 2022 11:00:15 +0200 |
wneuper |
cleanup
|
changeset |
files
|
| Tue, 31 May 2022 10:17:11 +0200 |
wneuper |
cleanup
|
changeset |
files
|
| Tue, 31 May 2022 09:57:15 +0200 |
wneuper |
Calculation 2: Demo_Example without ML code
|
changeset |
files
|
| Tue, 31 May 2022 09:36:02 +0200 |
wneuper |
Calculation 1''': remove test-code from previous changeset 1c8263e775d4
|
changeset |
files
|
| Tue, 31 May 2022 09:16:12 +0200 |
wneuper |
Calculation 1'': ERROR in Demo_Example.thy, questions in TODO.md
|
changeset |
files
|
| Sun, 29 May 2022 19:05:14 +0200 |
wneuper |
Calculation 1': include Demo_Example into build
|
changeset |
files
|
| Sun, 29 May 2022 19:00:35 +0200 |
wneuper |
Calculation 1: minimal changes in code + application
|
changeset |
files
|
| Sun, 29 May 2022 12:17:09 +0200 |
wneuper |
start Calculation by use of Makarius' "problem" as boilerplate + add files
|
changeset |
files
|
| Sun, 29 May 2022 11:34:05 +0200 |
wneuper |
cleanup
|
changeset |
files
|
| Sun, 29 May 2022 11:27:34 +0200 |
wneuper |
start Calculation by use of Makarius' "problem" as boilerplate
|
changeset |
files
|
| Fri, 27 May 2022 17:19:01 +0200 |
wneuper |
tuned
|
changeset |
files
|
| Fri, 27 May 2022 17:14:49 +0200 |
wneuper |
tuned
|
changeset |
files
|
| Fri, 27 May 2022 15:12:54 +0200 |
wneuper |
replace literals with constants
|
changeset |
files
|
| Fri, 27 May 2022 12:07:55 +0200 |
wneuper |
type check at init of Problem appears correct
|
changeset |
files
|
| Thu, 26 May 2022 12:53:13 +0200 |
wneuper |
tuned
|
changeset |
files
|
| Thu, 26 May 2022 12:45:00 +0200 |
wneuper |
merged
|
changeset |
files
|
| Thu, 26 May 2022 12:44:51 +0200 |
wneuper |
unify parse 6': TermC.parse eliminated, Test_Isac ok
|
changeset |
files
|
| Wed, 25 May 2022 10:37:35 +0200 |
wneuper |
unify parse 6: TermC.parse eliminated, Test_Isac_Short ok
|
changeset |
files
|
| Tue, 24 May 2022 16:47:31 +0200 |
wneuper |
unify parse 5': improved get_ctxt for appendFormula and CAS-cmd
|
changeset |
files
|
| Tue, 24 May 2022 12:57:47 +0200 |
wneuper |
unify parse 5: for appendFormula and CAS-cmd
|
changeset |
files
|
| Mon, 23 May 2022 18:23:25 +0200 |
wneuper |
disentangle isa and isa2
|
changeset |
files
|
| Mon, 23 May 2022 15:18:27 +0200 |
wneuper |
resume development
|
changeset |
files
|
| Tue, 16 Nov 2021 18:29:23 +0100 |
wneuper |
tuned
|
changeset |
files
|
| Tue, 16 Nov 2021 18:26:57 +0100 |
wneuper |
unify parse 4: eliminate parse, simple cases
|
changeset |
files
|
| Wed, 29 Sep 2021 19:34:32 +0200 |
wneuper |
unify parse 3: eliminate parseN
|
changeset |
files
|
| Wed, 29 Sep 2021 19:26:12 +0200 |
wneuper |
unify parse 2: eliminate parseold
|
changeset |
files
|
| Wed, 29 Sep 2021 18:56:38 +0200 |
wneuper |
unify parse 1: reorder defs
|
changeset |
files
|
| Mon, 27 Sep 2021 20:24:24 +0200 |
wneuper |
cleanup; all relevant tests work again
|
changeset |
files
|
| Mon, 27 Sep 2021 13:17:52 +0200 |
wneuper |
tuned
|
changeset |
files
|
| Mon, 27 Sep 2021 13:14:09 +0200 |
wneuper |
simp rules for realpow appear complete
|
changeset |
files
|
| Sun, 26 Sep 2021 20:58:57 +0200 |
wneuper |
another simp rule missing; lemma realpow_uminus_simps fails.
|
changeset |
files
|
| Sat, 25 Sep 2021 21:41:51 +0200 |
wenzelm |
more simp rules: 1 is another special case, so (- 1) needs to be treated separately;
|
changeset |
files
|
| Sat, 25 Sep 2021 13:54:06 +0200 |
wneuper |
\\ uncovered corner case of realpow: (- 1) ? 2
|
changeset |
files
|
| Fri, 24 Sep 2021 14:18:10 +0200 |
wenzelm |
proper simp_ctxt;
|
changeset |
files
|
| Thu, 23 Sep 2021 13:47:16 +0200 |
wneuper |
\\ realpow is not handled by present Simplifier.rewrite simp_ctxt
|
changeset |
files
|
| Thu, 16 Sep 2021 17:23:54 +0200 |
wenzelm |
separate realpow constant, with additional cases not covered by Transcendental.powr;
|
changeset |
files
|
| Thu, 16 Sep 2021 12:23:57 +0200 |
wenzelm |
adapted to Isabelle/c645d973f881;
|
changeset |
files
|
| Thu, 16 Sep 2021 11:47:03 +0200 |
wenzelm |
follow Isabelle repository;
|
changeset |
files
|
| Tue, 14 Sep 2021 16:06:42 +0200 |
wneuper |
\\adopt Isabelles calculation of numerals, "(- 1) ? 2" still missing
|
changeset |
files
|
| Tue, 14 Sep 2021 12:22:57 +0200 |
wneuper |
\\adopt Isabelles calculation of numerals, some cases are missing
|
changeset |
files
|
| Mon, 13 Sep 2021 16:01:48 +0200 |
wneuper |
cleanup TOODOOs from eliminate ThmC.numerals_to_Free
|
changeset |
files
|
| Mon, 13 Sep 2021 15:42:43 +0200 |
wneuper |
/----- eliminate ThmC.numerals_to_Free finished: all relevant tests work again
|
changeset |
files
|
| Mon, 13 Sep 2021 15:33:46 +0200 |
wneuper |
relevant test/../biegelinie-4.sml works again
|
changeset |
files
|
| Mon, 13 Sep 2021 15:31:50 +0200 |
wneuper |
investigate error from before CS "eliminate ThmC.numerals_to_Free"
|
changeset |
files
|
| 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
|