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.
local_def(_i): no constraint on var;
authorwenzelm
Sun, 30 Jul 2000 12:52:46 +0200
changeset 9466 e9f5768bb656
parent 9465 b285b91cd2b2
child 9467 52fb37876254
local_def(_i): no constraint on var;
src/Pure/Isar/isar_thy.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/isar_thy.ML	Sun Jul 30 12:52:13 2000 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Sun Jul 30 12:52:46 2000 +0200
@@ -103,9 +103,9 @@
     * Comment.text) list -> ProofHistory.T -> ProofHistory.T
   val presume_i: ((string * Proof.context attribute list * (term * (term list * term list)) list)
     * Comment.text) list -> ProofHistory.T -> ProofHistory.T
-  val local_def: (string * Args.src list * ((string * string option) * (string * string list)))
+  val local_def: (string * Args.src list * (string * (string * string list)))
     * Comment.text -> ProofHistory.T -> ProofHistory.T
-  val local_def_i: (string * Args.src list * ((string * typ option) * (term * term list)))
+  val local_def_i: (string * Args.src list * (string * (term * term list)))
     * Comment.text -> ProofHistory.T -> ProofHistory.T
   val show: (string * Args.src list * (string * (string list * string list)))
     * Comment.text -> ProofHistory.T -> ProofHistory.T
isabelle