| Wed, 11 Jan 2023 09:23:18 +0100 |
wneuper |
eliminate use of Thy_Info 12: prep.arg. ctxt in TermC, UnparseC
|
changeset |
files
|
| Wed, 11 Jan 2023 06:06:12 +0100 |
wneuper |
eliminate use of Thy_Info 11: arg. ctxt for ThmC.string_of_thm/s
|
changeset |
files
|
| Tue, 10 Jan 2023 17:07:53 +0100 |
wneuper |
eliminate use of Thy_Info 10: arg. ctxt for Rule.to_string finished
|
changeset |
files
|
| Tue, 10 Jan 2023 10:01:05 +0100 |
wneuper |
eliminate use of Thy_Info 9: arg. ctxt for Rule.to_string, Istate.to_string
|
changeset |
files
|
| Mon, 09 Jan 2023 16:40:54 +0100 |
wneuper |
eliminate use of Thy_Info 8: arg. ctxt for Rule.to_string, partially
|
changeset |
files
|
| Mon, 09 Jan 2023 16:11:17 +0100 |
wneuper |
eliminate use of Thy_Info 6: improved ThmC.*_sym_rule
|
changeset |
files
|
| Sun, 08 Jan 2023 17:26:00 +0100 |
wneuper |
eliminate use of Thy_Info 6: improve ctxt in fetchProposedTactic, Error_Pattern, etc
|
changeset |
files
|
| Sun, 08 Jan 2023 16:19:31 +0100 |
wneuper |
eliminate use of Thy_Info 5: ThyC.get_theory in Error_Pattern, Kernel
|
changeset |
files
|
| Sun, 08 Jan 2023 12:33:27 +0100 |
wneuper |
eliminate use of Thy_Info 4: ThyC.get_theory in Step_Solve, Fetch_Tacs
|
changeset |
files
|
| Sun, 08 Jan 2023 10:30:58 +0100 |
wneuper |
eliminate use of Thy_Info 3> improved LItool.tac_from_prog
|
changeset |
files
|
| Fri, 06 Jan 2023 15:40:45 +0100 |
wneuper |
eliminate use of Thy_Info 2: ThyC.get_theory in Math_Engine
|
changeset |
files
|
| Fri, 06 Jan 2023 15:06:40 +0100 |
wneuper |
eliminate use of Thy_Info 1: ThyC.get_theory in Specify_Step, Specify, Step_Specify
|
changeset |
files
|
| Fri, 06 Jan 2023 11:43:50 +0100 |
wneuper |
polished
|
changeset |
files
|
| Fri, 06 Jan 2023 11:32:57 +0100 |
wneuper |
eliminate thy-hierarchy 5, end: remove Thy_Write
|
changeset |
files
|
| Fri, 06 Jan 2023 10:50:33 +0100 |
wneuper |
eliminate thy-hierarchy 4: remove Thy_Read
|
changeset |
files
|
| Fri, 06 Jan 2023 10:33:16 +0100 |
wneuper |
eliminate thy-hierarchy 3: shift (part of) metadata to ThyC
|
changeset |
files
|
| Fri, 06 Jan 2023 09:55:35 +0100 |
wneuper |
shift add_errpats to respective theory
|
changeset |
files
|
| Fri, 06 Jan 2023 08:33:18 +0100 |
wneuper |
eliminate thy-hierarchy 2: Error_Pattern.from_store independent
|
changeset |
files
|
| Fri, 06 Jan 2023 08:04:36 +0100 |
wneuper |
eliminate thy-hierarchy 1: Error_Pattern.fill_from_store independent from..
|
changeset |
files
|
| Thu, 22 Dec 2022 17:06:19 +0100 |
wneuper |
make Minisubplb/800-append-on-Frm.sml independent from Thy_Info
|
changeset |
files
|
| Thu, 22 Dec 2022 10:27:12 +0100 |
wneuper |
make Minisubplb/800-append-on-Frm.sml independent from Thy_Info
|
changeset |
files
|
| Wed, 21 Dec 2022 18:48:23 +0100 |
wneuper |
make Minisubplb/710-interSteps-short.sml independent from Thy_Info
|
changeset |
files
|
| Tue, 20 Dec 2022 08:11:26 +0100 |
wneuper |
before Tactic.input_to_string ctxt -- hg rollback
|
changeset |
files
|
| Thu, 15 Dec 2022 13:16:00 +0100 |
wneuper |
less TODO;
|
changeset |
files
|
| Thu, 15 Dec 2022 13:03:55 +0100 |
wneuper |
merged
|
changeset |
files
|
| Thu, 15 Dec 2022 13:03:51 +0100 |
wneuper |
proper indication of error-msg "Wrong descriptor" in problem/method
|
changeset |
files
|
| Sat, 10 Dec 2022 15:16:41 +0100 |
wenzelm |
slightly more formal theory source;
|
changeset |
files
|
| Sat, 10 Dec 2022 15:00:55 +0100 |
wenzelm |
more TODO;
|
changeset |
files
|
| Sat, 10 Dec 2022 14:57:49 +0100 |
wenzelm |
backed out changeset 836b57d05d0a: cwd is above isa/ and isabisac/ in README.md;
|
changeset |
files
|
| Fri, 09 Dec 2022 16:29:04 +0100 |
wneuper |
merge
|
changeset |
files
|
| Fri, 09 Dec 2022 16:28:10 +0100 |
wneuper |
after update of Isabelle version
|
changeset |
files
|
| Fri, 09 Dec 2022 13:51:02 +0100 |
wneuper |
make up to Minisubplb/700-interSteps.sml from Thy_Info (on Isabelle2021-1)
|
changeset |
files
|
| Fri, 09 Dec 2022 12:59:16 +0100 |
wenzelm |
removed obsolete "extend" operation;
|
changeset |
files
|
| Fri, 09 Dec 2022 12:58:41 +0100 |
wenzelm |
more TODO;
|
changeset |
files
|
| Fri, 09 Dec 2022 12:37:26 +0100 |
wenzelm |
follow Isabelle repository;
|
changeset |
files
|
| Fri, 09 Dec 2022 12:23:30 +0100 |
wenzelm |
merged;
|
changeset |
files
|
| Tue, 15 Nov 2022 13:52:25 +0100 |
wenzelm |
update to Isabelle2022 release;
|
changeset |
files
|
| Tue, 15 Nov 2022 11:30:31 +0100 |
wenzelm |
proper session directories;
|
changeset |
files
|
| Thu, 08 Dec 2022 17:55:45 +0100 |
wneuper |
make Minisubplb/400-start-meth-subpbl.sml from Thy_Info
|
changeset |
files
|
| Thu, 08 Dec 2022 10:33:27 +0100 |
wneuper |
tuned files, Test_Isac.thy works
|
changeset |
files
|
| Thu, 08 Dec 2022 10:16:40 +0100 |
wneuper |
make Minisubplb/300-init-subpbl.sml independent from Thy_Info
|
changeset |
files
|
| Sun, 04 Dec 2022 16:48:06 +0100 |
wneuper |
make Minisubplb/300-init-subpbl-NEXT_STEP.sml independent from Thy_Info
|
changeset |
files
|
| Sat, 03 Dec 2022 19:12:38 +0100 |
wneuper |
cleanup
|
changeset |
files
|
| Sat, 03 Dec 2022 19:09:51 +0100 |
wneuper |
follow-up Makarius #4b: clarify type model_out
|
changeset |
files
|
| Sat, 26 Nov 2022 22:28:33 +0100 |
wneuper |
follow-up Makarius #4: prepare implementation of template for Specification
|
changeset |
files
|
| Fri, 25 Nov 2022 10:36:46 +0100 |
wneuper |
follow-up Makarius #3.1: compare parse_pos_cas etc with parse_pos_model_input etc
|
changeset |
files
|
| Thu, 24 Nov 2022 18:07:17 +0100 |
wneuper |
follow-up Makarius #3: reorganise parse for proper error-reporting in problem/method
|
changeset |
files
|
| Wed, 23 Nov 2022 11:14:38 +0100 |
wneuper |
while renamings in MethodC -- hg rollback
|
changeset |
files
|
| Sun, 20 Nov 2022 11:36:46 +0100 |
wneuper |
recall future refinement of Specification
|
changeset |
files
|
| Sun, 20 Nov 2022 10:36:34 +0100 |
wneuper |
follow-up Makarius #2: provisional parsers for Example
|
changeset |
files
|
| Sun, 20 Nov 2022 09:47:34 +0100 |
wneuper |
follow-up Makarius #1: errors are on the spot on CAS in problem
|
changeset |
files
|
| Sun, 20 Nov 2022 08:40:46 +0100 |
wneuper |
make Minisubplb/250-Rewrite_Set-from-method* independent from Thy_Info
|
changeset |
files
|
| Sat, 19 Nov 2022 17:00:59 +0100 |
wneuper |
make Minisubplb/200-start-method independent #5: prepreeding was 200-start-method-NEXT_STEP.sml
|
changeset |
files
|
| Sat, 19 Nov 2022 15:30:52 +0100 |
wneuper |
make Minisubplb/200-start-method independent #4: finish
|
changeset |
files
|
| Sat, 19 Nov 2022 12:10:19 +0100 |
wneuper |
improve Test_Tool
|
changeset |
files
|
| Wed, 16 Nov 2022 17:42:41 +0100 |
wneuper |
make Minisubplb/200-start-method independent #3: Rewrite_Ord.T with ctxt
|
changeset |
files
|
| Wed, 16 Nov 2022 10:30:59 +0100 |
wneuper |
merged
|
changeset |
files
|
| Wed, 16 Nov 2022 10:29:52 +0100 |
wneuper |
make Minisubplb/200-start-method independent #2: Tactic.Rewrite_Set partially
|
changeset |
files
|
| Tue, 15 Nov 2022 11:11:06 +0100 |
wenzelm |
proper quotes;
|
changeset |
files
|
| Thu, 10 Nov 2022 14:25:38 +0100 |
wneuper |
make Minisubplb/200-start-method independent from Thy_Info #1
|
changeset |
files
|