A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
the tactic has also changed and allows the abstaction over fuction occurences whose type is nat or int.
#! /bin/sh
#
#sedindex - shell script to create indexes, preprocessing LaTeX's .idx file
#
# puts strings prefixed by * into \tt font
# terminator characters for strings are |!@{}
#
# a space terminates the \tt part to allow \index{*notE theorem}, etc.
#
# note that makeindex uses a dboule quote (") to delimit special characters.
#
# change *"X"Y"Z"W to "X"Y"Z"W@{\tt "X"Y"Z"W}
# change *"X"Y"Z to "X"Y"Z@{\tt "X"Y"Z}
# change *"X"Y to "X"Y@{\tt "X"Y}
# change *"X to "X@{\tt "X}
# change *IDENT to IDENT@{\tt IDENT}
# where IDENT is any string not containing | ! or @
# FOUR backslashes: to escape the shell AND sed
sed -e "s~\*\(\".\".\".\".\)~\1@\\\\isa {\1}~g
s~\*\(\".\".\".\)~\1@\\\\isa {\1}~g
s~\*\(\".\".\)~\1@\\\\isa {\1}~g
s~\*\(\".\)~\1@\\\\isa {\1}~g
s~\*\([^ |!@{}][^ |!@{}]*\)~\1@\\\\isa {\1}~g" $1.idx | makeindex -c -q -o $1.ind