#!/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' $1echoecho `sed -n -e '/ext[end]*_theory/,/get_axiom/ s/^[ []*("\([^"]*\)".*$/\1/p' $1 | tr '\012' ','`