| Tue, 31 Jan 2023 12:47:11 +0100 |
wneuper |
eliminate use of Thy_Info 14: UnparseC.term_opt ctxt
|
changeset |
files
|
| Tue, 31 Jan 2023 12:29:42 +0100 |
wneuper |
eliminate use of Thy_Info 13: eliminate UnparseC.term in test/
|
changeset |
files
|
| Tue, 31 Jan 2023 11:23:16 +0100 |
wneuper |
cleanup parse #7: eliminate TermC.parseNEW*; cleanup finished
|
changeset |
files
|
| Tue, 31 Jan 2023 10:49:17 +0100 |
wneuper |
cleanup parse #6: eliminate TermC.parseNEW
|
changeset |
files
|
| Mon, 30 Jan 2023 12:38:17 +0100 |
wneuper |
cleanup parse #5: eliminate TermC.parse_patt
|
changeset |
files
|
| Mon, 30 Jan 2023 12:11:40 +0100 |
wneuper |
cleanup parse #4: eliminate TermC.parse
|
changeset |
files
|
| Mon, 30 Jan 2023 09:47:18 +0100 |
wneuper |
cleanup parse #3: final functions inb ParseC
|
changeset |
files
|
| Sun, 29 Jan 2023 14:31:56 +0100 |
wneuper |
cleanup parse #2: repair error hidden by parse NONE in I_Model.check_single
|
changeset |
files
|
| Sat, 28 Jan 2023 13:21:39 +0100 |
wneuper |
cleanup parse #1: start eliminate parseNEW
|
changeset |
files
|
| Thu, 26 Jan 2023 19:02:41 +0100 |
wneuper |
cleanup
|
changeset |
files
|
| Thu, 26 Jan 2023 18:58:17 +0100 |
wneuper |
renaming
|
changeset |
files
|
| Thu, 26 Jan 2023 18:54:25 +0100 |
wneuper |
use exclusively some new *.to_string ctxt
|
changeset |
files
|
| Thu, 26 Jan 2023 13:31:07 +0100 |
wneuper |
use exclusively new ContextC.build_while_parsing
|
changeset |
files
|
| Wed, 25 Jan 2023 18:35:02 +0100 |
wneuper |
use exclusively new O_Model.init
|
changeset |
files
|
| Wed, 25 Jan 2023 17:51:52 +0100 |
wneuper |
use exclusively new Step_Specify.initialise / initialise'
|
changeset |
files
|
| Wed, 25 Jan 2023 15:52:33 +0100 |
wneuper |
ContextC.build_while_parsing, improves O_Model.init_PIDE
|
changeset |
files
|
| Wed, 11 Jan 2023 11:38:01 +0100 |
wneuper |
eliminate use of Thy_Info 12: TermC partially
|
changeset |
files
|
| 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
|