Tue, 16 Aug 2022 12:21:21 +0200 |
prepare src for: push ctxt throught Lucas-Interpretation
|
file | diff | annotate |
Sat, 06 Aug 2022 18:50:43 +0200 |
push Proof.context through Derive.steps, note HACK
|
file | diff | annotate |
Sat, 06 Aug 2022 18:00:33 +0200 |
push Proof.context through Error_Pattern.fill_form
|
file | diff | annotate |
Sat, 06 Aug 2022 17:36:59 +0200 |
push Proof.context through Error_Pattern.check_for
|
file | diff | annotate |
Sat, 06 Aug 2022 15:57:46 +0200 |
review TODO.md: eliminate get_thes is easier than anticipated
|
file | diff | annotate |
Sat, 06 Aug 2022 15:02:55 +0200 |
eliminate union_overwrite and use standard namespace merge
|
file | diff | annotate |
Sat, 06 Aug 2022 10:45:24 +0200 |
reorder TODO.md priorities
|
file | diff | annotate |
Fri, 05 Aug 2022 12:30:16 +0200 |
push Proof.context through Eval.adhoc_thm
|
file | diff | annotate |
Fri, 05 Aug 2022 11:38:10 +0200 |
improve error-msg of Problem.from_store, MethodC.from_store
|
file | diff | annotate |
Fri, 05 Aug 2022 08:45:37 +0200 |
finish Calc_Binop, add signature EXAMPLE
|
file | diff | annotate |
Thu, 04 Aug 2022 16:48:37 +0200 |
add structure Calc_Binop
|
file | diff | annotate |
Thu, 04 Aug 2022 15:38:42 +0200 |
cleanup
|
file | diff | annotate |
Thu, 04 Aug 2022 15:24:58 +0200 |
review TODO.md, group items, make priority lists
|
file | diff | annotate |
Thu, 04 Aug 2022 14:18:35 +0200 |
Unchronized.ref are all eliminated by cf. b125dcf14489
|
file | diff | annotate |
Thu, 04 Aug 2022 12:48:37 +0200 |
polish naming in Rewrite_Order
|
file | diff | annotate |
Wed, 03 Aug 2022 18:06:02 +0200 |
eliminate global flags in GCD_Poly_ML, the last Unchronized.ref in isac
|
file | diff | annotate |
Wed, 03 Aug 2022 17:18:47 +0200 |
replace val rew_ord' = Unsynchronized.ref by Theory_Data
|
file | diff | annotate |
Wed, 03 Aug 2022 13:22:36 +0200 |
replace val example_store = Unsynchronized.ref by Thy_Data
|
file | diff | annotate |
Sun, 31 Jul 2022 16:35:33 +0200 |
eliminate global flag Eval.trace_on
|
file | diff | annotate |
Sat, 30 Jul 2022 16:47:45 +0200 |
eliminate global flag Rewrite.trace_on
|
file | diff | annotate |
Thu, 28 Jul 2022 11:43:27 +0200 |
trial on "empty" Example
|
file | diff | annotate |
Wed, 27 Jul 2022 14:14:16 +0200 |
polish naming
|
file | diff | annotate |
Wed, 27 Jul 2022 14:04:04 +0200 |
tuned
|
file | diff | annotate |
Wed, 27 Jul 2022 13:59:58 +0200 |
polish naming
|
file | diff | annotate |
Wed, 27 Jul 2022 13:11:43 +0200 |
polish naming
|
file | diff | annotate |
Tue, 26 Jul 2022 22:29:35 +0200 |
cleanup after trials on stepwise input to Example
|
file | diff | annotate |
Tue, 26 Jul 2022 22:11:41 +0200 |
questions about parsing in Outer_Syntax.command?Example?
|
file | diff | annotate |
Sat, 23 Jul 2022 20:05:25 +0200 |
//continued: investigate Outer_Syntax.command \<^command_keyword>?problem?
|
file | diff | annotate |
Wed, 20 Jul 2022 11:56:45 +0200 |
question about Outer_Syntax.command \<^command_keyword>?Example?
|
file | diff | annotate |
Wed, 20 Jul 2022 11:48:38 +0200 |
investigate Outer_Syntax.command \<^command_keyword>?problem?
|
file | diff | annotate |
Mon, 20 Jun 2022 09:56:48 +0200 |
review stepwise Specification in vscode-example.sml
|
file | diff | annotate |
Tue, 31 May 2022 16:21:22 +0200 |
cleanup
|
file | diff | annotate |
Tue, 31 May 2022 09:36:02 +0200 |
Calculation 1''': remove test-code from previous changeset 1c8263e775d4
|
file | diff | annotate |
Tue, 31 May 2022 09:16:12 +0200 |
Calculation 1'': ERROR in Demo_Example.thy, questions in TODO.md
|
file | diff | annotate |
Sun, 29 May 2022 19:00:35 +0200 |
Calculation 1: minimal changes in code + application
|
file | diff | annotate |
Fri, 27 May 2022 12:07:55 +0200 |
type check at init of Problem appears correct
|
file | diff | annotate |
Thu, 26 May 2022 12:44:51 +0200 |
unify parse 6': TermC.parse eliminated, Test_Isac ok
|
file | diff | annotate |
Mon, 13 Sep 2021 16:01:48 +0200 |
cleanup TOODOOs from eliminate ThmC.numerals_to_Free
|
file | diff | annotate |
Tue, 17 Aug 2021 22:39:48 +0200 |
less TODO;
|
file | diff | annotate |
Tue, 17 Aug 2021 14:47:12 +0200 |
more TODO;
|
file | diff | annotate |
Sat, 14 Aug 2021 21:40:55 +0200 |
update TODO.md
|
file | diff | annotate |
Sat, 14 Aug 2021 18:59:30 +0200 |
question about merge KEStore_Elems
|
file | diff | annotate |
Sat, 14 Aug 2021 18:49:36 +0200 |
question on @{make_string}, @{print}, @{print tracing}
|
file | diff | annotate |
Sat, 14 Aug 2021 18:13:37 +0200 |
checked all CS from 650e49610bfd upto 63cecf440235
|
file | diff | annotate |
Sat, 14 Aug 2021 15:18:48 +0200 |
update TODO.md according to cf.a56ac28081a9
|
file | diff | annotate |
Sat, 14 Aug 2021 13:52:23 +0200 |
note on Thm.get_name_hint
|
file | diff | annotate |
Wed, 11 Aug 2021 11:54:07 +0200 |
note on Context.theory_name vs. Context.theory_long_name
|
file | diff | annotate |
Tue, 10 Aug 2021 19:05:59 +0200 |
make Integrate.add_new_c a proper constant
|
file | diff | annotate |
Tue, 10 Aug 2021 12:58:33 +0200 |
explain "KEStore_Elems.add_thes" in TODO.md
|
file | diff | annotate |
Tue, 10 Aug 2021 12:56:06 +0200 |
cleanup MethodC.prep_input that used a different theory
|
file | diff | annotate |
Tue, 10 Aug 2021 11:55:24 +0200 |
tuned
|
file | diff | annotate |
Tue, 10 Aug 2021 11:54:12 +0200 |
relate note on planned improvements (cf.03dea0a179d0) to TODO.md
|
file | diff | annotate |
Tue, 10 Aug 2021 11:29:33 +0200 |
remove items already done
|
file | diff | annotate |
Tue, 10 Aug 2021 11:01:18 +0200 |
eliminate ThyC.to_ctxt, use Proof_Context.init_global inline
|
file | diff | annotate |
Tue, 10 Aug 2021 10:27:15 +0200 |
note on CS c7b1a99bcfd2 , \<^ML>?Thy_Info.get_theory?
|
file | diff | annotate |
Mon, 09 Aug 2021 14:20:20 +0200 |
eliminate ThyC.to_ctxt done except 1 error
|
file | diff | annotate |
Tue, 27 Jul 2021 11:21:14 +0200 |
revert previous changeset
|
file | diff | annotate |
Mon, 19 Jul 2021 18:39:02 +0200 |
eliminate type float; was an early attempt overrun by Isabelle
|
file | diff | annotate |
Sun, 18 Jul 2021 18:15:27 +0200 |
merged
|
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 |