| Mon, 11 Dec 2023 16:12:53 +0100 |
PIDE turn 15: I_Model.T(_POS) stores Position.T for Specification
|
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 |
| Mon, 02 Oct 2023 15:39:22 +0200 |
prepare 11: clean up new code 1
|
file | diff | annotate |
| Tue, 26 Sep 2023 15:57:12 +0200 |
rollback
|
file | diff | annotate |
| Fri, 21 Jul 2023 14:16:57 +0200 |
prepare 10: Minisubpbl/* is in test standard format
|
file | diff | annotate |
| Tue, 23 May 2023 07:56:29 +0200 |
rollback
|
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 |
| Sat, 04 Feb 2023 16:20:45 +0100 |
eliminate use of Thy_Info 21: replace Unparse.term, TermC.unparse_ERROR for far off ctxt
|
file | diff | annotate |
| Sat, 19 Nov 2022 17:00:59 +0100 |
make Minisubplb/200-start-method independent #5: prepreeding was 200-start-method-NEXT_STEP.sml
|
file | diff | annotate |
| Mon, 07 Nov 2022 17:37:20 +0100 |
rename fields in Method_Def.T
|
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 |
| Thu, 20 Oct 2022 10:23:38 +0200 |
followup 6a: tests run from @{context} without sessions
|
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 |
| Wed, 03 Feb 2021 16:39:44 +0100 |
Isac's MethodC not shadowing Isabelle's Method
|
file | diff | annotate |
| Wed, 03 Jun 2020 11:25:19 +0200 |
follow 2 ancient updates of Library.ML
|
file | diff | annotate |
| Sat, 30 May 2020 16:18:01 +0200 |
remove hacks, finally
|
file | diff | annotate |
| Wed, 20 May 2020 12:52:09 +0200 |
standard format for string lists
|
file | diff | annotate |
| Sat, 16 May 2020 16:23:24 +0200 |
shift code from Specification to I_Model, rename ids
|
file | diff | annotate |
| Thu, 14 May 2020 13:33:47 +0200 |
rename Specification -> References, contiued
|
file | diff | annotate |
| Thu, 14 May 2020 09:30:40 +0200 |
start renaming Specification -> References;
|
file | diff | annotate |
| Thu, 14 May 2020 08:49:08 +0200 |
shift 2 preliminary hacks close to usage
|
file | diff | annotate |
| Tue, 12 May 2020 17:42:29 +0200 |
shift code from struct.Specify to appropriate locations
|
file | diff | annotate |
| Mon, 04 May 2020 16:25:14 +0200 |
shift code specific for specify-phase to Specify/*
|
file | diff | annotate |
| Mon, 04 May 2020 09:25:51 +0200 |
separate Solve_Step.add, rearrange code, prep. Specify_Step
|
file | diff | annotate |
| Fri, 01 May 2020 15:28:40 +0200 |
separate Solve_Step.check, repair ALL of Test_Isac_Short
|
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 |
| Tue, 28 Apr 2020 15:31:49 +0200 |
assign code from Rtools to appropriate struct.s
|
file | diff | annotate |
| Wed, 22 Apr 2020 14:36:27 +0200 |
use "Spec", "Problem", "Method" for renaming identifiers
|
file | diff | annotate |
| Tue, 21 Apr 2020 15:42:50 +0200 |
replace Celem. with new struct.s in BaseDefinitions/
|
file | diff | annotate |
| Wed, 15 Apr 2020 18:00:58 +0200 |
collect code in ThyC
|
file | diff | annotate |
| Fri, 10 Apr 2020 18:32:36 +0200 |
use "UnparseC" for renaming identifiers
|
file | diff | annotate |
| Fri, 10 Apr 2020 16:16:09 +0200 |
use "Rule" and "Rule_Set" for renaming identifiers
|
file | diff | annotate |
| Thu, 09 Apr 2020 18:21:09 +0200 |
rearrange code in Rule_Set and Rule
|
file | diff | annotate |
| Thu, 09 Apr 2020 17:13:17 +0200 |
separate struct. UnparseC, shift code to ThmC
|
file | diff | annotate |
| Sat, 04 Apr 2020 12:11:32 +0200 |
separate Rule_Set from Rule
|
file | diff | annotate |
| Wed, 01 Apr 2020 18:54:03 +0200 |
renaming, cleanup
|
file | diff | annotate |
| Wed, 01 Apr 2020 12:42:39 +0200 |
renaming, cleanup
|
file | diff | annotate |
| Wed, 01 Apr 2020 10:24:13 +0200 |
renaming, cleanup
|
file | diff | annotate |
| Wed, 25 Mar 2020 10:38:31 +0100 |
remove unused field in Ctree
|
file | diff | annotate |
| Wed, 18 Mar 2020 15:23:15 +0100 |
prep. cleanup LItool.resume_prog
|
file | diff | annotate |
| Sat, 07 Mar 2020 18:44:31 +0100 |
cleanup tac_from_prog, end
|
file | diff | annotate |
| Thu, 20 Feb 2020 18:02:00 +0100 |
prep. cleanup istate/ctxt in Ctree, part 4
|
file | diff | annotate |
| Thu, 20 Feb 2020 17:09:24 +0100 |
prep. cleanup istate/ctxt in Ctree, part 3
|
file | diff | annotate |
| Tue, 11 Feb 2020 11:58:45 +0100 |
introduce Step.by_tactic, part 1
|
file | diff | annotate |
| Tue, 04 Feb 2020 17:11:54 +0100 |
lucin: rename central structure to Lucin
|
file | diff | annotate |
| Thu, 23 Jan 2020 10:48:57 +0100 |
lucin: renaming due to simpler scanning (Istate .. found_accept)
|
file | diff | annotate |
| Wed, 22 Jan 2020 11:20:54 +0100 |
lucin: tests towards simpl. Lucin.scan*
|
file | diff | annotate |
| Fri, 17 Jan 2020 12:37:21 +0100 |
lucin: renaming
|
file | diff | annotate |
| Wed, 15 Jan 2020 12:12:44 +0100 |
lucin: rename fun *2 to fun * with expectation to unify fun * with fun *1
|
file | diff | annotate |
| Mon, 23 Dec 2019 16:58:36 +0100 |
shift code from mathengine-stateless.sml to Step.do_next
|
file | diff | annotate |
| Sat, 21 Dec 2019 18:05:13 +0100 |
lucin: unify do_next postponed
|
file | diff | annotate |
| Sat, 21 Dec 2019 16:45:10 +0100 |
lucin: unify do_next, partially
|
file | diff | annotate |
| Fri, 20 Dec 2019 10:24:52 +0100 |
ok again Test_Isac_Short since last 2 change sets
|
file | diff | annotate |
| Fri, 20 Dec 2019 09:41:11 +0100 |
remove unused fun mk_tac'_, get_form
|
file | diff | annotate |
| Thu, 19 Dec 2019 17:37:25 +0100 |
lucin: unify fun.ids. for locate_input_tactic
|
file | diff | annotate |
| Thu, 19 Dec 2019 16:41:57 +0100 |
cleanup fun solve, shift from Solve --> Step_Solve
|
file | diff | annotate |
| Wed, 18 Dec 2019 11:31:31 +0100 |
lucin: plan for new identifiers of steps
|
file | diff | annotate |
| Tue, 17 Dec 2019 16:31:46 +0100 |
lucin: shift Istate into Interpret/ from MathEngBasic
|
file | diff | annotate |
| Sat, 30 Nov 2019 15:43:14 +0100 |
lucin: prep. next_tactic_result, Accept_Tac2 takes ctxt in addition
|
file | diff | annotate |