src/HOL/ex/reflection.ML

--- a/src/HOL/ex/reflection.ML	Tue Dec 05 22:14:53 2006 +0100
+++ b/src/HOL/ex/reflection.ML	Wed Dec 06 01:12:36 2006 +0100
@@ -14,6 +14,9 @@
 = struct
 
 val ext2 = thm "ext2";
+val nth_Cons_0 = thm "nth_Cons_0";
+val nth_Cons_Suc = thm "nth_Cons_Suc";
+
   (* Make a congruence rule out of a defining equation for the interpretation *)
   (* th is one defining equation of f, i.e.
      th is "f (Cp ?t1 ... ?tn) = P(f ?t1, .., f ?tn)" *)