src/CTT/rew.ML
changeset 19761 5cd82054c2c6
parent 17496 26535df536ae
child 35762 af3ff2ba4c54
     1.1 --- a/src/CTT/rew.ML	Fri Jun 02 16:06:19 2006 +0200
     1.2 +++ b/src/CTT/rew.ML	Fri Jun 02 18:15:38 2006 +0200
     1.3 @@ -1,15 +1,15 @@
     1.4 -(*  Title:      CTT/rew
     1.5 +(*  Title:      CTT/rew.ML
     1.6      ID:         $Id$
     1.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.8      Copyright   1991  University of Cambridge
     1.9  
    1.10 -Simplifier for CTT, using Typedsimp
    1.11 +Simplifier for CTT, using Typedsimp.
    1.12  *)
    1.13  
    1.14  (*Make list of ProdE RS ProdE ... RS ProdE RS EqE
    1.15    for using assumptions as rewrite rules*)
    1.16  fun peEs 0 = []
    1.17 -  | peEs n = EqE :: map (curry (op RS) ProdE) (peEs (n-1));
    1.18 +  | peEs n = thm "EqE" :: map (curry (op RS) (thm "ProdE")) (peEs (n-1));
    1.19  
    1.20  (*Tactic used for proving conditions for the cond_rls*)
    1.21  val prove_cond_tac = eresolve_tac (peEs 5);
    1.22 @@ -17,19 +17,19 @@
    1.23  
    1.24  structure TSimp_data: TSIMP_DATA =
    1.25    struct
    1.26 -  val refl              = refl_elem
    1.27 -  val sym               = sym_elem
    1.28 -  val trans             = trans_elem
    1.29 -  val refl_red          = refl_red
    1.30 -  val trans_red         = trans_red
    1.31 -  val red_if_equal      = red_if_equal
    1.32 -  val default_rls       = comp_rls
    1.33 -  val routine_tac       = routine_tac routine_rls
    1.34 +  val refl              = thm "refl_elem"
    1.35 +  val sym               = thm "sym_elem"
    1.36 +  val trans             = thm "trans_elem"
    1.37 +  val refl_red          = thm "refl_red"
    1.38 +  val trans_red         = thm "trans_red"
    1.39 +  val red_if_equal      = thm "red_if_equal"
    1.40 +  val default_rls       = thms "comp_rls"
    1.41 +  val routine_tac       = routine_tac (thms "routine_rls")
    1.42    end;
    1.43  
    1.44  structure TSimp = TSimpFun (TSimp_data);
    1.45  
    1.46 -val standard_congr_rls = intrL2_rls @ elimL_rls;
    1.47 +val standard_congr_rls = thms "intrL2_rls" @ thms "elimL_rls";
    1.48  
    1.49  (*Make a rewriting tactic from a normalization tactic*)
    1.50  fun make_rew_tac ntac =