renamed Thm(s) back to thm(s);
authorwenzelm
Sat, 20 Jun 1998 20:18:51 +0200
changeset 5059 dcdb21e53537
parent 5058 52a78ff5599e
child 5060 7b86df67cc1a
renamed Thm(s) back to thm(s);
NEWS
src/Pure/Thy/context.ML
--- 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'
--- 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 *)