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
|
Wed, 09 Nov 2022 15:15:24 +0100 |
wneuper |
rename Minisubpbl: in the future "a" indicates a "Maximum"-test
|
changeset |
files
|
Mon, 07 Nov 2022 19:58:01 +0100 |
wneuper |
rename KEstore_Elems to Know_Store
|
changeset |
files
|
Mon, 07 Nov 2022 19:49:14 +0100 |
wneuper |
delete superfluous field in Method_Def.T
|
changeset |
files
|
Mon, 07 Nov 2022 17:37:20 +0100 |
wneuper |
rename fields in Method_Def.T
|
changeset |
files
|
Mon, 31 Oct 2022 18:28:36 +0100 |
wneuper |
rename fields in Probl_Def.T
|
changeset |
files
|
Mon, 31 Oct 2022 16:53:59 +0100 |
wneuper |
delete forgotten code
|
changeset |
files
|
Mon, 31 Oct 2022 16:43:48 +0100 |
wneuper |
cleanup Problem/MethodC..prep_input
|
changeset |
files
|
Wed, 26 Oct 2022 09:54:58 +0200 |
wneuper |
review TODO
|
changeset |
files
|
Wed, 26 Oct 2022 09:38:28 +0200 |
wneuper |
cleanup
|
changeset |
files
|
Tue, 25 Oct 2022 17:44:08 +0200 |
wneuper |
polished
|
changeset |
files
|
Tue, 25 Oct 2022 17:42:04 +0200 |
wneuper |
follow up 7: Example with an *empty* Specification; follow ups finished
|
changeset |
files
|
Tue, 25 Oct 2022 16:15:47 +0200 |
wneuper |
follow up 6: eliminate use of Thy_Info.get_theory, part 1
|
changeset |
files
|
Sun, 23 Oct 2022 17:21:04 +0200 |
wneuper |
follow up 6a: eliminate Thy_Info.get_theory for Minisubplb/100-init-rootpbl.sml
|
changeset |
files
|
Sun, 23 Oct 2022 16:08:27 +0200 |
wneuper |
follow up 6a: eliminate Thy_Inof.get_thoery for Minisubplb/100-init-rootpbl.sml independent -- src only, rollback
|
changeset |
files
|
Fri, 21 Oct 2022 15:35:50 +0200 |
wneuper |
cleanup *?PIDE 2: finished
|
changeset |
files
|
Fri, 21 Oct 2022 15:19:00 +0200 |
wneuper |
follow up 5e: finish adapt_to_type for Tactic, eliminate term2str in src
|
changeset |
files
|
Thu, 20 Oct 2022 12:12:18 +0200 |
wneuper |
cleanup *_PIDE 1: TermC
|
changeset |
files
|
Thu, 20 Oct 2022 10:47:52 +0200 |
wneuper |
cleanup: Test_Isac works perfectly
|
changeset |
files
|
Thu, 20 Oct 2022 10:23:38 +0200 |
wneuper |
followup 6a: tests run from @{context} without sessions
|
changeset |
files
|
Wed, 19 Oct 2022 15:39:15 +0200 |
wneuper |
cleanup 1: clarify adapt_to_type finished
|
changeset |
files
|
Wed, 19 Oct 2022 14:23:40 +0200 |
wneuper |
Test_Isac works -- hg rollback
|
changeset |
files
|
Wed, 19 Oct 2022 13:10:24 +0200 |
wneuper |
cleanup 1: clarify adapt_to_type for Prog_Tac
|
changeset |
files
|
Wed, 19 Oct 2022 10:43:04 +0200 |
wneuper |
eliminate term2str in src, Prog_Tac.*_adapt_to_type
|
changeset |
files
|
Sun, 09 Oct 2022 09:01:29 +0200 |
wneuper |
eliminate term2str in doc-isac
|
changeset |
files
|
Sun, 09 Oct 2022 07:44:22 +0200 |
wneuper |
eliminate term2str in test/*
|
changeset |
files
|
Sun, 09 Oct 2022 06:53:03 +0200 |
wneuper |
plan for different parse in src/* and test/*
|
changeset |
files
|
Sat, 08 Oct 2022 19:17:24 +0200 |
wneuper |
follow up 5d: Error_Pattern.fill_in also included to adapt_to_type
|
changeset |
files
|
Sat, 08 Oct 2022 15:57:10 +0200 |
wneuper |
follow up 5c: Error_Pattern is covered by MethodC.adapt_to_type
|
changeset |
files
|
Sat, 08 Oct 2022 15:41:11 +0200 |
wneuper |
more cleanup
|
changeset |
files
|
Sat, 08 Oct 2022 12:13:13 +0200 |
wneuper |
follow up 5b: more cleanup
|
changeset |
files
|
Sat, 08 Oct 2022 11:40:48 +0200 |
wneuper |
follow up 5: cleanup
|
changeset |
files
|
Fri, 07 Oct 2022 20:46:48 +0200 |
wneuper |
follow up 3: MethodC.adapt_to_typ on loading by CalcTree, CalcTreeTEST
|
changeset |
files
|
Thu, 29 Sep 2022 18:02:10 +0200 |
wneuper |
build clean -- rollback
|
changeset |
files
|
Mon, 26 Sep 2022 10:57:53 +0200 |
wneuper |
follow up 2: Problem.adapt_to_typ on loading by CalcTree, CalcTreeTEST
|
changeset |
files
|
Fri, 16 Sep 2022 12:13:23 +0200 |
wneuper |
follow up 1a: restrict concept to adaptation of types within pre-compiled terms
|
changeset |
files
|
Thu, 15 Sep 2022 10:07:12 +0200 |
wneuper |
follow up meeting Makarius 1: new concept of parsing within current ?ML_structure Context?
|
changeset |
files
|
Wed, 14 Sep 2022 11:33:10 +0200 |
wneuper |
uniform "_PIDE" for functions intermediate in Isabelle/Isac
|
changeset |
files
|
Tue, 13 Sep 2022 10:28:04 +0200 |
wneuper |
adaptation to mail
|
changeset |
files
|
Mon, 12 Sep 2022 18:02:44 +0200 |
wneuper |
eliminate KEStore_Elems.get_thes, add_thes 2: get_cas 2: cleanup finished
|
changeset |
files
|