| 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 |
| Tue, 01 Jun 2021 15:41:23 +0200 |
Test_Some.thy with looping ML<>
|
file | diff | annotate |
| Mon, 21 Jun 2021 22:08:01 +0200 |
updated TODO;
|
file | diff | annotate |
| Mon, 21 Jun 2021 21:59:10 +0200 |
updated TODO;
|
file | diff | annotate |
| Mon, 21 Jun 2021 15:50:58 +0200 |
updated TODO;
|
file | diff | annotate |
| Wed, 16 Jun 2021 12:56:09 +0200 |
updated TODO;
|
file | diff | annotate |
| Sat, 12 Jun 2021 18:33:15 +0200 |
updated TODO;
|
file | diff | annotate |
| Sat, 12 Jun 2021 18:30:31 +0200 |
updated TODO;
|
file | diff | annotate |
| Sat, 12 Jun 2021 14:27:03 +0200 |
updated TODO;
|
file | diff | annotate |
| Thu, 10 Jun 2021 12:53:02 +0200 |
more TODO;
|
file | diff | annotate |
| Wed, 09 Jun 2021 20:28:42 +0200 |
more TODO;
|
file | diff | annotate |
| Tue, 01 Jun 2021 21:01:32 +0200 |
more TODO;
|
file | diff | annotate |
| Wed, 26 May 2021 16:19:41 +0200 |
more TODO;
|
file | diff | annotate |
| Wed, 26 May 2021 14:10:17 +0200 |
more TODO;
|
file | diff | annotate |
| Wed, 26 May 2021 13:26:55 +0200 |
more TODO;
|
file | diff | annotate |