changeset 38795 | 848be46708dc |
parent 37678 | 0040bafffdef |
child 40607 | 30d512bf47a7 |
--- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Fri Aug 27 10:55:20 2010 +0200 +++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Fri Aug 27 10:56:46 2010 +0200 @@ -17,8 +17,8 @@ T > True F > False "!" > All - "/\\" > "op &" - "\\/" > "op |" + "/\\" > HOL.conj + "\\/" > HOL.disj "?" > Ex "?!" > Ex1 "~" > Not