get-rulenames

"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.

#!/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' ','`