# HG changeset patch
# User wenzelm
# Date 857393440 -3600
# Node ID c3b86dcd340ad5df62718ed6afd25b6acab992ad
# Parent  3a1fe1c21b777a313e20ea82663c39eb2a82f8a2
added comment: print translations do not mark tokens;

diff -r 3a1fe1c21b77 -r c3b86dcd340a src/HOL/Hoare/Hoare.thy
--- a/src/HOL/Hoare/Hoare.thy	Sat Mar 01 20:09:50 1997 +0100
+++ b/src/HOL/Hoare/Hoare.thy	Mon Mar 03 13:50:40 1997 +0100
@@ -151,6 +151,8 @@
 
 (*** print translations: semantics -> syntax ***)
 
+(* Note: does not mark tokens *)
+
 (* term_tr':term (name:string,trm:term) ersetzt in trm alle Vorkommen von name $ pvar durch
    entsprechende freie Variablen, welche die pvarID zu pvar darstellen. Beispiel:
         bei name="s" und dem Term "s(0)=s(Suc(0)) & s(0)=X" wird der Term "a=b & a=X" geliefert *)