--- a/src/CTT/rew.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/CTT/rew.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: CTT/rew
+(* Title: CTT/rew
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
Simplifier for CTT, using Typedsimp
@@ -17,14 +17,14 @@
structure TSimp_data: TSIMP_DATA =
struct
- val refl = refl_elem
- val sym = sym_elem
- val trans = trans_elem
- val refl_red = refl_red
- val trans_red = trans_red
- val red_if_equal = red_if_equal
- val default_rls = comp_rls
- val routine_tac = routine_tac routine_rls
+ val refl = refl_elem
+ val sym = sym_elem
+ val trans = trans_elem
+ val refl_red = refl_red
+ val trans_red = trans_red
+ val red_if_equal = red_if_equal
+ val default_rls = comp_rls
+ val routine_tac = routine_tac routine_rls
end;
structure TSimp = TSimpFun (TSimp_data);