Tue, 07 Feb 2023 17:25:09 +0100 |
eliminate use of Thy_Info 23: ThyC.get_theory ctxt is mandadory
|
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 |
Tue, 31 Jan 2023 12:29:42 +0100 |
eliminate use of Thy_Info 13: eliminate UnparseC.term in test/
|
file | diff | annotate |
Tue, 31 Jan 2023 10:49:17 +0100 |
cleanup parse #6: eliminate TermC.parseNEW
|
file | diff | annotate |
Mon, 30 Jan 2023 09:47:18 +0100 |
cleanup parse #3: final functions inb ParseC
|
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 06:06:12 +0100 |
eliminate use of Thy_Info 11: arg. ctxt for ThmC.string_of_thm/s
|
file | diff | annotate |
Mon, 07 Nov 2022 19:58:01 +0100 |
rename KEstore_Elems to Know_Store
|
file | diff | annotate |
Thu, 20 Oct 2022 10:23:38 +0200 |
followup 6a: tests run from @{context} without sessions
|
file | diff | annotate |
Sun, 09 Oct 2022 07:44:22 +0200 |
eliminate term2str in test/*
|
file | diff | annotate |
Mon, 12 Sep 2022 17:46:32 +0200 |
eliminate KEStore_Elems.get_thes, add_thes 2: get_cas 1: Test_Isac ok
|
file | diff | annotate |
Wed, 24 Aug 2022 19:02:19 +0200 |
use Eval.* instead of Eval_Def.* wherever possible
|
file | diff | annotate |
Wed, 24 Aug 2022 18:29:33 +0200 |
polish naming in structure Eval
|
file | diff | annotate |
Fri, 05 Aug 2022 12:30:16 +0200 |
push Proof.context through Eval.adhoc_thm
|
file | diff | annotate |
Fri, 05 Aug 2022 08:45:37 +0200 |
finish Calc_Binop, add signature EXAMPLE
|
file | diff | annotate |
Thu, 04 Aug 2022 12:48:37 +0200 |
polish naming in Rewrite_Order
|
file | diff | annotate |
Sun, 31 Jul 2022 16:35:33 +0200 |
eliminate global flag Eval.trace_on
|
file | diff | annotate |
Sat, 30 Jul 2022 16:47:45 +0200 |
eliminate global flag Rewrite.trace_on
|
file | diff | annotate |
Thu, 26 May 2022 12:44:51 +0200 |
unify parse 6': TermC.parse eliminated, Test_Isac ok
|
file | diff | annotate |
Fri, 24 Sep 2021 14:18:10 +0200 |
proper simp_ctxt;
|
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, 14 Sep 2021 12:22:57 +0200 |
\\adopt Isabelles calculation of numerals, some cases are missing
|
file | diff | annotate |
Mon, 23 Aug 2021 14:24:06 +0200 |
repair rule-set reduce_0_1_2
|
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 |
Tue, 17 Aug 2021 21:57:40 +0200 |
make "sqrt" work by proper use of HOLogic.dest_number and its resulting type;
|
file | diff | annotate |
Mon, 09 Aug 2021 14:20:20 +0200 |
eliminate ThyC.to_ctxt done except 1 error
|
file | diff | annotate |
Mon, 09 Aug 2021 11:19:25 +0200 |
remove TOODOOs
|
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 17:29:35 +0200 |
introduce ALL valid const_name in test/*
|
file | diff | annotate |
Sun, 18 Jul 2021 18:15:27 +0200 |
merged
|
file | diff | annotate |
Sun, 18 Jul 2021 16:20:32 +0200 |
eliminate ThmC.numerals_to_Free: Test_Isac_Short.thy works with TOODOO s
|
file | diff | annotate |
Sat, 17 Jul 2021 14:05:28 +0200 |
replace "-*" by "- *" for numerals "*" in test/*
|
file | diff | annotate |
Thu, 15 Jul 2021 14:10:18 +0200 |
ewrite.sml + poly.sml + rational.sml: ok, repair rewrite-orders
|
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 15:36:09 +0200 |
more antiquotations for Isabelle/HOL consts/types, 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 |
Mon, 03 May 2021 08:49:50 +0200 |
replace Isac's power with Isabelle's Transcendental.powr
|
file | diff | annotate |
Thu, 29 Apr 2021 17:05:11 +0200 |
repair test broken in previous changeset
|
file | diff | annotate |
Thu, 29 Apr 2021 17:02:10 +0200 |
eliminate "handle _ => ..." finished
|
file | diff | annotate |
Tue, 20 Apr 2021 16:58:44 +0200 |
replace power ^^^ by \<up>
|
file | diff | annotate |
Mon, 19 Apr 2021 15:02:00 +0200 |
long identifiers for occurences in test/../termC.sml
|
file | diff | annotate |
Wed, 20 May 2020 12:52:09 +0200 |
standard format for string lists
|
file | diff | annotate |
Sun, 10 May 2020 17:26:36 +0200 |
cleanup generate.sml, model.sml
|
file | diff | annotate |
Wed, 29 Apr 2020 09:03:01 +0200 |
comments on relation between files.
|
file | diff | annotate |
Wed, 22 Apr 2020 11:23:30 +0200 |
rename file according to struct.; start renaming with "Spec"
|
file | diff | annotate | base |