| Mon, 01 Jan 2024 11:31:16 +0100 |
Doc/Specify_Phase 4: start use antiquotations from isar-ref
|
file | diff | annotate |
| Sat, 30 Dec 2023 07:07:58 +0100 |
update Lucas_Interpreter.thy
|
file | diff | annotate |
| Sat, 30 Dec 2023 06:22:52 +0100 |
more TODO
|
file | diff | annotate |
| Mon, 11 Dec 2023 17:26:30 +0100 |
eliminate the intermediate *_POS
|
file | diff | annotate |
| Mon, 11 Dec 2023 16:18:42 +0100 |
repair settings ISABELLE_ISAC_TEST
|
file | diff | annotate |
| Mon, 11 Dec 2023 09:24:02 +0100 |
prepare 1: delete old code with I_Model.T (without Position.T)
|
file | diff | annotate |
| Sun, 10 Dec 2023 17:35:07 +0100 |
PIDE turn 14: ALL src/* (except Ctree) with I_Model.T_POS exclusively
|
file | diff | annotate |
| Tue, 05 Dec 2023 18:15:45 +0100 |
prepare 1: towards I_Model.T_POS in Specify/ (and no I_Model.T)
|
file | diff | annotate |
| Fri, 01 Dec 2023 06:08:22 +0100 |
PIDE turn 13: rename ALL(?) code already handling Position.T from *_TEST to *_POS
|
file | diff | annotate |
| Fri, 01 Dec 2023 05:51:18 +0100 |
prepare 16: adapt Refine to variants
|
file | diff | annotate |
| Thu, 30 Nov 2023 08:11:50 +0100 |
some renamings
|
file | diff | annotate |
| Wed, 29 Nov 2023 07:51:28 +0100 |
prepare 15: adapt M_Match.by_o_model to varaints
|
file | diff | annotate |
| Sat, 25 Nov 2023 15:33:14 +0100 |
followup 4: cleanup new code
|
file | diff | annotate |
| Fri, 24 Nov 2023 15:34:07 +0100 |
followup 3: repair new fill_from_o, uncomment maximum of tests
|
file | diff | annotate |
| Mon, 20 Nov 2023 10:49:54 +0100 |
followup 2: un-comment / investigate tests, part.review TODO.md
|
file | diff | annotate |
| Thu, 16 Nov 2023 08:15:46 +0100 |
prepare 14: improved item_to_add
|
file | diff | annotate |
| Sun, 29 Oct 2023 07:14:14 +0100 |
prepare 13: improved max_variants
|
file | diff | annotate |
| Wed, 25 Oct 2023 12:34:12 +0200 |
prepare 12: M_Model.match_itms_oris takes Position.T and new max_mariants
|
file | diff | annotate |
| Tue, 03 Oct 2023 16:33:54 +0200 |
umpdate TODO.md
|
file | diff | annotate |
| Mon, 02 Oct 2023 12:02:59 +0200 |
prepare 10: check completeness of Specification regards variants and Position.T
|
file | diff | annotate |
| 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 |