Main changes are:
- Lemmas for blift and plift are deleted
- added split_tac for If (via If2, as If does not begin with a constant)
- added new lemmata relating TT, FF and booleans:
Def_bool1, Def_bool2, Def_bool3,Def_bool4
They are added to !simpset, but should not cause difficulties
- added lemma andalso_or relating | on booleans and andalso on truth values
- deleted If_and_if and andalso from !simpset: Pay attention, may kill your proofs!
- added adm lemmas for (f x)~=TT and (f x)~=FF.
#!/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' ','`