--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/get-rulenames	Thu Sep 16 12:20:38 1993 +0200
@@ -0,0 +1,20 @@
+#!/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' ','`