Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
doc-src/TutorialI/isa-index
author chaieb
Wed, 19 May 2004 11:23:59 +0200
changeset 14758 af3b71a46a1c
parent 11404 280436a346ca
permissions -rwxr-xr-x
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.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
11400
ddcfdc38090d isa-index replaces ../sedindex: knows about \\isa
paulson
parents:
diff changeset 
     1
 
#! /bin/sh
ddcfdc38090d isa-index replaces ../sedindex: knows about \\isa
paulson
parents:
diff changeset 
     2
 
#
ddcfdc38090d isa-index replaces ../sedindex: knows about \\isa
paulson
parents:
diff changeset 
     3
 
#sedindex - shell script to create indexes, preprocessing LaTeX's .idx file
ddcfdc38090d isa-index replaces ../sedindex: knows about \\isa
paulson
parents:
diff changeset 
     4
 
#
ddcfdc38090d isa-index replaces ../sedindex: knows about \\isa
paulson
parents:
diff changeset 
     5
 
#  puts strings prefixed by * into \tt font
ddcfdc38090d isa-index replaces ../sedindex: knows about \\isa
paulson
parents:
diff changeset 
     6
 
#    terminator characters for strings are |!@{}
ddcfdc38090d isa-index replaces ../sedindex: knows about \\isa
paulson
parents:
diff changeset 
     7
 
#
ddcfdc38090d isa-index replaces ../sedindex: knows about \\isa
paulson
parents:
diff changeset 
     8
 
# a space terminates the \tt part to allow \index{*notE theorem}, etc.
ddcfdc38090d isa-index replaces ../sedindex: knows about \\isa
paulson
parents:
diff changeset 
     9
 
#
ddcfdc38090d isa-index replaces ../sedindex: knows about \\isa
paulson
parents:
diff changeset 
    10
 
# note that makeindex uses a dboule quote (") to delimit special characters.
ddcfdc38090d isa-index replaces ../sedindex: knows about \\isa
paulson
parents:
diff changeset 
    11
 
#
ddcfdc38090d isa-index replaces ../sedindex: knows about \\isa
paulson
parents:
diff changeset 
    12
 
# change *"X"Y"Z"W  to  "X"Y"Z"W@{\tt "X"Y"Z"W}
ddcfdc38090d isa-index replaces ../sedindex: knows about \\isa
paulson
parents:
diff changeset 
    13
 
# change *"X"Y"Z    to  "X"Y"Z@{\tt "X"Y"Z}
ddcfdc38090d isa-index replaces ../sedindex: knows about \\isa
paulson
parents:
diff changeset 
    14
 
# change *"X"Y      to  "X"Y@{\tt "X"Y}
ddcfdc38090d isa-index replaces ../sedindex: knows about \\isa
paulson
parents:
diff changeset 
    15
 
# change *"X        to  "X@{\tt "X}
ddcfdc38090d isa-index replaces ../sedindex: knows about \\isa
paulson
parents:
diff changeset 
    16
 
# change *IDENT  to  IDENT@{\tt IDENT}
ddcfdc38090d isa-index replaces ../sedindex: knows about \\isa
paulson
parents:
diff changeset 
    17
 
#    where IDENT is any string not containing | ! or @
ddcfdc38090d isa-index replaces ../sedindex: knows about \\isa
paulson
parents:
diff changeset 
    18
 
# FOUR backslashes: to escape the shell AND sed
11404
280436a346ca careful changes to make its output identical to that of indexing macros
paulson
parents: 11400
diff changeset 
    19
 
sed -e "s~\*\(\".\".\".\".\)~\1@\\\\isa {\1}~g
280436a346ca careful changes to make its output identical to that of indexing macros
paulson
parents: 11400
diff changeset 
    20
 
s~\*\(\".\".\".\)~\1@\\\\isa {\1}~g
280436a346ca careful changes to make its output identical to that of indexing macros
paulson
parents: 11400
diff changeset 
    21
 
s~\*\(\".\".\)~\1@\\\\isa {\1}~g
280436a346ca careful changes to make its output identical to that of indexing macros
paulson
parents: 11400
diff changeset 
    22
 
s~\*\(\".\)~\1@\\\\isa {\1}~g
280436a346ca careful changes to make its output identical to that of indexing macros
paulson
parents: 11400
diff changeset 
    23
 
s~\*\([^ |!@{}][^ |!@{}]*\)~\1@\\\\isa {\1}~g" $1.idx | makeindex -c -q -o $1.ind
isabelle