| Sun, 31 Jul 2022 16:35:33 +0200 |
eliminate global flag Eval.trace_on
|
file | diff | annotate |
| Wed, 01 Jun 2022 14:17:23 +0200 |
Calculation 6: separate "Problem" and "Problem_Ref"
|
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 |
| 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 |
| Wed, 18 Aug 2021 11:35:24 +0200 |
repair test/../root.sml, diff.sml; outcomment NEW errors TOODOO.1
|
file | diff | annotate |
| Tue, 10 Aug 2021 09:43:07 +0200 |
complete replacement of Rule.Thm/Eval by \<^rule_thm> and \<^rule_eval> in src/*
|
file | diff | annotate |
| Mon, 02 Aug 2021 15:25:49 +0200 |
reapir minus_mult_left, many tests work again
|
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 12:32:43 +0200 |
//test/../diff.sml works again
|
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 15:28:43 +0200 |
Test_Some.thy + rewrite.sml + poly.sml + rational.sml: ok
|
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 09:49:45 +0200 |
Test_Some.thy + rewrite.sml + poly.sml ok: shift code Test_Some.thy --> Poly.thy
|
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 |
| Sat, 03 Jul 2021 16:21:07 +0200 |
//test/../rewrite.sml,poly.sml WORK
|
file | diff | annotate |
| Tue, 01 Jun 2021 15:41:23 +0200 |
Test_Some.thy with looping ML<>
|
file | diff | annotate |
| Mon, 21 Jun 2021 20:06:12 +0200 |
Isar command 'calculation' as front-end for KEStore_Elems.add_calcs, without change of semantics;
|
file | diff | annotate |
| Mon, 21 Jun 2021 16:18:27 +0200 |
more antiquotations, without 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 |
| Sun, 20 Jun 2021 16:26:18 +0200 |
Isar command 'problem' as combination of KEStore_Elems.add_pbts + Problem.prep_import, 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 |
| Sat, 12 Jun 2021 18:22:07 +0200 |
use more antiquotations;
|
file | diff | annotate |
| Sat, 12 Jun 2021 18:06:27 +0200 |
use more antiquotations;
|
file | diff | annotate |
| Sat, 12 Jun 2021 14:29:10 +0200 |
ML antiquotations for Rule.Thm, with special treatment of symmetric rule;
|
file | diff | annotate |
| Fri, 11 Jun 2021 11:49:34 +0200 |
ML antiquotation for formally checked Rule.Eval;
|
file | diff | annotate |
| Thu, 10 Jun 2021 12:48:50 +0200 |
clarified theory context: avoid global "val thy = ..." hanging around (left-over from Isabelle2005), which is apt to various pitfalls;
|
file | diff | annotate |
| Thu, 10 Jun 2021 12:23:57 +0200 |
clarified theory context: from current command instead of earlier state;
|
file | diff | annotate |
| Thu, 10 Jun 2021 11:54:20 +0200 |
clarified command name: this is to register already defined rule sets in the Knowledge Store;
|
file | diff | annotate |
| Wed, 26 May 2021 16:24:05 +0200 |
command 'setup_rule' semantic equivalent for KEStore_Elems.add_rlss;
|
file | diff | annotate |
| Fri, 07 May 2021 18:12:51 +0200 |
* WN: simplify const names like "is'_expanded"
|
file | diff | annotate |
| Mon, 03 May 2021 08:49:50 +0200 |
replace Isac's power with Isabelle's Transcendental.powr
|
file | diff | annotate |
| Sun, 25 Apr 2021 12:49:37 +0200 |
cleanup remaining ^^^ in comments, finished (?)
|
file | diff | annotate |
| Tue, 20 Apr 2021 16:58:44 +0200 |
replace power ^^^ by \<up>
|
file | diff | annotate |
| Wed, 03 Feb 2021 16:39:44 +0100 |
Isac's MethodC not shadowing Isabelle's Method
|
file | diff | annotate |
| Wed, 20 May 2020 12:52:09 +0200 |
standard format for string lists
|
file | diff | annotate |
| Wed, 13 May 2020 16:10:22 +0200 |
shift code from Specify to Problem, Method, Test_Tool
|
file | diff | annotate |
| Mon, 11 May 2020 11:38:52 +0200 |
error -> raise ERROR
|
file | diff | annotate |
| Fri, 24 Apr 2020 09:01:48 +0200 |
tuned
|
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 12:22:37 +0200 |
rename KEStore to Know_Store, replace respect.part of Celem with Celem1
|
file | diff | annotate |
| Wed, 15 Apr 2020 18:00:58 +0200 |
collect code in ThyC
|
file | diff | annotate |
| Wed, 15 Apr 2020 11:37:43 +0200 |
cleanup
|
file | diff | annotate |
| Wed, 15 Apr 2020 11:11:54 +0200 |
cleanup handling of ThmC.sym_thm
|
file | diff | annotate |
| Tue, 14 Apr 2020 15:56:15 +0200 |
use "ThmC_Def" for renaming identifiers
|
file | diff | annotate |
| Mon, 13 Apr 2020 15:31:23 +0200 |
reorganise struct. ThmC, part 1
|
file | diff | annotate |
| Mon, 13 Apr 2020 13:27:55 +0200 |
improve renaming
|
file | diff | annotate |
| Fri, 10 Apr 2020 18:32:36 +0200 |
use "UnparseC" for renaming identifiers
|
file | diff | annotate |
| Thu, 09 Apr 2020 18:21:09 +0200 |
rearrange code in Rule_Set and Rule
|
file | diff | annotate |
| Thu, 09 Apr 2020 17:13:17 +0200 |
separate struct. UnparseC, shift code to ThmC
|
file | diff | annotate |
| Wed, 08 Apr 2020 16:56:47 +0200 |
separate struct Rewrite_Ord
|
file | diff | annotate |
| Wed, 08 Apr 2020 12:32:51 +0200 |
use new struct "Rule_Set" for renaming identifiers
|
file | diff | annotate |
| Mon, 06 Apr 2020 11:44:36 +0200 |
use "Rule_Set" for shorter identifiers
|
file | diff | annotate |