Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Object.T;
authorwenzelm
Fri, 05 Jun 1998 14:29:54 +0200
changeset 4999 4c74267cfa0c
parent 4998 28fe46a570d7
child 5000 9271b89c7e2c
Object.T;
src/Pure/thm.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/thm.ML	Fri Jun 05 14:29:33 1998 +0200
+++ b/src/Pure/thm.ML	Fri Jun 05 14:29:54 1998 +0200
@@ -44,7 +44,7 @@
   val keep_derivs       : deriv_kind ref
   datatype rule = 
       MinProof                          
-    | Oracle		  of string * Sign.sg * object
+    | Oracle		  of string * Sign.sg * Object.T
     | Axiom               of string
     | Theorem             of string       
     | Assume              of cterm
@@ -172,7 +172,7 @@
   val rewrite_cterm     : bool * bool * bool -> meta_simpset ->
                           (meta_simpset -> thm -> thm option) -> cterm -> thm
 
-  val invoke_oracle     : theory -> xstring -> Sign.sg * object -> thm
+  val invoke_oracle     : theory -> xstring -> Sign.sg * Object.T -> thm
 end;
 
 structure Thm: THM =
@@ -298,7 +298,7 @@
   executed in ML.*)
 datatype rule = 
     MinProof                            (*for building minimal proof terms*)
-  | Oracle              of string * Sign.sg * object       (*oracles*)
+  | Oracle              of string * Sign.sg * Object.T       (*oracles*)
 (*Axioms/theorems*)
   | Axiom               of string
   | Theorem             of string
isabelle