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.
fix_i, local_def_i: typ option;
authorwenzelm
Thu, 30 Sep 1999 21:22:26 +0200
changeset 7666 226ea33c7cd6
parent 7665 1ab0c74cd748
child 7667 22dc8b2455b8
fix_i, local_def_i: typ option;
src/Pure/Isar/isar_thy.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/isar_thy.ML	Thu Sep 30 21:21:52 1999 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Thu Sep 30 21:22:26 1999 +0200
@@ -72,7 +72,7 @@
   val chain: Comment.text -> ProofHistory.T -> ProofHistory.T
   val export_chain: Comment.text -> ProofHistory.T -> ProofHistory.T
   val fix: ((string list * string option) * Comment.text) list -> ProofHistory.T -> ProofHistory.T
-  val fix_i: ((string list * typ) * Comment.text) list -> ProofHistory.T -> ProofHistory.T
+  val fix_i: ((string list * typ option) * Comment.text) list -> ProofHistory.T -> ProofHistory.T
   val match_bind: ((string list * string) * Comment.text) list -> ProofHistory.T -> ProofHistory.T
   val match_bind_i: ((term list * term) * Comment.text) list -> ProofHistory.T -> ProofHistory.T
   val theorem: (bstring * Args.src list * (string * (string list * string list)))
@@ -93,7 +93,7 @@
     * Comment.text) list -> ProofHistory.T -> ProofHistory.T
   val local_def: (string * Args.src list * ((string * string option) * (string * string list)))
     * Comment.text -> ProofHistory.T -> ProofHistory.T
-  val local_def_i: (string * Args.src list * ((string * typ) * (term * term list)))
+  val local_def_i: (string * Args.src list * ((string * typ option) * (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