search

jukoepke / hol-light

Automatically exported from code.google.com/p/hol-light
Other
0 stars 0 forks source link

grammar error in 'new_type' documentation #13

Open GoogleCodeExporter opened 9 years ago

GoogleCodeExporter commented 9 years ago 
Documentation of new_type's FAILURE CONDITIONS contains a grammar error (or a 
grammar mistake): "Fails if HOL is there is already a type operator..."

Original issue reported on code.google.com by piotr.tr...@gmail.com on 23 Jul 2014 at 7:54

GoogleCodeExporter commented 9 years ago 
Thanks, finally fixed in r205.

Original comment by jrh...@gmail.com on 16 Nov 2014 at 8:30