get-rulenames
author paulson
Fri Feb 16 17:24:51 1996 +0100 (1996-02-16)
changeset 1511 09354d37a5ab
parent 0 a5a9c433f639
permissions -rwxr-xr-x
Elimination of fully-functorial style.
Type tactic changed to a type abbrevation (from a datatype).
Constructor tactic and function apply deleted.
     1 #!/bin/sh
     2 #   Title: 	get-rulenames  (see also make-rulenames)
     3 #   Author: 	Larry Paulson, Cambridge University Computer Laboratory
     4 #   Copyright   1990  University of Cambridge
     5 #
     6 #shell script to generate "val" declarations for a theory's axioms 
     7 #  also generates a comma-separated list of axiom names
     8 #
     9 #  usage:  make-rulenames  <file>
    10 #
    11 #Rule lines begin with a line containing the word "extend_theory"
    12 #       and end   with a line containing the word "get_axiom"
    13 #Each rule name xyz must appear on a line that begins
    14 #        <spaces> ("xyz"
    15 #Output lines have the form
    16 #        val Eq_comp = ax"Eq_comp";
    17 #
    18 sed -n -e '/ext[end]*_theory/,/get_axiom/ s/^[ []*("\([^"]*\)".*$/val \1	= ax"\1";/p' $1
    19 echo
    20 echo `sed -n -e '/ext[end]*_theory/,/get_axiom/ s/^[ []*("\([^"]*\)".*$/\1/p' $1 | tr '\012' ','`