Thu, 07 Dec 2023 16:14:32 +0100 |
prepare 3: Tactic.T with I_Model.T_POS
|
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 |
Thu, 30 Nov 2023 08:11:50 +0100 |
some renamings
|
file | diff | annotate |
Sun, 19 Nov 2023 07:51:41 +0100 |
followup 1: improve new code
|
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 |
Tue, 29 Aug 2023 08:35:46 +0200 |
followup 4: delete old code
|
file | diff | annotate |
Sun, 27 Aug 2023 17:47:56 +0200 |
rename Refine.*
|
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 |
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, 19 Feb 2023 13:03:54 +0100 |
PIDE turn 4: I_Model.init requires other datatype feedback
|
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 |
Sat, 04 Feb 2023 17:00:25 +0100 |
eliminate use of Thy_Info 22: eliminate UnparseC.term, rename "_in_ctxt" -> ""
|
file | diff | annotate |
Thu, 26 Jan 2023 18:54:25 +0100 |
use exclusively some new *.to_string ctxt
|
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, 22 Dec 2022 17:06:19 +0100 |
make Minisubplb/800-append-on-Frm.sml independent from Thy_Info
|
file | diff | annotate |
Wed, 21 Dec 2022 18:48:23 +0100 |
make Minisubplb/710-interSteps-short.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 |
Sat, 08 Oct 2022 11:40:48 +0200 |
follow up 5: cleanup
|
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, 27 Jul 2022 13:11:43 +0200 |
polish naming
|
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 |
Mon, 01 Jun 2020 11:49:37 +0200 |
unify code
|
file | diff | annotate |
Fri, 29 May 2020 12:43:41 +0200 |
[errors 4, Test_Isac_Short] resolve hacks, part 4: reapired O_Model.complete_for
|
file | diff | annotate |
Mon, 18 May 2020 14:21:41 +0200 |
Specify/* removed all warnings, only "handle _" remains
|
file | diff | annotate |
Fri, 15 May 2020 14:22:05 +0200 |
prep. cleanup of Specification
|
file | diff | annotate |
Wed, 13 May 2020 11:34:05 +0200 |
shift code from struct.Specify to appropriate locations
|
file | diff | annotate |
Tue, 12 May 2020 17:42:29 +0200 |
shift code from struct.Specify to appropriate locations
|
file | diff | annotate |
Tue, 12 May 2020 16:22:00 +0200 |
cleanup struct.O_Model, P_Model
|
file | diff | annotate |
Tue, 12 May 2020 10:14:09 +0200 |
distribute code from old Specify/ptyps.sml
|
file | diff | annotate |
Mon, 11 May 2020 11:07:19 +0200 |
separate struct.Refine, Pre_Conds.
|
file | diff | annotate |
Sun, 10 May 2020 17:26:36 +0200 |
cleanup generate.sml, model.sml
|
file | diff | annotate |
Sun, 10 May 2020 15:55:30 +0200 |
collect code for struct.I_Model
|
file | diff | annotate |
Mon, 04 May 2020 11:13:16 +0200 |
cleanup struct.Derive
|
file | diff | annotate |
Mon, 04 May 2020 10:19:16 +0200 |
spearate Specify_Step.add
|
file | diff | annotate |
Mon, 04 May 2020 09:25:51 +0200 |
separate Solve_Step.add, rearrange code, prep. Specify_Step
|
file | diff | annotate |
Sat, 02 May 2020 16:55:14 +0200 |
simplify Specify_Step.chek
|
file | diff | annotate |
Sat, 02 May 2020 11:36:13 +0200 |
remove Init_Proof, is NOT a tactic
|
file | diff | annotate |
Fri, 01 May 2020 17:17:41 +0200 |
unify sequence of tactics
|
file | diff | annotate |
Fri, 01 May 2020 16:06:59 +0200 |
separate Specify_Step.check
|
file | diff | annotate |
Wed, 29 Apr 2020 12:30:51 +0200 |
prep. separation of check Applicable between specify-phase and solve-phase
|
file | diff | annotate |