# HG changeset patch
# User wenzelm
# Date 898366731 -7200
# Node ID dcdb21e5353784989058bcb9fe00ebc747f53326
# Parent  52a78ff5599e423a18fafd72fdd72036d11e79e0
renamed Thm(s) back to thm(s);

diff -r 52a78ff5599e -r dcdb21e53537 NEWS
--- a/NEWS	Sat Jun 20 20:18:22 1998 +0200
+++ b/NEWS	Sat Jun 20 20:18:51 1998 +0200
@@ -38,7 +38,7 @@
 * inductive definitions now handle disjunctive premises correctly (HOL
 and ZF);
 
-* new toplevel commands 'Thm' and 'Thms' for retrieving theorems from
+* new toplevel commands 'thm' and 'thms' for retrieving theorems from
 the current theory context;
 
 * new toplevel commands `Goal' and `Goalw' that improve upon `goal'
diff -r 52a78ff5599e -r dcdb21e53537 src/Pure/Thy/context.ML
--- a/src/Pure/Thy/context.ML	Sat Jun 20 20:18:22 1998 +0200
+++ b/src/Pure/Thy/context.ML	Sat Jun 20 20:18:51 1998 +0200
@@ -9,8 +9,8 @@
 sig
   val context: theory -> unit
   val the_context: unit -> theory
-  val Thm: xstring -> thm
-  val Thms: xstring -> thm list
+  val thm: xstring -> thm
+  val thms: xstring -> thm list
   val Goal: string -> thm list
   val Goalw: thm list -> string -> thm list
 end;
@@ -73,8 +73,8 @@
 
 (* retrieve thms *)
 
-fun Thm name = PureThy.get_thm (the_context ()) name;
-fun Thms name = PureThy.get_thms (the_context ()) name;
+fun thm name = PureThy.get_thm (the_context ()) name;
+fun thms name = PureThy.get_thms (the_context ()) name;
 
 
 (* shortcut goal commands *)