summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

get-rulenames

author | nipkow |

Mon Apr 22 15:42:20 1996 +0200 (1996-04-22) | |

changeset 1669 | e56cdf711729 |

parent 0 | a5a9c433f639 |

permissions | -rwxr-xr-x |

inserted Suc_less_eq explictly in a few proofs.

inserted o_def explictly in a few proofs because the new split_tac causes

fewer eta-expansions which some of the rewrites need.

Indented proof in I.ML

inserted o_def explictly in a few proofs because the new split_tac causes

fewer eta-expansions which some of the rewrites need.

Indented proof in I.ML

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' ','`