| Wed, 08 Feb 2023 07:51:39 +0100 |
remove accomplished TODOs
|
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 16:20:45 +0100 |
eliminate use of Thy_Info 21: replace Unparse.term, TermC.unparse_ERROR for far off ctxt
|
file | diff | annotate |
| Sat, 04 Feb 2023 09:47:27 +0100 |
eliminate use of Thy_Info 19: some more uses of UnparseC.term_in_ctxt
|
file | diff | annotate |
| Fri, 03 Feb 2023 15:26:19 +0100 |
eliminate use of Thy_Info 18: UnparseC.terms_to_strings --> asms_test
|
file | diff | annotate |
| Mon, 30 Jan 2023 09:47:18 +0100 |
cleanup parse #3: final functions inb ParseC
|
file | diff | annotate |
| Thu, 26 Jan 2023 18:54:25 +0100 |
use exclusively some new *.to_string ctxt
|
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 |
| Fri, 06 Jan 2023 15:40:45 +0100 |
eliminate use of Thy_Info 2: ThyC.get_theory in Math_Engine
|
file | diff | annotate |
| Fri, 06 Jan 2023 11:32:57 +0100 |
eliminate thy-hierarchy 5, end: remove Thy_Write
|
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 |
| Fri, 09 Dec 2022 12:59:16 +0100 |
removed obsolete "extend" operation;
|
file | diff | annotate |
| Thu, 08 Dec 2022 10:16:40 +0100 |
make Minisubplb/300-init-subpbl.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 |
| Wed, 23 Nov 2022 11:14:38 +0100 |
while renamings in MethodC -- hg rollback
|
file | diff | annotate |
| Mon, 07 Nov 2022 19:58:01 +0100 |
rename KEstore_Elems to Know_Store
|
file | diff | annotate |
| Mon, 31 Oct 2022 16:43:48 +0100 |
cleanup Problem/MethodC..prep_input
|
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 |
| Thu, 29 Sep 2022 18:02:10 +0200 |
build clean -- rollback
|
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 |
| Mon, 12 Sep 2022 18:02:44 +0200 |
eliminate KEStore_Elems.get_thes, add_thes 2: get_cas 2: cleanup finished
|
file | diff | annotate |
| Mon, 12 Sep 2022 17:46:32 +0200 |
eliminate KEStore_Elems.get_thes, add_thes 2: get_cas 1: Test_Isac ok
|
file | diff | annotate |
| Fri, 09 Sep 2022 10:53:51 +0200 |
eliminate KEStore_Elems.get_thes, add_thes 2: get_rew_ord finished
|
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 |
| Wed, 07 Sep 2022 15:06:50 +0200 |
eliminate KEStore_Elems.get_thes, add_thes 1: get_rls 4: cleanup
|
file | diff | annotate |
| Wed, 07 Sep 2022 10:58:12 +0200 |
eliminate KEStore_Elems.get_thes, add_thes 1: get_rls 1
|
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 18:29:33 +0200 |
polish naming in structure Eval
|
file | diff | annotate |
| Wed, 24 Aug 2022 17:21:14 +0200 |
polish naming in Rule_Def for Eval
|
file | diff | annotate |
| Tue, 23 Aug 2022 18:05:08 +0200 |
note name-polishing required
|
file | diff | annotate |
| Sat, 06 Aug 2022 15:02:55 +0200 |
eliminate union_overwrite and use standard namespace merge
|
file | diff | annotate |
| Thu, 04 Aug 2022 12:48:37 +0200 |
polish naming in Rewrite_Order
|
file | diff | annotate |
| Wed, 03 Aug 2022 18:17:27 +0200 |
cleanup
|
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 13:23:38 +0200 |
eliminate global flag Check_Unique.on
|
file | diff | annotate |
| Wed, 27 Jul 2022 13:59:58 +0200 |
polish naming
|
file | diff | annotate |
| Mon, 21 Jun 2021 21:53:23 +0200 |
Isar command 'cas' as front-end for KEStore_Elems.add_cas, without change of semantics;
|
file | diff | annotate |
| Mon, 21 Jun 2021 20:06:12 +0200 |
Isar command 'calculation' as front-end for KEStore_Elems.add_calcs, without change of semantics;
|
file | diff | annotate |
| Thu, 10 Jun 2021 11:54:20 +0200 |
clarified command name: this is to register already defined rule sets in the Knowledge Store;
|
file | diff | annotate |
| Wed, 26 May 2021 16:24:05 +0200 |
command 'setup_rule' semantic equivalent for KEStore_Elems.add_rlss;
|
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 |
| Fri, 15 May 2020 19:31:04 +0200 |
shift code from Specification to References, separate References_Def
|
file | diff | annotate |
| Thu, 14 May 2020 09:30:40 +0200 |
start renaming Specification -> References;
|
file | diff | annotate |
| Mon, 11 May 2020 11:38:52 +0200 |
error -> raise ERROR
|
file | diff | annotate |
| Thu, 07 May 2020 11:42:19 +0200 |
proper naming for Problem_Pattern (+ show old names)
|
file | diff | annotate |
| Wed, 29 Apr 2020 09:03:01 +0200 |
comments on relation between files.
|
file | diff | annotate |
| Tue, 28 Apr 2020 17:50:18 +0200 |
separate struct.Thy_Present, rename Thy_Html to Thy_Write
|
file | diff | annotate |
| Fri, 24 Apr 2020 08:51:05 +0200 |
separate struct.Error_Pattern, rename identifiers
|
file | diff | annotate |
| Wed, 22 Apr 2020 16:01:53 +0200 |
use "Check_Unique" for renaming identifiers
|
file | diff | annotate |
| Wed, 22 Apr 2020 14:36:27 +0200 |
use "Spec", "Problem", "Method" for renaming identifiers
|
file | diff | annotate |
| Wed, 22 Apr 2020 11:23:30 +0200 |
rename file according to struct.; start renaming with "Spec"
|
file | diff | annotate |
| Tue, 21 Apr 2020 12:26:08 +0200 |
use "Store" for renaming identifiers
|
file | diff | annotate |
| Tue, 21 Apr 2020 11:28:20 +0200 |
CAS_Cmd appears independent from CAS_Def (required for Know_Store)
|
file | diff | annotate |
| Tue, 21 Apr 2020 10:53:04 +0200 |
derive Method.T from Meth_Def.T, drop funs and types used by Know_Store
|
file | diff | annotate |
| Tue, 21 Apr 2020 10:13:30 +0200 |
derive Problem from Probl_Def, drop funs and types used by Know_Store
|
file | diff | annotate |
| Mon, 20 Apr 2020 16:47:01 +0200 |
rename remaining struct.s Celem5..Celem8
|
file | diff | annotate |