| Thu, 16 Nov 2023 08:15:46 +0100 |
prepare 14: improved item_to_add
|
file | diff | annotate |
| Sat, 04 Mar 2023 19:02:39 +0100 |
PIDE turn 9a: handle empty input correct
|
file | diff | annotate |
| Sun, 12 Feb 2023 12:44:25 +0100 |
move code from LibraryC to approptiate structures
|
file | diff | annotate |
| Wed, 08 Feb 2023 08:59:37 +0100 |
rollback
|
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 |
| Sat, 04 Feb 2023 11:21:56 +0100 |
eliminate use of Thy_Info 20: cleanup Subst.*, detect design flaw in fun eval_*
|
file | diff | annotate |
| Wed, 19 Oct 2022 14:23:40 +0200 |
Test_Isac works -- hg rollback
|
file | diff | annotate |
| Wed, 19 Oct 2022 10:43:04 +0200 |
eliminate term2str in src, Prog_Tac.*_adapt_to_type
|
file | diff | annotate |
| Wed, 03 Aug 2022 13:22:36 +0200 |
replace val example_store = Unsynchronized.ref by Thy_Data
|
file | diff | annotate |
| Mon, 27 Sep 2021 20:24:24 +0200 |
cleanup; all relevant tests work again
|
file | diff | annotate |
| Mon, 27 Sep 2021 13:17:52 +0200 |
tuned
|
file | diff | annotate |
| Mon, 27 Sep 2021 13:14:09 +0200 |
simp rules for realpow appear complete
|
file | diff | annotate |
| Sun, 26 Sep 2021 20:58:57 +0200 |
another simp rule missing; lemma realpow_uminus_simps fails.
|
file | diff | annotate |
| Sat, 25 Sep 2021 21:41:51 +0200 |
more simp rules: 1 is another special case, so (- 1) needs to be treated separately;
|
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 |
| Tue, 10 Aug 2021 11:01:18 +0200 |
eliminate ThyC.to_ctxt, use Proof_Context.init_global inline
|
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 |
| 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 |
| Fri, 08 May 2020 18:30:21 +0200 |
cleanup O_Model
|
file | diff | annotate |
| Tue, 28 Apr 2020 19:39:06 +0200 |
move code from struct.Celem to appropriate struct.s
|
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 |
| Wed, 22 Apr 2020 11:06:48 +0200 |
shift Unsynchronized.ref for tracing to respect.struct.
|
file | diff | annotate |
| Tue, 21 Apr 2020 10:13:30 +0200 |
derive Problem from Probl_Def, drop funs and types used by Know_Store
|
file | diff | annotate |
| Sun, 19 Apr 2020 15:51:31 +0200 |
run Know_Store independent from Celem. in calcelements.sml
|
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 |
| Mon, 13 Apr 2020 15:31:23 +0200 |
reorganise struct. ThmC, part 1
|
file | diff | annotate |
| Fri, 10 Apr 2020 15:02:50 +0200 |
rename directory CalcElements to BaseDefinitions
|
file | diff | annotate | base |