| Wed, 22 Apr 2020 11:06:48 +0200 |
shift Unsynchronized.ref for tracing to respect.struct.
|
file | diff | annotate |
| Tue, 21 Apr 2020 16:53:17 +0200 |
Test_Isac_Short now ok.
|
file | diff | annotate |
| Wed, 15 Apr 2020 11:11:54 +0200 |
cleanup handling of ThmC.sym_thm
|
file | diff | annotate |
| Wed, 15 Apr 2020 10:07:43 +0200 |
use "ThmC" for renaming identifiers
|
file | diff | annotate |
| Tue, 14 Apr 2020 15:56:15 +0200 |
use "ThmC_Def" for renaming identifiers
|
file | diff | annotate |
| Tue, 14 Apr 2020 12:39:26 +0200 |
reorganise struct. ThmC, part 3 end
|
file | diff | annotate |
| Mon, 13 Apr 2020 15:31:23 +0200 |
reorganise struct. ThmC, part 1
|
file | diff | annotate |
| Fri, 10 Apr 2020 18:32:36 +0200 |
use "UnparseC" for renaming identifiers
|
file | diff | annotate |
| Fri, 10 Apr 2020 16:16:09 +0200 |
use "Rule" and "Rule_Set" for renaming identifiers
|
file | diff | annotate |
| Fri, 10 Apr 2020 14:46:55 +0200 |
rearrange code for ThmC
|
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 12:32:51 +0200 |
use new struct "Rule_Set" for renaming identifiers
|
file | diff | annotate |
| Wed, 18 Sep 2019 12:15:59 +0200 |
tests run in Test_Isac with ML_system_64 = "true", still exception Size
|
file | diff | annotate |
| Mon, 26 Aug 2019 17:40:27 +0200 |
rename Isac.thy --> Isac_Knowledge.thy
|
file | diff | annotate |
| Wed, 24 Jul 2019 09:32:17 +0200 |
lucin: improve signature of "fun locate_input_tactic"
|
file | diff | annotate |
| Thu, 04 Apr 2019 17:52:52 +0200 |
[-Test_Isac] code cleanup & tests from previous changeset
|
file | diff | annotate |
| Wed, 27 Mar 2019 19:14:47 +0100 |
[-Test_Isac] adapt monom_of_term, add_fraction_p_ to AA
|
file | diff | annotate |
| Tue, 13 Feb 2018 16:17:59 +0100 |
Isabelle2015->17: simplification of rationals changed
|
file | diff | annotate |
| Tue, 06 Feb 2018 16:18:43 +0100 |
Isabelle2015->17: transfer changes from src/ to test/
|
file | diff | annotate |
| Wed, 05 Oct 2016 13:09:54 +0200 |
cleaned tests from autoCalculate' (removed ')
|
file | diff | annotate |
| Mon, 21 Dec 2015 14:06:19 +0100 |
Isabelle2014-->15: finished closed Thm.thy for tests
|
file | diff | annotate |
| Mon, 07 Dec 2015 14:10:59 +0100 |
Isabelle2014-->15: closed Thm.thy applied to tests
|
file | diff | annotate |
| Mon, 20 Apr 2015 14:18:40 +0200 |
update test/ to Isabelle2014 (~ updates of src/)
|
file | diff | annotate |
| Thu, 31 Jul 2014 14:15:41 +0200 |
ad (b): lookup for sym_thmID directly from Isabelle using sym_thm
|
file | diff | annotate |
| Thu, 24 Jul 2014 17:22:21 +0200 |
corrected string_of_thmI, wrong since Isabelle2009-->2011
|
file | diff | annotate |
| Thu, 24 Jul 2014 15:44:50 +0200 |
removed the only occurrence of (ill-named) string_of_thm: finished
|
file | diff | annotate |
| Fri, 13 Jun 2014 12:42:15 +0200 |
autoCalculate now parallelized
|
file | diff | annotate |
| Fri, 13 Jun 2014 12:06:38 +0200 |
moved from "Unsynchronized.ref states" to "Synchronized.var states"
|
file | diff | annotate |
| Mon, 16 Sep 2013 12:27:20 +0200 |
review of examples for non-termination of rls norm_Rational
|
file | diff | annotate |
| Mon, 16 Sep 2013 12:20:00 +0200 |
Test_Isac works again, perfectly ..
|
file | diff | annotate |
| Mon, 16 Sep 2013 11:28:43 +0200 |
gcd_poly requires special handling for a monomial argument
|
file | diff | annotate |
| Mon, 02 Sep 2013 16:16:08 +0200 |
Test_Isac works again, almost ..
|
file | diff | annotate |
| Mon, 02 Sep 2013 15:17:34 +0200 |
GCD_Poly_ML: survey on levels integrating gcd_poly in Rational.thy
|
file | diff | annotate |
| Fri, 30 Aug 2013 13:43:30 +0200 |
GCD_Poly_ML: rewrite cancel is NONE if gcd_poly is 1
|
file | diff | annotate |
| Wed, 28 Aug 2013 11:48:37 +0200 |
GCD_Poly_ML: test 2nd level integration of gcd_poly
|
file | diff | annotate |
| Wed, 28 Aug 2013 11:02:03 +0200 |
GCD_Poly_ML: correct & improve assumptions generated from gcd_pol
|
file | diff | annotate |
| Wed, 28 Aug 2013 10:40:53 +0200 |
GCD_Poly_ML: test 1st level integration of gcd_poly
|
file | diff | annotate |
| Mon, 26 Aug 2013 16:32:21 +0200 |
tuned
|
file | diff | annotate |
| Sat, 24 Aug 2013 17:41:40 +0200 |
GCD_Poly_ML: integrated tests, reactivated test/../rational.sml
|
file | diff | annotate |
| Sat, 24 Aug 2013 11:54:39 +0200 |
GCD_Poly_ML: conversions term <--> poly
|
file | diff | annotate |
| Sat, 24 Aug 2013 11:18:43 +0200 |
GCD_Poly_ML: reformat specific part of rewriter
|
file | diff | annotate |
| Wed, 05 Dec 2012 10:21:35 +0100 |
collected non-termination in gcd_poly from Isabelle2002
|
file | diff | annotate |
| Sun, 14 Oct 2012 20:00:27 +0200 |
2011-->2012: ...
|
file | diff | annotate |
| Sun, 29 Jul 2012 16:29:04 +0200 |
prepare for stepToErrorPattern
|
file | diff | annotate |
| Wed, 13 Jun 2012 10:30:33 +0200 |
errpats for cancel
|
file | diff | annotate |
| Sat, 17 Mar 2012 12:52:30 +0100 |
uncomment test/../root,equation,poly.sml (Isabelle 2002 --> 2011)
|
file | diff | annotate |
| Thu, 06 Oct 2011 17:43:00 +0200 |
intermed. Build_Inverse_Z_Transform:
|
file | diff | annotate |
| Fri, 18 Mar 2011 09:26:03 +0100 |
intermed. usecase Diophant
|
file | diff | annotate |
| Thu, 17 Mar 2011 10:46:02 +0100 |
intermed usecase Diophant
|
file | diff | annotate |
| Thu, 17 Mar 2011 10:11:18 +0100 |
intermed. usecase Diophant
|
file | diff | annotate |
| Mon, 14 Mar 2011 16:50:44 +0100 |
intermed.update Isabelle2011: tests finished...
|
file | diff | annotate |
| Thu, 10 Mar 2011 17:05:09 +0100 |
intermed.update Isabelle2011: Not --> HOL.Not
|
file | diff | annotate |
| Thu, 10 Mar 2011 16:04:00 +0100 |
intermed.update Isabelle2011: HOL.True
|
file | diff | annotate |
| Fri, 31 Dec 2010 14:54:02 +0100 |
removed error *** nxt_add: EX itm. not(dat(itm)<=dat(ori))
|
file | diff | annotate |
| Wed, 29 Dec 2010 20:07:52 +0100 |
intermed. in course/T3_MathEngine.thy
|
file | diff | annotate |
| Tue, 05 Oct 2010 16:46:56 +0200 |
repaired 'fun calc_equ' for "op <", completed rewriting in test/../rational.sml
|
file | diff | annotate |
| Tue, 05 Oct 2010 14:41:16 +0200 |
intermed. test/../rational.sml, before "op *" --> "Orderings.ord_class.less"
|
file | diff | annotate |
| Tue, 05 Oct 2010 09:17:48 +0200 |
updated print_exn
|
file | diff | annotate |
| Tue, 05 Oct 2010 08:35:55 +0200 |
intermed. test/../rational.sml
|
file | diff | annotate |
| Tue, 28 Sep 2010 10:10:26 +0200 |
updated "op *" --> Groups.times_class.times in src and test
|
file | diff | annotate |