# HG changeset patch # User Christian Urban # Date 1275399943 -7200 # Node ID 530b0adbcf77db8561edf106f89295eec7076aa7 # Parent bdbf040dce897a47083214c7905e0b4235381cf5 tuned diff -r bdbf040dce89 -r 530b0adbcf77 Paper/Paper.thy --- a/Paper/Paper.thy Sat May 29 00:16:39 2010 +0200 +++ b/Paper/Paper.thy Tue Jun 01 15:45:43 2010 +0200 @@ -937,8 +937,8 @@ \noindent Similarly for the other binding modes. Interestingly, in case of \isacommand{bind\_set} - and \isacommand{bind\_res} the binding clauses will make a difference to the semantics - of the specification (the corresponding alpha-equivalence will differ). We will + and \isacommand{bind\_res} the binding clauses above will make a difference to the semantics + of the specifications (the corresponding alpha-equivalence will differ). We will show this later with an example. There are some restrictions we need to impose on binding clasues: First, a @@ -1058,7 +1058,6 @@ "bn(as)"} in the term @{text t}, but with @{text "Let_rec"} we also want to bind the atoms inside the assignment. This difference has consequences for the free-variable function and alpha-equivalence relation, which we are going to define below. - For this definition, we have to impose some restrictions on deep binders. First, we cannot have more than one binding function for one binder. So we exclude: