src/HOLCF/FOCUS/Buffer.ML
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2003-08-28 skalberg 2003-08-28 Extended the notion of letter and digit, such that now one may use greek, gothic, euler, or calligraphic letters as normal letters.
2002-08-05 berghofe 2002-08-05 Replaced nat_ind_tac by induct_tac.
2001-10-03 wenzelm 2001-10-03 tuned parentheses in relational expressions;
2001-05-31 wenzelm 2001-05-31 tuned
2001-05-31 oheimb 2001-05-31 added FOCUS including the One-Element Buffer by Manfred Broy