| Wed, 25 Jan 2023 15:52:33 +0100 |
ContextC.build_while_parsing, improves O_Model.init_PIDE
|
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 15:06:40 +0100 |
eliminate use of Thy_Info 1: ThyC.get_theory in Specify_Step, Specify, Step_Specify
|
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 17:06:19 +0100 |
make Minisubplb/800-append-on-Frm.sml independent from Thy_Info
|
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 |
| Wed, 21 Dec 2022 18:48:23 +0100 |
make Minisubplb/710-interSteps-short.sml independent from Thy_Info
|
file | diff | annotate |
| Tue, 20 Dec 2022 08:11:26 +0100 |
before Tactic.input_to_string ctxt -- hg rollback
|
file | diff | annotate |
| Fri, 09 Dec 2022 13:51:02 +0100 |
make up to Minisubplb/700-interSteps.sml from Thy_Info (on Isabelle2021-1)
|
file | diff | annotate |
| Thu, 08 Dec 2022 17:55:45 +0100 |
make Minisubplb/400-start-meth-subpbl.sml from Thy_Info
|
file | diff | annotate |
| Thu, 08 Dec 2022 10:33:27 +0100 |
tuned files, Test_Isac.thy works
|
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 |
| Sun, 20 Nov 2022 08:40:46 +0100 |
make Minisubplb/250-Rewrite_Set-from-method* independent from Thy_Info
|
file | diff | annotate |
| Sat, 19 Nov 2022 17:00:59 +0100 |
make Minisubplb/200-start-method independent #5: prepreeding was 200-start-method-NEXT_STEP.sml
|
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 |
| Thu, 10 Nov 2022 14:25:38 +0100 |
make Minisubplb/200-start-method independent from Thy_Info #1
|
file | diff | annotate |
| Wed, 09 Nov 2022 15:15:24 +0100 |
rename Minisubpbl: in the future "a" indicates a "Maximum"-test
|
file | diff | annotate |
| Tue, 25 Oct 2022 17:44:08 +0200 |
polished
|
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 17:21:04 +0200 |
follow up 6a: eliminate Thy_Info.get_theory for Minisubplb/100-init-rootpbl.sml
|
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 10:43:04 +0200 |
eliminate term2str in src, Prog_Tac.*_adapt_to_type
|
file | diff | annotate |
| Sun, 09 Oct 2022 09:01:29 +0200 |
eliminate term2str in doc-isac
|
file | diff | annotate |
| Sat, 08 Oct 2022 12:13:13 +0200 |
follow up 5b: more cleanup
|
file | diff | annotate |
| Sat, 08 Oct 2022 11:40:48 +0200 |
follow up 5: cleanup
|
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 |
| Mon, 12 Sep 2022 18:02:44 +0200 |
eliminate KEStore_Elems.get_thes, add_thes 2: get_cas 2: cleanup finished
|
file | diff | annotate |
| Sun, 11 Sep 2022 14:31:15 +0200 |
resolve name clash in get_calc
|
file | diff | annotate |
| Fri, 05 Aug 2022 08:45:37 +0200 |
finish Calc_Binop, add signature EXAMPLE
|
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 |
| Sun, 31 Jul 2022 13:45:20 +0200 |
eliminate global flags of Check_Unique, LI_Tool
|
file | diff | annotate |
| Sun, 31 Jul 2022 13:23:38 +0200 |
eliminate global flag Check_Unique.on
|
file | diff | annotate |
| Fri, 27 May 2022 17:19:01 +0200 |
tuned
|
file | diff | annotate |
| Fri, 27 May 2022 15:12:54 +0200 |
replace literals with constants
|
file | diff | annotate |
| Tue, 01 Jun 2021 15:41:23 +0200 |
Test_Some.thy with looping ML<>
|
file | diff | annotate |
| Sun, 18 Apr 2021 18:30:31 +0200 |
proper test sessions, but with remaining failures;
|
file | diff | annotate |
| Fri, 16 Apr 2021 22:29:23 +0200 |
prefer symbolic directories $ISABELLE_ISAC and $ISABELLE_ISAC_TEST, instead of re-using ~~ for $ISABELLE_HOME;
|
file | diff | annotate |
| Sat, 03 Apr 2021 15:27:52 +0200 |
review and update directories in Build_Isac
|
file | diff | annotate |
| Fri, 22 Jan 2021 14:56:44 +0100 |
step 5.4: clarify dependencies of BridgeJEdit.thy
|
file | diff | annotate |
| Mon, 05 Oct 2020 12:16:16 +0200 |
Isabelle2019->20: adapt to new session requirements
|
file | diff | annotate |
| Sun, 02 Aug 2020 12:32:34 +0200 |
shift code from Test_Parse_Isac to src/
|
file | diff | annotate |
| Sun, 24 May 2020 16:05:36 +0200 |
prep.resolve hacks introduced with funpack, part 1
|
file | diff | annotate |
| Wed, 20 May 2020 12:52:09 +0200 |
standard format for string lists
|
file | diff | annotate |
| Mon, 11 May 2020 12:25:52 +0200 |
introduce Pre_Conds.T
|
file | diff | annotate |
| Sat, 09 May 2020 11:55:51 +0200 |
shift code to Input_Descript, rename identifiers (+ keep old)
|
file | diff | annotate |
| Mon, 04 May 2020 13:27:45 +0200 |
remove unused code
|
file | diff | annotate |
| Wed, 29 Apr 2020 09:03:01 +0200 |
comments on relation between files.
|
file | diff | annotate |
| Tue, 28 Apr 2020 19:39:06 +0200 |
move code from struct.Celem to appropriate struct.s
|
file | diff | annotate |
| Wed, 22 Apr 2020 16:01:53 +0200 |
use "Check_Unique" 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 |
| Wed, 22 Apr 2020 11:06:48 +0200 |
shift Unsynchronized.ref for tracing to respect.struct.
|
file | diff | annotate |
| Mon, 20 Apr 2020 15:54:19 +0200 |
separate Check_Unique, an exercise in higher order funs
|
file | diff | annotate |
| Sun, 19 Apr 2020 12:22:37 +0200 |
rename KEStore to Know_Store, replace respect.part of Celem with Celem1
|
file | diff | annotate |
| Wed, 15 Apr 2020 11:37:43 +0200 |
cleanup
|
file | diff | annotate |