# HG changeset patch
# User wenzelm
# Date 939382139 -7200
# Node ID 0e9ad8ad41d76d81cd8a1d68bec9a77b4bf27798
# Parent  66d3b64dbf49448279804845feb1f42bdaddda70
*** empty log message ***

diff -r 66d3b64dbf49 -r 0e9ad8ad41d7 src/HOL/Real/HahnBanach/document/notation.tex