| Mon, 11 Dec 2023 17:26:30 +0100 |
eliminate the intermediate *_POS
|
file | diff | annotate |
| Mon, 11 Dec 2023 12:14:28 +0100 |
rollback
|
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 |
| Sun, 10 Dec 2023 07:56:02 +0100 |
prepare 5: whole directory Specify/* with I_Model.T_POS exclusively
|
file | diff | annotate |
| Thu, 07 Dec 2023 16:14:32 +0100 |
prepare 3: Tactic.T with I_Model.T_POS
|
file | diff | annotate |
| Thu, 07 Dec 2023 11:54:42 +0100 |
prepare 2: p-spec.sml in Specify/ with I_Model.T_POS
|
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 |
| Wed, 29 Nov 2023 07:51:28 +0100 |
prepare 15: adapt M_Match.by_o_model to varaints
|
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 |
| Thu, 16 Nov 2023 08:15:46 +0100 |
prepare 14: improved item_to_add
|
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 |
| Mon, 02 Oct 2023 15:39:22 +0200 |
prepare 11: clean up new code 1
|
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, 30 Aug 2023 06:37:56 +0200 |
prepare 2: I_Model.of_max_variant ready for use in I_Model.complete
|
file | diff | annotate |
| Sun, 27 Aug 2023 16:48:03 +0200 |
followup 3: rename Pre_Conds.* and I_Model.* (eliminate *_TEST as much as possible)
|
file | diff | annotate |
| Wed, 26 Jul 2023 11:12:55 +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 Feb 2023 17:25:09 +0100 |
eliminate use of Thy_Info 23: ThyC.get_theory ctxt is mandadory
|
file | diff | annotate |
| Thu, 26 Jan 2023 13:31:07 +0100 |
use exclusively new ContextC.build_while_parsing
|
file | diff | annotate |
| Fri, 06 Jan 2023 15:06:40 +0100 |
eliminate use of Thy_Info 1: ThyC.get_theory in Specify_Step, Specify, Step_Specify
|
file | diff | annotate |
| Thu, 08 Dec 2022 17:55:45 +0100 |
make Minisubplb/400-start-meth-subpbl.sml from Thy_Info
|
file | diff | annotate |
| Thu, 08 Dec 2022 10:16:40 +0100 |
make Minisubplb/300-init-subpbl.sml independent from Thy_Info
|
file | diff | annotate |
| Thu, 10 Nov 2022 14:25:38 +0100 |
make Minisubplb/200-start-method independent from Thy_Info #1
|
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 |
| Tue, 25 Oct 2022 16:15:47 +0200 |
follow up 6: eliminate use of Thy_Info.get_theory, part 1
|
file | diff | annotate |
| Fri, 21 Oct 2022 15:35:50 +0200 |
cleanup *?PIDE 2: finished
|
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 |
| Wed, 14 Sep 2022 11:33:10 +0200 |
uniform "_PIDE" for functions intermediate in Isabelle/Isac
|
file | diff | annotate |
| Wed, 27 Jul 2022 13:11:43 +0200 |
polish naming
|
file | diff | annotate |
| Wed, 22 Jun 2022 17:33:45 +0200 |
initialise VSCode_Example with complete Specification
|
file | diff | annotate |
| Tue, 21 Jun 2022 16:04:43 +0200 |
rename functions in i-model.sml
|
file | diff | annotate |
| Mon, 20 Jun 2022 18:37:54 +0200 |
rename functions in o-model.sml
|
file | diff | annotate |
| Sun, 18 Apr 2021 23:37:59 +0200 |
conditional compilation via system option "isac_test" and antiquotation \<^isac_test>CARTOUCHE:
|
file | diff | annotate |
| Wed, 03 Feb 2021 16:39:44 +0100 |
Isac's MethodC not shadowing Isabelle's Method
|
file | diff | annotate |
| Wed, 04 Nov 2020 09:59:30 +0100 |
separate code for Example from spark_open, resolve name clash
|
file | diff | annotate |
| Sun, 14 Jun 2020 15:39:55 +0200 |
unify code (and replace Specify.by_tactic_input' by Specify.by_Add_)
|
file | diff | annotate |
| Wed, 03 Jun 2020 17:15:04 +0200 |
make Specify.find_next_step more readable
|
file | diff | annotate |
| Wed, 03 Jun 2020 13:57:22 +0200 |
unify Pre_Conds.check, partially
|
file | diff | annotate |
| Wed, 03 Jun 2020 11:25:19 +0200 |
follow 2 ancient updates of Library.ML
|
file | diff | annotate |
| Wed, 03 Jun 2020 09:56:24 +0200 |
simplify code, rename
|
file | diff | annotate |
| Mon, 01 Jun 2020 16:11:05 +0200 |
remove Specify.find_next_step'
|
file | diff | annotate |
| Sat, 30 May 2020 15:20:22 +0200 |
cleanup code after resolve hacks
|
file | diff | annotate |
| Sat, 30 May 2020 14:10:58 +0200 |
resolve hacks finished
|
file | diff | annotate |
| Thu, 28 May 2020 12:52:25 +0200 |
resolve hacks, part 2: Specify.find_next_step, Specify.by_tactic_input
|
file | diff | annotate |
| Wed, 27 May 2020 13:42:37 +0200 |
Test_Isac_Short OK with OLD code, Test_Some OK with NEW
|
file | diff | annotate |
| Tue, 26 May 2020 11:53:43 +0200 |
prep.resolve hacks introduced with funpack, part 4
|
file | diff | annotate |
| Mon, 25 May 2020 16:52:38 +0200 |
prep.resolve hacks introduced with funpack, part 3
|
file | diff | annotate |
| Sun, 24 May 2020 16:05:36 +0200 |
prep.resolve hacks introduced with funpack, part 1
|
file | diff | annotate |
| Mon, 18 May 2020 14:12:01 +0200 |
cleanup Specification, Specify
|
file | diff | annotate |
| Mon, 18 May 2020 14:02:54 +0200 |
sprep.cleanup Specification, Specify
|
file | diff | annotate |