changeset 38786 | e46e7a9cb622 |
parent 37678 | 0040bafffdef |
child 38795 | 848be46708dc |
--- a/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy Thu Aug 26 13:44:50 2010 +0200 +++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy Thu Aug 26 20:51:17 2010 +0200 @@ -54,7 +54,7 @@ ONE_ONE > HOL4Setup.ONE_ONE ONTO > Fun.surj "=" > "op =" - "==>" > "op -->" + "==>" > HOL.implies "/\\" > "op &" "\\/" > "op |" "!" > All