renamed Thm(s) back to thm(s);
authorwenzelm
Sat Jun 20 20:18:51 1998 +0200 (1998-06-20)
changeset 5059dcdb21e53537
parent 5058 52a78ff5599e
child 5060 7b86df67cc1a
renamed Thm(s) back to thm(s);
NEWS
src/Pure/Thy/context.ML
     1.1 --- a/NEWS	Sat Jun 20 20:18:22 1998 +0200
     1.2 +++ b/NEWS	Sat Jun 20 20:18:51 1998 +0200
     1.3 @@ -38,7 +38,7 @@
     1.4  * inductive definitions now handle disjunctive premises correctly (HOL
     1.5  and ZF);
     1.6  
     1.7 -* new toplevel commands 'Thm' and 'Thms' for retrieving theorems from
     1.8 +* new toplevel commands 'thm' and 'thms' for retrieving theorems from
     1.9  the current theory context;
    1.10  
    1.11  * new toplevel commands `Goal' and `Goalw' that improve upon `goal'
     2.1 --- a/src/Pure/Thy/context.ML	Sat Jun 20 20:18:22 1998 +0200
     2.2 +++ b/src/Pure/Thy/context.ML	Sat Jun 20 20:18:51 1998 +0200
     2.3 @@ -9,8 +9,8 @@
     2.4  sig
     2.5    val context: theory -> unit
     2.6    val the_context: unit -> theory
     2.7 -  val Thm: xstring -> thm
     2.8 -  val Thms: xstring -> thm list
     2.9 +  val thm: xstring -> thm
    2.10 +  val thms: xstring -> thm list
    2.11    val Goal: string -> thm list
    2.12    val Goalw: thm list -> string -> thm list
    2.13  end;
    2.14 @@ -73,8 +73,8 @@
    2.15  
    2.16  (* retrieve thms *)
    2.17  
    2.18 -fun Thm name = PureThy.get_thm (the_context ()) name;
    2.19 -fun Thms name = PureThy.get_thms (the_context ()) name;
    2.20 +fun thm name = PureThy.get_thm (the_context ()) name;
    2.21 +fun thms name = PureThy.get_thms (the_context ()) name;
    2.22  
    2.23  
    2.24  (* shortcut goal commands *)