refined new tutorial announcement
authornipkow
Wed Apr 04 09:59:49 2012 +0200 (2012-04-04)
changeset 474948c8f27864ed1
parent 47326 b4490e1a0732
child 47495 573ca05db948
refined new tutorial announcement
NEWS
     1.1 --- a/NEWS	Tue Apr 03 23:49:24 2012 +0200
     1.2 +++ b/NEWS	Wed Apr 04 09:59:49 2012 +0200
     1.3 @@ -95,7 +95,11 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 -* New tutorial Programming and Proving in Isabelle/HOL
     1.8 +* New tutorial "Programming and Proving in Isabelle/HOL".
     1.9 +It completely supercedes "A Tutorial Introduction to Structured Isar Proofs",
    1.10 +which has been removed. It supercedes "Isabelle/HOL, A Proof Assistant
    1.11 +for Higher-Order Logic" as the recommended beginners tutorial
    1.12 +but does not cover all of the material of that old tutorial.
    1.13  
    1.14  * The representation of numerals has changed. We now have a datatype
    1.15  "num" representing strictly positive binary numerals, along with