#!/bin/sh

 #   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

 echo `sed -n -e '/ext[end]*_theory/,/get_axiom/ s/^[ []*("\([^"]*\)".*$/\1/p' $1 | tr '\012' ','`