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/Isar/proof.ML
changeset 30240 5b25fee0362c
parent 29581 b3b33e0298eb
child 30279 84097bba7bdc 
--- a/src/Pure/Isar/proof.ML	Wed Mar 04 10:43:39 2009 +0100
+++ b/src/Pure/Isar/proof.ML	Wed Mar 04 10:45:52 2009 +0100
@@ -48,23 +48,18 @@
   val assm: Assumption.export ->
     (Attrib.binding * (string * string list) list) list -> state -> state
   val assm_i: Assumption.export ->
-    ((binding * attribute list) * (term * term list) list) list -> state -> state
+    (Thm.binding * (term * term list) list) list -> state -> state
   val assume: (Attrib.binding * (string * string list) list) list -> state -> state
-  val assume_i: ((binding * attribute list) * (term * term list) list) list ->
-    state -> state
+  val assume_i: (Thm.binding * (term * term list) list) list -> state -> state
   val presume: (Attrib.binding * (string * string list) list) list -> state -> state
-  val presume_i: ((binding * attribute list) * (term * term list) list) list ->
-    state -> state
-  val def: (Attrib.binding * ((binding * mixfix) * (string * string list))) list ->
-    state -> state
-  val def_i: ((binding * attribute list) *
-    ((binding * mixfix) * (term * term list))) list -> state -> state
+  val presume_i: (Thm.binding * (term * term list) list) list -> state -> state
+  val def: (Attrib.binding * ((binding * mixfix) * (string * string list))) list -> state -> state
+  val def_i: (Thm.binding * ((binding * mixfix) * (term * term list))) list -> state -> state
   val chain: state -> state
   val chain_facts: thm list -> state -> state
   val get_thmss: state -> (Facts.ref * Attrib.src list) list -> thm list
   val note_thmss: (Attrib.binding * (Facts.ref * Attrib.src list) list) list -> state -> state
-  val note_thmss_i: ((binding * attribute list) *
-    (thm list * attribute list) list) list -> state -> state
+  val note_thmss_i: (Thm.binding * (thm list * attribute list) list) list -> state -> state
   val from_thmss: ((Facts.ref * Attrib.src list) list) list -> state -> state
   val from_thmss_i: ((thm list * attribute list) list) list -> state -> state
   val with_thmss: ((Facts.ref * Attrib.src list) list) list -> state -> state
@@ -107,11 +102,11 @@
   val have: Method.text option -> (thm list list -> state -> state) ->
     (Attrib.binding * (string * string list) list) list -> bool -> state -> state
   val have_i: Method.text option -> (thm list list -> state -> state) ->
-    ((binding * attribute list) * (term * term list) list) list -> bool -> state -> state
+    (Thm.binding * (term * term list) list) list -> bool -> state -> state
   val show: Method.text option -> (thm list list -> state -> state) ->
     (Attrib.binding * (string * string list) list) list -> bool -> state -> state
   val show_i: Method.text option -> (thm list list -> state -> state) ->
-    ((binding * attribute list) * (term * term list) list) list -> bool -> state -> state
+    (Thm.binding * (term * term list) list) list -> bool -> state -> state
   val schematic_goal: state -> bool
   val is_relevant: state -> bool
   val local_future_proof: (state -> ('a * state) Future.future) ->
isabelle