Sun, 27 Aug 2023 11:19:14 +0200 |
followup 1 (to PIDE turn 11a): eliminate penv
|
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 |
Sun, 20 Aug 2023 08:54:01 +0200 |
rollback
|
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, 21 Jul 2023 14:16:57 +0200 |
prepare 10: Minisubpbl/* is in test standard format
|
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 |
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 |
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, 11 Jan 2023 09:23:18 +0100 |
eliminate use of Thy_Info 12: prep.arg. ctxt in TermC, UnparseC
|
file | diff | annotate |
Wed, 11 Jan 2023 06:06:12 +0100 |
eliminate use of Thy_Info 11: arg. ctxt for ThmC.string_of_thm/s
|
file | diff | annotate |
Sun, 08 Jan 2023 10:30:58 +0100 |
eliminate use of Thy_Info 3> improved LItool.tac_from_prog
|
file | diff | annotate |
Fri, 06 Jan 2023 08:33:18 +0100 |
eliminate thy-hierarchy 2: Error_Pattern.from_store independent
|
file | diff | annotate |
Fri, 06 Jan 2023 08:04:36 +0100 |
eliminate thy-hierarchy 1: Error_Pattern.fill_from_store independent from..
|
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 |
Sun, 04 Dec 2022 16:48:06 +0100 |
make Minisubplb/300-init-subpbl-NEXT_STEP.sml independent from Thy_Info
|
file | diff | annotate |
Sat, 19 Nov 2022 15:30:52 +0100 |
make Minisubplb/200-start-method independent #4: finish
|
file | diff | annotate |
Mon, 07 Nov 2022 17:37:20 +0100 |
rename fields in Method_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 |
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 |
Wed, 19 Oct 2022 14:23:40 +0200 |
Test_Isac works -- hg rollback
|
file | diff | annotate |
Wed, 19 Oct 2022 10:43:04 +0200 |
eliminate term2str in src, Prog_Tac.*_adapt_to_type
|
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 |
Mon, 26 Sep 2022 10:57:53 +0200 |
follow up 2: Problem.adapt_to_typ on loading by CalcTree, CalcTreeTEST
|
file | diff | annotate |
Mon, 22 Aug 2022 11:26:20 +0200 |
cleanup test for: push ctxt through LI
|
file | diff | annotate |
Sun, 21 Aug 2022 16:14:45 +0200 |
prepare test 4 for: push ctxt through LI
|
file | diff | annotate |
Sun, 21 Aug 2022 11:22:04 +0200 |
//prepare test 3 for: push ctxt through LI (only CAS_Cmd not OK)
|
file | diff | annotate |
Tue, 26 Jul 2022 22:29:35 +0200 |
cleanup after trials on stepwise input to Example
|
file | diff | annotate |
Tue, 26 Jul 2022 19:29:09 +0200 |
prepare stepwise input to Example (1)
|
file | diff | annotate |
Tue, 21 Jun 2022 12:41:52 +0200 |
rename functions in o-model.sml finish
|
file | diff | annotate |
Mon, 20 Jun 2022 17:36:25 +0200 |
intermed 3
|
file | diff | annotate |
Mon, 20 Jun 2022 17:22:26 +0200 |
intermed 2
|
file | diff | annotate |
Mon, 20 Jun 2022 16:58:32 +0200 |
intermed 1
|
file | diff | annotate |
Mon, 20 Jun 2022 09:56:48 +0200 |
review stepwise Specification in vscode-example.sml
|
file | diff | annotate |
Sun, 19 Jun 2022 16:55:13 +0200 |
shifts tests to VSCode_Example.thy, vscode-example.sml
|
file | diff | annotate |
Sun, 19 Jun 2022 16:10:11 +0200 |
remove type error from Fromalise.model
|
file | diff | annotate |
Sun, 19 Jun 2022 09:35:51 +0200 |
review tests similar to Demo_Example
|
file | diff | annotate |
Thu, 26 May 2022 12:53:13 +0200 |
tuned
|
file | diff | annotate |
Wed, 25 May 2022 10:37:35 +0200 |
unify parse 6: TermC.parse eliminated, Test_Isac_Short ok
|
file | diff | annotate |
Tue, 16 Nov 2021 18:29:23 +0100 |
tuned
|
file | diff | annotate |
Tue, 16 Nov 2021 18:26:57 +0100 |
unify parse 4: eliminate parse, simple cases
|
file | diff | annotate |
Mon, 27 Sep 2021 20:24:24 +0200 |
cleanup; all relevant tests work again
|
file | diff | annotate |
Sat, 25 Sep 2021 21:41:51 +0200 |
more simp rules: 1 is another special case, so (- 1) needs to be treated separately;
|
file | diff | annotate |
Sat, 25 Sep 2021 13:54:06 +0200 |
\\ uncovered corner case of realpow: (- 1) ? 2
|
file | diff | annotate |
Fri, 24 Sep 2021 14:18:10 +0200 |
proper simp_ctxt;
|
file | diff | annotate |
Thu, 23 Sep 2021 13:47:16 +0200 |
\\ realpow is not handled by present Simplifier.rewrite simp_ctxt
|
file | diff | annotate |
Thu, 16 Sep 2021 17:23:54 +0200 |
separate realpow constant, with additional cases not covered by Transcendental.powr;
|
file | diff | annotate |
Tue, 14 Sep 2021 16:06:42 +0200 |
\\adopt Isabelles calculation of numerals, "(- 1) ? 2" still missing
|
file | diff | annotate |
Tue, 14 Sep 2021 12:22:57 +0200 |
\\adopt Isabelles calculation of numerals, some cases are missing
|
file | diff | annotate |
Sun, 12 Sep 2021 15:40:15 +0200 |
cleanup
|
file | diff | annotate |
Mon, 23 Aug 2021 14:24:06 +0200 |
repair rule-set reduce_0_1_2
|
file | diff | annotate |
Mon, 23 Aug 2021 12:33:10 +0200 |
repair fun eval_cancel finished
|
file | diff | annotate |
Sun, 22 Aug 2021 14:28:38 +0200 |
repair fun adhoc_thm + fun eval_cancel
|
file | diff | annotate |
Sun, 22 Aug 2021 11:42:55 +0200 |
improve error message for eval_fn
|
file | diff | annotate |
Sun, 22 Aug 2021 09:43:43 +0200 |
improvement in Rational.thy makes several testfiles run, breaks one.
|
file | diff | annotate |