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.
tuned;
authorwenzelm
Tue, 03 Apr 2012 11:21:17 +0200
changeset 47287 8f06d8ac4609
parent 47286 392c4cd97e5c
child 47288 b79bf8288b29
tuned;
src/Pure/Isar/expression.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/expression.ML	Tue Apr 03 10:59:20 2012 +0200
+++ b/src/Pure/Isar/expression.ML	Tue Apr 03 11:21:17 2012 +0200
@@ -43,12 +43,9 @@
     (Attrib.binding * term) list -> theory -> Proof.state
   val sublocale_cmd: (local_theory -> local_theory) -> xstring * Position.T -> expression ->
     (Attrib.binding * string) list -> theory -> Proof.state
-  val interpretation: expression_i -> (Attrib.binding * term) list ->
-    theory -> Proof.state
-  val interpretation_cmd: expression -> (Attrib.binding * string) list ->
-    theory -> Proof.state
-  val interpret: expression_i -> (Attrib.binding * term) list ->
-    bool -> Proof.state -> Proof.state
+  val interpretation: expression_i -> (Attrib.binding * term) list -> theory -> Proof.state
+  val interpretation_cmd: expression -> (Attrib.binding * string) list -> theory -> Proof.state
+  val interpret: expression_i -> (Attrib.binding * term) list -> bool -> Proof.state -> Proof.state
   val interpret_cmd: expression -> (Attrib.binding * string) list ->
     bool -> Proof.state -> Proof.state
isabelle