author | nipkow |

Wed Apr 04 09:59:49 2012 +0200 (2012-04-04) | |

changeset 47494 | 8c8f27864ed1 |

parent 47326 | b4490e1a0732 |

child 47495 | 573ca05db948 |

refined new tutorial announcement

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