Much tidying including "qed" instead of result(), and even qed_spec_mp,
and Safe_tac instead of step_tac
(* Title: Redex.ML
ID: $Id$
Author: Ole Rasmussen
Copyright 1995 University of Cambridge
Logic Image: ZF
*)
open Redex;
(* ------------------------------------------------------------------------- *)
(* redex_rec conversions *)
(* ------------------------------------------------------------------------- *)
goal Redex.thy "redex_rec(Var(n),b,c,d) = b(n)";
by (rtac (redex_rec_def RS def_Vrec RS trans) 1);
by (simp_tac (rank_ss addsimps redexes.con_defs) 1);
qed "redex_rec_Var";
goal Redex.thy "redex_rec(Fun(t),b,c,d) = c(t,redex_rec(t,b,c,d))";
by (rtac (redex_rec_def RS def_Vrec RS trans) 1);
by (simp_tac (rank_ss addsimps redexes.con_defs) 1);
qed "redex_rec_Fun";
goal Redex.thy "redex_rec(App(m,f,a),b,c,d) = \
\ d(m,f,a,redex_rec(f,b,c,d),redex_rec(a,b,c,d))";
by (rtac (redex_rec_def RS def_Vrec RS trans) 1);
by (simp_tac (rank_ss addsimps redexes.con_defs) 1);
qed "redex_rec_App";
Addsimps ([redex_rec_App,redex_rec_Fun,redex_rec_Var]@redexes.intrs);