--- 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 *)