command 'interpret' no longer exposes resulting theorems as literal facts;
Subject: Announcing Isabelle2017To: isabelle-users@cl.cam.ac.ukIsabelle2017 is now available.This version introduces many changes over Isabelle2016-1: see the NEWSfile for further details. Some notable points:* Experimental support for Visual Studio Code as alternative PIDE front-end.* Improved Isabelle/jEdit Prover IDE: management of session sourcesindependently of editor buffers, removal of unused theories, explicitindication of theory status, more careful auto-indentation.* Session-qualified theory imports.* Code generator improvements: support for statically embedded computations.* Numerous HOL library improvements.* More material in HOL-Algebra, HOL-Computational_Algebra and HOL-Analysis(ported from HOL-Light).* Improved Nunchaku model finder, now in main HOL.* SQL database support in Isabelle/Scala.You may get Isabelle2017 from the following mirror sites: Cambridge (UK) http://www.cl.cam.ac.uk/research/hvg/Isabelle Munich (Germany) http://isabelle.in.tum.de Sydney (Australia) http://mirror.cse.unsw.edu.au/pub/isabelle Potsdam, NY (USA) http://mirror.clarkson.edu/isabelle