| Sun, 27 Aug 2023 17:56:50 +0200 |
update TODO.md
|
file | diff | annotate |
| Tue, 15 Aug 2023 12:22:49 +0200 |
prepare 13: Testi_Isac_Short without errors
|
file | diff | annotate |
| Wed, 19 Jul 2023 11:14:22 +0200 |
prepare 8: Test_Theory works until Tactic Specify_Theory
|
file | diff | annotate |
| Sat, 15 Jul 2023 17:44:37 +0200 |
prepare 7: extend I_Model.of_max_variant with make_envs_preconds
|
file | diff | annotate |
| Thu, 13 Jul 2023 10:51:16 +0200 |
prepare 5: clarify three environments in the specify-phase, see (*2*) type env_subst
|
file | diff | annotate |
| Tue, 20 Jun 2023 06:26:18 +0200 |
prepare 4: narrow I_Model.T -- _TEST
|
file | diff | annotate |
| Sat, 03 Jun 2023 16:45:43 +0200 |
prepare 3: clean code
|
file | diff | annotate |
| Tue, 23 May 2023 07:56:29 +0200 |
rollback
|
file | diff | annotate |
| Tue, 04 Apr 2023 10:54:12 +0200 |
PIDE turn 10> new handling of variants, Pre_Conds.check_OLD/_TEST, I_Model.is_complete_OLD/_TEST
|
file | diff | annotate |
| Fri, 31 Mar 2023 12:07:52 +0200 |
//new Pre_Conds.check/_TEST breaks tests, need new signature
|
file | diff | annotate |
| Mon, 27 Feb 2023 09:45:29 +0100 |
PIDE turn 9: handle empty input, error in Test_VSCode_Example, isabelle@
|
file | diff | annotate |
| Wed, 22 Feb 2023 18:38:56 +0100 |
PIDE turn 7: prepare for Template.show
|
file | diff | annotate |
| Wed, 15 Feb 2023 15:56:09 +0100 |
PIDE turn 1: model's terms show syntax error
|
file | diff | annotate |
| Mon, 13 Feb 2023 09:54:34 +0100 |
tuned
|
file | diff | annotate |
| Sun, 12 Feb 2023 14:06:11 +0100 |
one more TODO
|
file | diff | annotate |
| Wed, 08 Feb 2023 07:51:39 +0100 |
remove accomplished TODOs
|
file | diff | annotate |
| Wed, 25 Jan 2023 17:51:52 +0100 |
use exclusively new Step_Specify.initialise / initialise'
|
file | diff | annotate |
| Thu, 15 Dec 2022 13:16:00 +0100 |
less TODO;
|
file | diff | annotate |
| Thu, 15 Dec 2022 13:03:55 +0100 |
merged
|
file | diff | annotate |
| Thu, 15 Dec 2022 13:03:51 +0100 |
proper indication of error-msg "Wrong descriptor" in problem/method
|
file | diff | annotate |
| Sat, 10 Dec 2022 15:00:55 +0100 |
more TODO;
|
file | diff | annotate |
| Fri, 09 Dec 2022 12:58:41 +0100 |
more TODO;
|
file | diff | annotate |
| Sat, 26 Nov 2022 22:28:33 +0100 |
follow-up Makarius #4: prepare implementation of template for Specification
|
file | diff | annotate |
| Sat, 19 Nov 2022 15:30:52 +0100 |
make Minisubplb/200-start-method independent #4: finish
|
file | diff | annotate |
| Wed, 16 Nov 2022 10:29:52 +0100 |
make Minisubplb/200-start-method independent #2: Tactic.Rewrite_Set partially
|
file | diff | annotate |
| Mon, 07 Nov 2022 19:58:01 +0100 |
rename KEstore_Elems to Know_Store
|
file | diff | annotate |
| Mon, 07 Nov 2022 17:37:20 +0100 |
rename fields in Method_Def.T
|
file | diff | annotate |
| Mon, 31 Oct 2022 18:28:36 +0100 |
rename fields in Probl_Def.T
|
file | diff | annotate |
| Mon, 31 Oct 2022 16:43:48 +0100 |
cleanup Problem/MethodC..prep_input
|
file | diff | annotate |
| Wed, 26 Oct 2022 09:54:58 +0200 |
review TODO
|
file | diff | annotate |
| Tue, 25 Oct 2022 17:42:04 +0200 |
follow up 7: Example with an *empty* Specification; follow ups finished
|
file | diff | annotate |
| Tue, 25 Oct 2022 16:15:47 +0200 |
follow up 6: eliminate use of Thy_Info.get_theory, part 1
|
file | diff | annotate |
| Sun, 23 Oct 2022 16:08:27 +0200 |
follow up 6a: eliminate Thy_Inof.get_thoery for Minisubplb/100-init-rootpbl.sml independent -- src only, rollback
|
file | diff | annotate |
| Thu, 20 Oct 2022 12:12:18 +0200 |
cleanup *_PIDE 1: TermC
|
file | diff | annotate |
| Thu, 20 Oct 2022 10:23:38 +0200 |
followup 6a: tests run from @{context} without sessions
|
file | diff | annotate |
| Wed, 19 Oct 2022 13:10:24 +0200 |
cleanup 1: clarify adapt_to_type for Prog_Tac
|
file | diff | annotate |
| Wed, 19 Oct 2022 10:43:04 +0200 |
eliminate term2str in src, Prog_Tac.*_adapt_to_type
|
file | diff | annotate |
| Sat, 08 Oct 2022 19:17:24 +0200 |
follow up 5d: Error_Pattern.fill_in also included to adapt_to_type
|
file | diff | annotate |
| Sat, 08 Oct 2022 11:40:48 +0200 |
follow up 5: cleanup
|
file | diff | annotate |
| Fri, 07 Oct 2022 20:46:48 +0200 |
follow up 3: MethodC.adapt_to_typ on loading by CalcTree, CalcTreeTEST
|
file | diff | annotate |
| Thu, 29 Sep 2022 18:02:10 +0200 |
build clean -- rollback
|
file | diff | annotate |
| Mon, 26 Sep 2022 10:57:53 +0200 |
follow up 2: Problem.adapt_to_typ on loading by CalcTree, CalcTreeTEST
|
file | diff | annotate |
| Fri, 16 Sep 2022 12:13:23 +0200 |
follow up 1a: restrict concept to adaptation of types within pre-compiled terms
|
file | diff | annotate |
| Thu, 15 Sep 2022 10:07:12 +0200 |
follow up meeting Makarius 1: new concept of parsing within current ?ML_structure Context?
|
file | diff | annotate |
| Wed, 14 Sep 2022 11:33:10 +0200 |
uniform "_PIDE" for functions intermediate in Isabelle/Isac
|
file | diff | annotate |
| Tue, 13 Sep 2022 10:28:04 +0200 |
adaptation to mail
|
file | diff | annotate |
| Fri, 09 Sep 2022 10:15:28 +0200 |
eliminate KEStore_Elems.get_thes, add_thes 2: get_rew_ord, get_calc, get_cas
|
file | diff | annotate |
| Tue, 06 Sep 2022 11:47:00 +0200 |
prepare elimination of KEStore_Elems.get_thes, add_thes
|
file | diff | annotate |
| Wed, 24 Aug 2022 19:15:06 +0200 |
cleanup Rule_Def and Eval_Def
|
file | diff | annotate |
| Wed, 24 Aug 2022 12:37:07 +0200 |
eliminate SPARK; as an example replaced by Outer_Syntax.command..problem
|
file | diff | annotate |
| Tue, 23 Aug 2022 18:05:08 +0200 |
note name-polishing required
|
file | diff | annotate |
| Mon, 22 Aug 2022 13:39:32 +0200 |
push ctxt through LI (Lucas-Interpreter)
|
file | diff | annotate |
| Mon, 22 Aug 2022 11:26:20 +0200 |
cleanup test for: push ctxt through LI
|
file | diff | annotate |
| Sun, 21 Aug 2022 16:20:48 +0200 |
reminder of userrequirement "start Calculation with CAS_Cmd"
|
file | diff | annotate |
| 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 |