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"
Walther Neuper <wneuper@ist.tugraz.at> [Tue, 13 Feb 2018 15:25:16 +0100] rev 59368
Isabelle2015->17: fix not checked with PCD_Poly_ML.thy
Walther Neuper <wneuper@ist.tugraz.at> [Tue, 13 Feb 2018 15:14:55 +0100] rev 59367
Isabelle2015->17: "normalize" as identifier causes type clash now, etc
etc fixes:
# new negation "~ " --> "<not>"n noteq cf. 17bc5920c2fb
# session identifiers enforced now cf. 172b53399454
Walther Neuper <wneuper@ist.tugraz.at> [Sat, 10 Feb 2018 16:21:12 +0100] rev 59366
Isabelle2015->17: fix error introduced by 'session identifiers' 172b53399454
Walther Neuper <wneuper@ist.tugraz.at> [Sat, 10 Feb 2018 15:12:59 +0100] rev 59365
Isabelle2015->17: mini fixes in test
Walther Neuper <wneuper@ist.tugraz.at> [Fri, 09 Feb 2018 12:12:25 +0100] rev 59364
Isabelle2015->17: imports of Text_Isac work again
Walther Neuper <wneuper@ist.tugraz.at> [Fri, 09 Feb 2018 12:00:21 +0100] rev 59363
Isabelle2015->17: Minisubpbl works due to previous fixes
Walther Neuper <wneuper@ist.tugraz.at> [Fri, 09 Feb 2018 11:57:24 +0100] rev 59362
Isabelle2015->17: tests work down to Minisubpbl