author nipkow
Tue, 09 May 1995 22:10:08 +0200
changeset 1114 c8dfb56a7e95
parent 0 a5a9c433f639
permissions -rwxr-xr-x
Prod is now a parent of Lfp. Added thm induct2 to Lfp. Changed the way patterns in abstractions are pretty printed. It has become simpler now but fails if split has more than one argument because then the ast-translation does not match.

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