| Wed, 11 Jan 2023 11:38:01 +0100 |
eliminate use of Thy_Info 12: TermC partially
|
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 |
| Wed, 11 Jan 2023 06:06:12 +0100 |
eliminate use of Thy_Info 11: arg. ctxt for ThmC.string_of_thm/s
|
file | diff | annotate |
| Sun, 08 Jan 2023 10:30:58 +0100 |
eliminate use of Thy_Info 3> improved LItool.tac_from_prog
|
file | diff | annotate |
| Fri, 06 Jan 2023 11:32:57 +0100 |
eliminate thy-hierarchy 5, end: remove Thy_Write
|
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 |
| Thu, 15 Dec 2022 13:03:51 +0100 |
proper indication of error-msg "Wrong descriptor" in problem/method
|
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, 16 Nov 2022 17:42:41 +0100 |
make Minisubplb/200-start-method independent #3: Rewrite_Ord.T with ctxt
|
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 |
| Mon, 07 Nov 2022 19:58:01 +0100 |
rename KEstore_Elems to Know_Store
|
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 |
| Thu, 20 Oct 2022 10:47:52 +0200 |
cleanup: Test_Isac works perfectly
|
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 |
| Fri, 07 Oct 2022 20:46:48 +0200 |
follow up 3: MethodC.adapt_to_typ on loading by CalcTree, CalcTreeTEST
|
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 |
| Sat, 06 Aug 2022 15:02:55 +0200 |
eliminate union_overwrite and use standard namespace merge
|
file | diff | annotate |
| Fri, 05 Aug 2022 12:30:16 +0200 |
push Proof.context through Eval.adhoc_thm
|
file | diff | annotate |
| Wed, 03 Aug 2022 17:18:47 +0200 |
replace val rew_ord' = Unsynchronized.ref by Theory_Data
|
file | diff | annotate |
| Sat, 30 Jul 2022 16:47:45 +0200 |
eliminate global flag Rewrite.trace_on
|
file | diff | annotate |
| Sun, 19 Jun 2022 16:55:13 +0200 |
shifts tests to VSCode_Example.thy, vscode-example.sml
|
file | diff | annotate |
| Sat, 18 Jun 2022 12:34:29 +0200 |
adapth thy to Demo_Example
|
file | diff | annotate |
| Thu, 26 May 2022 12:44:51 +0200 |
unify parse 6': TermC.parse eliminated, Test_Isac ok
|
file | diff | annotate |
| Fri, 06 Aug 2021 18:27:05 +0200 |
cleanup files on GCD/gcd
|
file | diff | annotate |
| Thu, 22 Apr 2021 21:34:20 +0200 |
purge XML output from pbl- and met-hierarchies, coarse part
|
file | diff | annotate |
| Thu, 22 Apr 2021 16:49:41 +0200 |
purge code for input to Kernel
|
file | diff | annotate |
| Mon, 19 Apr 2021 20:33:04 +0200 |
obsolete;
|
file | diff | annotate |
| Mon, 19 Apr 2021 19:55:31 +0200 |
no \<^isac_test> guard for test material: thus the Prover IDE does not have to switch the option "isac_test";
|
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 |
| 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 |
| Wed, 09 Dec 2020 14:37:10 +0100 |
step 3.2: prep.data for start of specify-phase
|
file | diff | annotate |
| Wed, 09 Dec 2020 14:22:24 +0100 |
adopt new theory identifier also in comments
|
file | diff | annotate |
| Mon, 26 Oct 2020 13:52:26 +0100 |
copy Outer_Syntax.command..spark_open as model for Isac Calculation
|
file | diff | annotate |
| Thu, 22 Oct 2020 15:40:41 +0200 |
complete imports to Test_Isac*
|
file | diff | annotate |
| Fri, 17 Jul 2020 11:42:20 +0200 |
cleanup Test_Parse*, start parsers for keyword ISAC
|
file | diff | annotate |
| Mon, 29 Jun 2020 17:27:34 +0200 |
new test me' doesn't overload jEdit buffers
|
file | diff | annotate |
| Wed, 03 Jun 2020 11:25:19 +0200 |
follow 2 ancient updates of Library.ML
|
file | diff | annotate |
| Tue, 19 May 2020 12:33:35 +0200 |
adapt test/../Specify/* to new files in src/../Specify/*
|
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 13:33:47 +0200 |
rename Specification -> References, contiued
|
file | diff | annotate |
| Thu, 14 May 2020 09:30:40 +0200 |
start renaming Specification -> References;
|
file | diff | annotate |
| Wed, 13 May 2020 11:34:05 +0200 |
shift code from struct.Specify to appropriate locations
|
file | diff | annotate |
| Tue, 12 May 2020 07:27:21 +0200 |
remove Specify/mstools.sml
|
file | diff | annotate |
| Mon, 11 May 2020 20:49:27 +0200 |
prep. remove Specify/mstools.sml
|
file | diff | annotate |
| Sun, 10 May 2020 17:26:36 +0200 |
cleanup generate.sml, model.sml
|
file | diff | annotate |
| Sun, 10 May 2020 13:16:56 +0200 |
investigate I_Model
|
file | diff | annotate |
| Tue, 05 May 2020 09:07:36 +0200 |
separate struc.Formalise
|
file | diff | annotate |
| Mon, 04 May 2020 13:27:45 +0200 |
remove unused code
|
file | diff | annotate |
| Wed, 29 Apr 2020 12:30:51 +0200 |
prep. separation of check Applicable between specify-phase and solve-phase
|
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 |
| Tue, 28 Apr 2020 15:31:49 +0200 |
assign code from Rtools to appropriate struct.s
|
file | diff | annotate |
| Mon, 27 Apr 2020 12:36:21 +0200 |
separate struct.Subst, rename idenfitiers
|
file | diff | annotate |
| Fri, 24 Apr 2020 08:51:05 +0200 |
separate struct.Error_Pattern, rename identifiers
|
file | diff | annotate |
| Thu, 23 Apr 2020 09:29:56 +0200 |
separate struct. Derive
|
file | diff | annotate |
| Wed, 22 Apr 2020 11:23:30 +0200 |
rename file according to struct.; start renaming with "Spec"
|
file | diff | annotate |
| Mon, 20 Apr 2020 15:54:19 +0200 |
separate Check_Unique, an exercise in higher order funs
|
file | diff | annotate |