Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/drule.ML
changeset 32958 3228627994d9
parent 31977 e03059ae2d82
child 33095 bbd52d2f8696 
--- a/src/Pure/drule.ML	Sat Oct 17 00:52:37 2009 +0200
+++ b/src/Pure/drule.ML	Sat Oct 17 00:53:18 2009 +0200
@@ -29,8 +29,6 @@
   val zero_var_indexes_list: thm list -> thm list
   val zero_var_indexes: thm -> thm
   val implies_intr_hyps: thm -> thm
-  val standard: thm -> thm
-  val standard': thm -> thm
   val rotate_prems: int -> thm -> thm
   val rearrange_prems: int list -> thm -> thm
   val RSN: thm * (int * thm) -> thm
@@ -77,6 +75,8 @@
   val beta_conv: cterm -> cterm -> cterm
   val types_sorts: thm -> (indexname-> typ option) * (indexname-> sort option)
   val flexflex_unique: thm -> thm
+  val standard: thm -> thm
+  val standard': thm -> thm
   val get_def: theory -> xstring -> thm
   val store_thm: bstring -> thm -> thm
   val store_standard_thm: bstring -> thm -> thm
isabelle