src/HOL/ex/reflection.ML
changeset 21669 c68717c16013
parent 21621 f9fd69d96c4e
child 21757 093ca3efb132
     1.1 --- a/src/HOL/ex/reflection.ML	Tue Dec 05 22:14:53 2006 +0100
     1.2 +++ b/src/HOL/ex/reflection.ML	Wed Dec 06 01:12:36 2006 +0100
     1.3 @@ -14,6 +14,9 @@
     1.4  = struct
     1.5  
     1.6  val ext2 = thm "ext2";
     1.7 +val nth_Cons_0 = thm "nth_Cons_0";
     1.8 +val nth_Cons_Suc = thm "nth_Cons_Suc";
     1.9 +
    1.10    (* Make a congruence rule out of a defining equation for the interpretation *)
    1.11    (* th is one defining equation of f, i.e.
    1.12       th is "f (Cp ?t1 ... ?tn) = P(f ?t1, .., f ?tn)" *)