Walther Neuper <wneuper@ist.tugraz.at> [Fri, 23 Feb 2018 06:50:06 +0100] rev 59378
tuned redundant pattern in fun def.
Walther Neuper <wneuper@ist.tugraz.at> [Thu, 22 Feb 2018 17:55:29 +0100] rev 59377
LTool: cleanup test file
Walther Neuper <wneuper@ist.tugraz.at> [Fri, 16 Feb 2018 14:39:29 +0100] rev 59376
LTool: cleanup source file
Walther Neuper <wneuper@ist.tugraz.at> [Wed, 14 Feb 2018 15:59:00 +0100] rev 59375
prep. opening LTool for test/
Walther Neuper <wneuper@ist.tugraz.at> [Wed, 14 Feb 2018 12:20:35 +0100] rev 59374
separate structure LTools : LANGUAGE_TOOLS
Walther Neuper <wneuper@ist.tugraz.at> [Wed, 14 Feb 2018 10:54:53 +0100] rev 59373
/----- finish update Isabelle2015 --> Isabelle2017
Walther Neuper <wneuper@ist.tugraz.at> [Wed, 14 Feb 2018 10:50:12 +0100] rev 59372
Isabelle2015->17: "biegelinie" is broken
presumed cause: simplification changed cf. 5f9f07d37a1e
ATTENTION: exp 7.70 causes overflow, which has not been noticed in isabisac15;
but overflow-version in isabisac15 works in isac-java --
-- so fix is postponed to update of isac-java.
Walther Neuper <wneuper@ist.tugraz.at> [Wed, 14 Feb 2018 08:05:37 +0100] rev 59371
Isabelle2015->17: simplification changed cf. 5f9f07d37a1e
Walther Neuper <wneuper@ist.tugraz.at> [Wed, 14 Feb 2018 06:06:27 +0100] rev 59370
Isabelle2015->17: completed "normalise" cf. fb6f5ef2c647
Walther Neuper <wneuper@ist.tugraz.at> [Tue, 13 Feb 2018 16:17:59 +0100] rev 59369
Isabelle2015->17: simplification of rationals changed
different
# \<noteq> in assumptions cf. 17bc5920c2fb
# 1 non-termination
# "a / b" --> "-a / -b"
# "0" --> "0 / b"