| Wed, 27 Sep 2023 12:17:44 +0200 |
prepare 9: I_Model.complete* all replaced by I_Model.s_make_complete
|
file | diff | annotate |
| Tue, 26 Sep 2023 15:57:12 +0200 |
rollback
|
file | diff | annotate |
| Mon, 18 Sep 2023 08:38:33 +0200 |
prepare 3: shift new code
|
file | diff | annotate |
| Wed, 30 Aug 2023 06:37:56 +0200 |
prepare 2: I_Model.of_max_variant ready for use in I_Model.complete
|
file | diff | annotate |
| Tue, 23 May 2023 07:56:29 +0200 |
rollback
|
file | diff | annotate |
| Tue, 07 Feb 2023 18:32:58 +0100 |
improve previous changeset
|
file | diff | annotate |
| Sat, 04 Feb 2023 17:00:25 +0100 |
eliminate use of Thy_Info 22: eliminate UnparseC.term, rename "_in_ctxt" -> ""
|
file | diff | annotate |
| Sat, 04 Feb 2023 16:20:45 +0100 |
eliminate use of Thy_Info 21: replace Unparse.term, TermC.unparse_ERROR for far off ctxt
|
file | diff | annotate |
| Thu, 26 Jan 2023 18:54:25 +0100 |
use exclusively some new *.to_string ctxt
|
file | diff | annotate |
| Tue, 10 Jan 2023 10:01:05 +0100 |
eliminate use of Thy_Info 9: arg. ctxt for Rule.to_string, Istate.to_string
|
file | diff | annotate |
| Sun, 08 Jan 2023 17:26:00 +0100 |
eliminate use of Thy_Info 6: improve ctxt in fetchProposedTactic, Error_Pattern, etc
|
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 |
| Thu, 22 Dec 2022 17:06:19 +0100 |
make Minisubplb/800-append-on-Frm.sml independent from Thy_Info
|
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:16:40 +0100 |
make Minisubplb/300-init-subpbl.sml independent from Thy_Info
|
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 |
| 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 17:37:20 +0100 |
rename fields in Method_Def.T
|
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 |
| Wed, 19 Oct 2022 10:43:04 +0200 |
eliminate term2str in src, Prog_Tac.*_adapt_to_type
|
file | diff | annotate |
| Sat, 08 Oct 2022 11:40:48 +0200 |
follow up 5: cleanup
|
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 |
| Thu, 29 Sep 2022 18:02:10 +0200 |
build clean -- rollback
|
file | diff | annotate |
| Wed, 07 Sep 2022 14:51:58 +0200 |
eliminate KEStore_Elems.get_thes, add_thes 1: get_rls 2: shift parent_node
|
file | diff | annotate |
| Mon, 22 Aug 2022 13:39:32 +0200 |
push ctxt through LI (Lucas-Interpreter)
|
file | diff | annotate |
| Sun, 21 Aug 2022 11:22:04 +0200 |
//prepare test 3 for: push ctxt through LI (only CAS_Cmd not OK)
|
file | diff | annotate |
| Sat, 06 Aug 2022 18:50:43 +0200 |
push Proof.context through Derive.steps, note HACK
|
file | diff | annotate |
| Sat, 30 Jul 2022 16:47:45 +0200 |
eliminate global flag Rewrite.trace_on
|
file | diff | annotate |
| Mon, 13 Sep 2021 16:01:48 +0200 |
cleanup TOODOOs from eliminate ThmC.numerals_to_Free
|
file | diff | annotate |
| Sun, 22 Aug 2021 09:43:43 +0200 |
improvement in Rational.thy makes several testfiles run, breaks one.
|
file | diff | annotate |
| Mon, 19 Jul 2021 15:34:54 +0200 |
ALL const_name replaces (others cannot be replaced)
|
file | diff | annotate |
| Mon, 21 Jun 2021 15:36:09 +0200 |
more antiquotations for Isabelle/HOL consts/types, without change of semantics;
|
file | diff | annotate |
| Wed, 21 Apr 2021 11:47:30 +0200 |
check remaining "for tests only" wrt. \<^isac_test>CARTOUCHE
|
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 |
| Wed, 03 Feb 2021 16:39:44 +0100 |
Isac's MethodC not shadowing Isabelle's Method
|
file | diff | annotate |
| Mon, 29 Jun 2020 16:01:01 +0200 |
renamings for Isabelle WS
|
file | diff | annotate |
| Mon, 29 Jun 2020 15:43:35 +0200 |
code polishing
|
file | diff | annotate |
| Sat, 30 May 2020 16:18:01 +0200 |
remove hacks, finally
|
file | diff | annotate |
| Wed, 20 May 2020 12:52:09 +0200 |
standard format for string lists
|
file | diff | annotate |
| Mon, 18 May 2020 11:48:27 +0200 |
shift code from Specification to Specify
|
file | diff | annotate |
| Sat, 16 May 2020 16:23:24 +0200 |
shift code from Specification to I_Model, rename ids
|
file | diff | annotate |
| Thu, 14 May 2020 16:08:41 +0200 |
shift code Specification --> Calc
|
file | diff | annotate |
| Thu, 14 May 2020 13:33:47 +0200 |
rename Specification -> References, contiued
|
file | diff | annotate |
| Thu, 14 May 2020 08:49:08 +0200 |
shift 2 preliminary hacks close to usage
|
file | diff | annotate |
| Tue, 12 May 2020 17:42:29 +0200 |
shift code from struct.Specify to appropriate locations
|
file | diff | annotate |
| Mon, 11 May 2020 11:38:52 +0200 |
error -> raise ERROR
|
file | diff | annotate |
| Mon, 04 May 2020 11:13:16 +0200 |
cleanup struct.Derive
|
file | diff | annotate |
| Mon, 04 May 2020 09:25:51 +0200 |
separate Solve_Step.add, rearrange code, prep. Specify_Step
|
file | diff | annotate |
| Sat, 02 May 2020 15:41:27 +0200 |
simplify Solve_Step.check, remove CAScmd (is not a tactic)
|
file | diff | annotate |
| Fri, 01 May 2020 15:28:40 +0200 |
separate Solve_Step.check, repair ALL of Test_Isac_Short
|
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 |
| Thu, 23 Apr 2020 15:48:31 +0200 |
separate struct.State_Steps, rename
|
file | diff | annotate |
| Thu, 23 Apr 2020 12:34:54 +0200 |
use "Derive" for renaming identifiers
|
file | diff | annotate |
| Thu, 23 Apr 2020 09:29:56 +0200 |
separate struct. Derive
|
file | diff | annotate |
| Wed, 22 Apr 2020 14:36:27 +0200 |
use "Spec", "Problem", "Method" for renaming identifiers
|
file | diff | annotate |
| Tue, 21 Apr 2020 15:42:50 +0200 |
replace Celem. with new struct.s in BaseDefinitions/
|
file | diff | annotate |
| Sun, 19 Apr 2020 11:07:02 +0200 |
switch "activate for Test_Isac .." back to Build_Isac
|
file | diff | annotate |
| Fri, 17 Apr 2020 18:47:29 +0200 |
Test_Isac_Short OK (except the 2 strange errors)
|
file | diff | annotate |
| Wed, 15 Apr 2020 18:00:58 +0200 |
collect code in ThyC
|
file | diff | annotate |