| Thu, 15 Dec 2022 13:16:00 +0100 |
less TODO;
|
file | diff | annotate |
| Thu, 15 Dec 2022 13:03:55 +0100 |
merged
|
file | diff | annotate |
| Thu, 15 Dec 2022 13:03:51 +0100 |
proper indication of error-msg "Wrong descriptor" in problem/method
|
file | diff | annotate |
| Sat, 10 Dec 2022 15:00:55 +0100 |
more TODO;
|
file | diff | annotate |
| Fri, 09 Dec 2022 12:58:41 +0100 |
more TODO;
|
file | diff | annotate |
| Sat, 26 Nov 2022 22:28:33 +0100 |
follow-up Makarius #4: prepare implementation of template for Specification
|
file | diff | annotate |
| Sat, 19 Nov 2022 15:30:52 +0100 |
make Minisubplb/200-start-method independent #4: finish
|
file | diff | annotate |
| Wed, 16 Nov 2022 10:29:52 +0100 |
make Minisubplb/200-start-method independent #2: Tactic.Rewrite_Set partially
|
file | diff | annotate |
| Mon, 07 Nov 2022 19:58:01 +0100 |
rename KEstore_Elems to Know_Store
|
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 |
| Mon, 31 Oct 2022 16:43:48 +0100 |
cleanup Problem/MethodC..prep_input
|
file | diff | annotate |
| Wed, 26 Oct 2022 09:54:58 +0200 |
review TODO
|
file | diff | annotate |
| Tue, 25 Oct 2022 17:42:04 +0200 |
follow up 7: Example with an *empty* Specification; follow ups finished
|
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 12:12:18 +0200 |
cleanup *_PIDE 1: TermC
|
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 13:10:24 +0200 |
cleanup 1: clarify adapt_to_type for Prog_Tac
|
file | diff | annotate |
| Wed, 19 Oct 2022 10:43:04 +0200 |
eliminate term2str in src, Prog_Tac.*_adapt_to_type
|
file | diff | annotate |
| Sat, 08 Oct 2022 19:17:24 +0200 |
follow up 5d: Error_Pattern.fill_in also included to adapt_to_type
|
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 |
| Fri, 16 Sep 2022 12:13:23 +0200 |
follow up 1a: restrict concept to adaptation of types within pre-compiled terms
|
file | diff | annotate |
| Thu, 15 Sep 2022 10:07:12 +0200 |
follow up meeting Makarius 1: new concept of parsing within current ?ML_structure Context?
|
file | diff | annotate |
| Wed, 14 Sep 2022 11:33:10 +0200 |
uniform "_PIDE" for functions intermediate in Isabelle/Isac
|
file | diff | annotate |
| Tue, 13 Sep 2022 10:28:04 +0200 |
adaptation to mail
|
file | diff | annotate |
| Fri, 09 Sep 2022 10:15:28 +0200 |
eliminate KEStore_Elems.get_thes, add_thes 2: get_rew_ord, get_calc, get_cas
|
file | diff | annotate |
| Tue, 06 Sep 2022 11:47:00 +0200 |
prepare elimination of KEStore_Elems.get_thes, add_thes
|
file | diff | annotate |
| Wed, 24 Aug 2022 19:15:06 +0200 |
cleanup Rule_Def and Eval_Def
|
file | diff | annotate |
| Wed, 24 Aug 2022 12:37:07 +0200 |
eliminate SPARK; as an example replaced by Outer_Syntax.command..problem
|
file | diff | annotate |
| Tue, 23 Aug 2022 18:05:08 +0200 |
note name-polishing required
|
file | diff | annotate |
| Mon, 22 Aug 2022 13:39:32 +0200 |
push ctxt through LI (Lucas-Interpreter)
|
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:20:48 +0200 |
reminder of userrequirement "start Calculation with CAS_Cmd"
|
file | diff | annotate |
| Tue, 16 Aug 2022 12:21:21 +0200 |
prepare src for: push ctxt throught Lucas-Interpretation
|
file | diff | annotate |
| Sat, 06 Aug 2022 18:50:43 +0200 |
push Proof.context through Derive.steps, note HACK
|
file | diff | annotate |
| Sat, 06 Aug 2022 18:00:33 +0200 |
push Proof.context through Error_Pattern.fill_form
|
file | diff | annotate |
| Sat, 06 Aug 2022 17:36:59 +0200 |
push Proof.context through Error_Pattern.check_for
|
file | diff | annotate |
| Sat, 06 Aug 2022 15:57:46 +0200 |
review TODO.md: eliminate get_thes is easier than anticipated
|
file | diff | annotate |
| Sat, 06 Aug 2022 15:02:55 +0200 |
eliminate union_overwrite and use standard namespace merge
|
file | diff | annotate |
| Sat, 06 Aug 2022 10:45:24 +0200 |
reorder TODO.md priorities
|
file | diff | annotate |
| Fri, 05 Aug 2022 12:30:16 +0200 |
push Proof.context through Eval.adhoc_thm
|
file | diff | annotate |
| Fri, 05 Aug 2022 11:38:10 +0200 |
improve error-msg of Problem.from_store, MethodC.from_store
|
file | diff | annotate |
| Fri, 05 Aug 2022 08:45:37 +0200 |
finish Calc_Binop, add signature EXAMPLE
|
file | diff | annotate |
| Thu, 04 Aug 2022 16:48:37 +0200 |
add structure Calc_Binop
|
file | diff | annotate |
| Thu, 04 Aug 2022 15:38:42 +0200 |
cleanup
|
file | diff | annotate |
| Thu, 04 Aug 2022 15:24:58 +0200 |
review TODO.md, group items, make priority lists
|
file | diff | annotate |
| Thu, 04 Aug 2022 14:18:35 +0200 |
Unchronized.ref are all eliminated by cf. b125dcf14489
|
file | diff | annotate |
| Thu, 04 Aug 2022 12:48:37 +0200 |
polish naming in Rewrite_Order
|
file | diff | annotate |
| Wed, 03 Aug 2022 18:06:02 +0200 |
eliminate global flags in GCD_Poly_ML, the last Unchronized.ref in isac
|
file | diff | annotate |
| Wed, 03 Aug 2022 17:18:47 +0200 |
replace val rew_ord' = Unsynchronized.ref by Theory_Data
|
file | diff | annotate |
| Wed, 03 Aug 2022 13:22:36 +0200 |
replace val example_store = Unsynchronized.ref by Thy_Data
|
file | diff | annotate |
| Sun, 31 Jul 2022 16:35:33 +0200 |
eliminate global flag Eval.trace_on
|
file | diff | annotate |
| Sat, 30 Jul 2022 16:47:45 +0200 |
eliminate global flag Rewrite.trace_on
|
file | diff | annotate |
| Thu, 28 Jul 2022 11:43:27 +0200 |
trial on "empty" Example
|
file | diff | annotate |
| Wed, 27 Jul 2022 14:14:16 +0200 |
polish naming
|
file | diff | annotate |
| Wed, 27 Jul 2022 14:04:04 +0200 |
tuned
|
file | diff | annotate |