| Thu, 26 Oct 2023 10:29:17 +0200 |
tuned
|
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 |
| Wed, 27 Sep 2023 12:17:44 +0200 |
prepare 9: I_Model.complete* all replaced by I_Model.s_make_complete
|
file | diff | annotate |
| Mon, 25 Sep 2023 08:39:43 +0200 |
prepare 8: replace complete_Method by general I_Model.s_make_complete
|
file | diff | annotate |
| Sun, 24 Sep 2023 20:04:41 +0200 |
rollback
|
file | diff | annotate |
| Wed, 20 Sep 2023 16:51:08 +0200 |
prepare 7: separate test for I_Model.s_make_complete
|
file | diff | annotate |
| Mon, 18 Sep 2023 10:26:35 +0200 |
prepare 4: shift new code (previous CS was: intermediate I_Model.complete_method)
|
file | diff | annotate |
| Mon, 18 Sep 2023 08:38:33 +0200 |
prepare 3: shift new code
|
file | diff | annotate |
| Wed, 30 Aug 2023 06:37:56 +0200 |
prepare 2: I_Model.of_max_variant ready for use in I_Model.complete
|
file | diff | annotate |
| Sat, 26 Aug 2023 11:37:16 +0200 |
PIDE turn 11a: specify-phase works with 3 new environments from max_variant
|
file | diff | annotate |
| Sat, 26 Aug 2023 10:51:35 +0200 |
prepare 17: repair Biegelinie formals and accordingly data for Formlise.model
|
file | diff | annotate |
| Sat, 19 Aug 2023 05:06:55 +0200 |
PIDE turn 11: Test_Isac_Short works on env_mode, type env_subst and type env_eval
|
file | diff | annotate |
| Fri, 18 Aug 2023 18:51:18 +0200 |
prepare 16: delete old code 2, shift feedback_to_string Pre_Conds -> I_Model
|
file | diff | annotate |
| Thu, 17 Aug 2023 08:01:45 +0200 |
prepare 15: delete old code 1, repair Pre_Conds.check_envs_TEST and check_pos
|
file | diff | annotate |
| Tue, 15 Aug 2023 17:39:06 +0200 |
prepare 14: eliminate Pre_Conds.check in test/*
|
file | diff | annotate |
| Tue, 15 Aug 2023 12:22:49 +0200 |
prepare 13: Testi_Isac_Short without errors
|
file | diff | annotate |
| Fri, 04 Aug 2023 23:07:04 +0200 |
//prepare 12: Test_Theory/100-init-.. and 150a-add-.. both work with src/*
|
file | diff | annotate |
| Fri, 04 Aug 2023 10:46:05 +0200 |
prepare 11: Test_Theory/100-init-rootpbl-NEXT_STEP.sml and 150a-add-.. both work
|
file | diff | annotate |
| Wed, 26 Jul 2023 11:12:55 +0200 |
rollback
|
file | diff | annotate |
| Fri, 21 Jul 2023 14:16:57 +0200 |
prepare 10: Minisubpbl/* is in test standard format
|
file | diff | annotate |
| Thu, 20 Jul 2023 10:24:48 +0200 |
prepare 9: Test_Theory works completely (until Apply_Method)
|
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 |
| Fri, 14 Jul 2023 12:33:25 +0200 |
prepare 6: repair I_Model.of_max_variant
|
file | diff | annotate |
| Fri, 14 Jul 2023 10:15:38 +0200 |
better usable descriptor type
|
file | diff | annotate |
| Fri, 14 Jul 2023 09:29:49 +0200 |
generalise descriptor type
|
file | diff | annotate |
| Thu, 13 Jul 2023 17:53:58 +0200 |
repair input-template for type bool
|
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 |
| Sun, 04 Jun 2023 10:12:38 +0200 |
prepare 3a: delete respective 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 |
| Tue, 07 Mar 2023 15:38:23 +0100 |
I_Model.init_TEST provides completion as far as reasonable
|
file | diff | annotate |
| Sun, 19 Feb 2023 13:03:54 +0100 |
PIDE turn 4: I_Model.init requires other datatype feedback
|
file | diff | annotate |
| Sun, 12 Feb 2023 12:44:25 +0100 |
move code from LibraryC to approptiate structures
|
file | diff | annotate |
| Tue, 07 Feb 2023 17:43:16 +0100 |
eliminate use of Thy_Info 24: finished
|
file | diff | annotate |
| Sun, 29 Jan 2023 14:31:56 +0100 |
cleanup parse #2: repair error hidden by parse NONE in I_Model.check_single
|
file | diff | annotate |
| Sat, 28 Jan 2023 13:21:39 +0100 |
cleanup parse #1: start eliminate parseNEW
|
file | diff | annotate |
| Wed, 25 Jan 2023 15:52:33 +0100 |
ContextC.build_while_parsing, improves O_Model.init_PIDE
|
file | diff | annotate |
| Thu, 22 Dec 2022 10:27:12 +0100 |
make Minisubplb/800-append-on-Frm.sml independent from Thy_Info
|
file | diff | annotate |
| Tue, 20 Dec 2022 08:11:26 +0100 |
before Tactic.input_to_string ctxt -- hg rollback
|
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 17:21:04 +0200 |
follow up 6a: eliminate Thy_Info.get_theory for Minisubplb/100-init-rootpbl.sml
|
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 10:23:38 +0200 |
followup 6a: tests run from @{context} without sessions
|
file | diff | annotate |
| Sun, 18 Apr 2021 18:30:31 +0200 |
proper test sessions, but with remaining failures;
|
file | diff | annotate |
| Fri, 16 Apr 2021 22:29:23 +0200 |
prefer symbolic directories $ISABELLE_ISAC and $ISABELLE_ISAC_TEST, instead of re-using ~~ for $ISABELLE_HOME;
|
file | diff | annotate |
| Wed, 03 Feb 2021 14:53:37 +0100 |
step 5.1: adapt ParseC.specification to new keywords
|
file | diff | annotate |
| Wed, 07 Oct 2020 09:31:10 +0200 |
Isabelle2019->20: adapt to new session requirements continued
|
file | diff | annotate |
| Fri, 10 Apr 2020 15:02:50 +0200 |
rename directory CalcElements to BaseDefinitions
|
file | diff | annotate |
| Fri, 29 Nov 2019 15:22:29 +0100 |
lucin: fun determine_next_tactic gets envisaged arguments
|
file | diff | annotate |
| Wed, 06 Nov 2019 15:08:27 +0100 |
lucin: args of appy, assy & Co reorganised
|
file | diff | annotate |
| Thu, 22 Aug 2019 16:48:04 +0200 |
lucin: rename Script --> Program
|
file | diff | annotate |
| Thu, 04 Jul 2019 15:13:30 +0200 |
lucin: tuned
|
file | diff | annotate |
| Wed, 21 Nov 2018 12:32:54 +0100 |
update to new Isabelle conventions: {*...*} to \<open>...\<close>
|
file | diff | annotate |
| Tue, 28 Aug 2018 13:34:22 +0200 |
Isabelle2017->18: adapt to more rigorous session handling
|
file | diff | annotate |
| Sun, 20 Sep 2015 16:04:35 +0200 |
tuned
|
file | diff | annotate |
| Fri, 08 May 2015 16:05:42 +0200 |
usage of Test_Theory.thy and Test_Some.thy
|
file | diff | annotate |
| Mon, 27 Jan 2014 11:09:57 +0100 |
ad 967c8a1eb6b1 (2b): add functions accessing Theory_Data in parallel to those accessing "ptyps = Unsynchronized.ref"
|
file | diff | annotate |