A small mod.
2 # Title: get-rulenames (see also make-rulenames)
3 # Author: Larry Paulson, Cambridge University Computer Laboratory
4 # Copyright 1990 University of Cambridge
6 #shell script to generate "val" declarations for a theory's axioms
7 # also generates a comma-separated list of axiom names
9 # usage: make-rulenames <file>
11 #Rule lines begin with a line containing the word "extend_theory"
12 # and end with a line containing the word "get_axiom"
13 #Each rule name xyz must appear on a line that begins
15 #Output lines have the form
16 # val Eq_comp = ax"Eq_comp";
18 sed -n -e '/ext[end]*_theory/,/get_axiom/ s/^[ []*("\([^"]*\)".*$/val \1 = ax"\1";/p' $1
20 echo `sed -n -e '/ext[end]*_theory/,/get_axiom/ s/^[ []*("\([^"]*\)".*$/\1/p' $1 | tr '\012' ','`