| Fri, 24 Nov 2023 15:34:07 +0100 |
followup 3: repair new fill_from_o, uncomment maximum of tests
|
file | diff | annotate |
| Mon, 20 Nov 2023 10:49:54 +0100 |
followup 2: un-comment / investigate tests, part.review TODO.md
|
file | diff | annotate |
| Thu, 16 Nov 2023 08:15:46 +0100 |
prepare 14: improved item_to_add
|
file | diff | annotate |
| Tue, 23 May 2023 07:56:29 +0200 |
rollback
|
file | diff | annotate |
| Fri, 31 Mar 2023 12:07:52 +0200 |
//new Pre_Conds.check/_TEST breaks tests, need new signature
|
file | diff | annotate |
| Sun, 12 Feb 2023 12:44:25 +0100 |
move code from LibraryC to approptiate structures
|
file | diff | annotate |
| Tue, 07 Feb 2023 18:32:58 +0100 |
improve previous changeset
|
file | diff | annotate |
| Tue, 07 Feb 2023 18:05:15 +0100 |
unify ctxt for ERROR
|
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 |
| Tue, 31 Jan 2023 11:23:16 +0100 |
cleanup parse #7: eliminate TermC.parseNEW*; cleanup finished
|
file | diff | annotate |
| Tue, 31 Jan 2023 10:49:17 +0100 |
cleanup parse #6: eliminate TermC.parseNEW
|
file | diff | annotate |
| Mon, 30 Jan 2023 12:38:17 +0100 |
cleanup parse #5: eliminate TermC.parse_patt
|
file | diff | annotate |
| Mon, 30 Jan 2023 12:11:40 +0100 |
cleanup parse #4: eliminate TermC.parse
|
file | diff | annotate |
| Mon, 30 Jan 2023 09:47:18 +0100 |
cleanup parse #3: final functions inb ParseC
|
file | diff | annotate |
| Sat, 28 Jan 2023 13:21:39 +0100 |
cleanup parse #1: start eliminate parseNEW
|
file | diff | annotate |
| Wed, 25 Jan 2023 15:52:33 +0100 |
ContextC.build_while_parsing, improves O_Model.init_PIDE
|
file | diff | annotate |
| 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 |
| Mon, 07 Nov 2022 17:37:20 +0100 |
rename fields in Method_Def.T
|
file | diff | annotate |
| Mon, 31 Oct 2022 18:28:36 +0100 |
rename fields in Probl_Def.T
|
file | diff | annotate |
| Mon, 31 Oct 2022 16:53:59 +0100 |
delete forgotten code
|
file | diff | annotate |
| Fri, 21 Oct 2022 15:19:00 +0200 |
follow up 5e: finish adapt_to_type for Tactic, eliminate term2str in src
|
file | diff | annotate |
| Thu, 20 Oct 2022 12:12:18 +0200 |
cleanup *_PIDE 1: TermC
|
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 07:44:22 +0200 |
eliminate term2str in test/*
|
file | diff | annotate |
| Sun, 09 Oct 2022 06:53:03 +0200 |
plan for different parse in src/* and test/*
|
file | diff | annotate |
| Sat, 08 Oct 2022 15:41:11 +0200 |
more cleanup
|
file | diff | annotate |
| Sat, 08 Oct 2022 11:40:48 +0200 |
follow up 5: cleanup
|
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 |
| Tue, 21 Jun 2022 16:04:43 +0200 |
rename functions in i-model.sml
|
file | diff | annotate |
| Fri, 27 May 2022 17:14:49 +0200 |
tuned
|
file | diff | annotate |
| Thu, 26 May 2022 12:44:51 +0200 |
unify parse 6': TermC.parse eliminated, Test_Isac ok
|
file | diff | annotate |
| Wed, 29 Sep 2021 19:34:32 +0200 |
unify parse 3: eliminate parseN
|
file | diff | annotate |
| Wed, 29 Sep 2021 19:26:12 +0200 |
unify parse 2: eliminate parseold
|
file | diff | annotate |
| Wed, 29 Sep 2021 18:56:38 +0200 |
unify parse 1: reorder defs
|
file | diff | annotate |
| Thu, 16 Sep 2021 17:23:54 +0200 |
separate realpow constant, with additional cases not covered by Transcendental.powr;
|
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 14:28:38 +0200 |
repair fun adhoc_thm + fun eval_cancel
|
file | diff | annotate |
| Wed, 18 Aug 2021 20:34:41 +0200 |
replace is_const with is_num, ERROR removed
|
file | diff | annotate |
| Wed, 18 Aug 2021 16:46:22 +0200 |
\\re-establish is_const DOES NOT REMOVE THE STRANGE ERROR
|
file | diff | annotate |
| Wed, 18 Aug 2021 16:03:08 +0200 |
\\replace is_const with is_num: STRANGE ERROR assoc_calc: 'Prog_Expr.is_num' not found in theory Poly
|
file | diff | annotate |
| Tue, 17 Aug 2021 22:50:20 +0200 |
prefer existing signed_string_of_int;
|
file | diff | annotate |
| Tue, 10 Aug 2021 11:01:18 +0200 |
eliminate ThyC.to_ctxt, use Proof_Context.init_global inline
|
file | diff | annotate |
| Mon, 09 Aug 2021 11:19:25 +0200 |
remove TOODOOs
|
file | diff | annotate |
| Mon, 02 Aug 2021 11:38:40 +0200 |
repair thm real_mult_minus1_sym; many newly broken tests
|
file | diff | annotate |
| Tue, 27 Jul 2021 11:21:14 +0200 |
revert previous changeset
|
file | diff | annotate |
| Tue, 20 Jul 2021 14:37:56 +0200 |
//reduce the number of TermC.parse*; "//"means: tests broken .
|
file | diff | annotate |
| Mon, 19 Jul 2021 18:29:46 +0200 |
cleanup after "eliminate ThmC.numerals_to_Free"
|
file | diff | annotate |
| Mon, 19 Jul 2021 15:34:54 +0200 |
ALL const_name replaces (others cannot be replaced)
|
file | diff | annotate |
| Sun, 18 Jul 2021 21:15:21 +0200 |
Test_Isac_Short.thy, Test_Some.the work on new src, new TOODOOs
|
file | diff | annotate |
| Sun, 18 Jul 2021 18:15:27 +0200 |
merged
|
file | diff | annotate |
| Thu, 15 Jul 2021 14:10:18 +0200 |
ewrite.sml + poly.sml + rational.sml: ok, repair rewrite-orders
|
file | diff | annotate |
| Tue, 13 Jul 2021 10:43:21 +0200 |
Test_Some.thy + rewrite.sml + poly.sml ok: improve eval_is_atom
|
file | diff | annotate |
| Tue, 13 Jul 2021 08:52:35 +0200 |
Test_Some.thy + rewrite.sml + poly.sml ok: real_mult_minus1_sym works with is_atom
|
file | diff | annotate |
| Tue, 01 Jun 2021 15:41:23 +0200 |
Test_Some.thy with looping ML<>
|
file | diff | annotate |
| Mon, 21 Jun 2021 15:42:53 +0200 |
proper formal names for consts/types, *with* change of semantics;
|
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 |
| Tue, 15 Jun 2021 22:24:20 +0200 |
Isar command 'method' as combination of KEStore_Elems.add_mets + MethodC.prep_import, without change of semantics;
|
file | diff | annotate |
| Fri, 07 May 2021 18:12:51 +0200 |
* WN: simplify const names like "is'_expanded"
|
file | diff | annotate |