| author | Christian Urban <urbanc@in.tum.de> |
| Mon, 18 Jul 2011 00:21:51 +0100 | |
| changeset 2971 | d629240f0f63 |
| parent 2931 | aaef9dec5e1d |
| permissions | -rw-r--r-- |
|
2856
e36beb11723c
added a stub for function paper; "isabelle make fnpaper"
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1 |
(*<*) |
|
e36beb11723c
added a stub for function paper; "isabelle make fnpaper"
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
2 |
theory Paper |
|
e36beb11723c
added a stub for function paper; "isabelle make fnpaper"
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
3 |
imports "~~/src/HOL/Library/LaTeXsugar" |
|
e36beb11723c
added a stub for function paper; "isabelle make fnpaper"
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
4 |
begin |
|
e36beb11723c
added a stub for function paper; "isabelle make fnpaper"
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
5 |
|
|
e36beb11723c
added a stub for function paper; "isabelle make fnpaper"
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
6 |
declare [[show_question_marks = false]] |
|
e36beb11723c
added a stub for function paper; "isabelle make fnpaper"
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
7 |
|
|
2862
47063163f333
added eqvt_at and invariant for boths sides of the equations
Christian Urban <urbanc@in.tum.de>
parents:
2856
diff
changeset
|
8 |
section {* Introduction *}
|
|
2856
e36beb11723c
added a stub for function paper; "isabelle make fnpaper"
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
9 |
|
|
2931
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
2862
diff
changeset
|
10 |
text {*
|
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
2862
diff
changeset
|
11 |
mention Russo paper which concludes that technology is not |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
2862
diff
changeset
|
12 |
ready beyond core-calculi. |
|
2856
e36beb11723c
added a stub for function paper; "isabelle make fnpaper"
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
13 |
|
|
e36beb11723c
added a stub for function paper; "isabelle make fnpaper"
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
14 |
|
|
e36beb11723c
added a stub for function paper; "isabelle make fnpaper"
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
15 |
|
|
2931
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
2862
diff
changeset
|
16 |
*} |
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
2862
diff
changeset
|
17 |
|
|
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
parents:
2862
diff
changeset
|
18 |
|
|
2856
e36beb11723c
added a stub for function paper; "isabelle make fnpaper"
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
19 |
(*<*) |
|
e36beb11723c
added a stub for function paper; "isabelle make fnpaper"
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
20 |
end |
|
e36beb11723c
added a stub for function paper; "isabelle make fnpaper"
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
21 |
(*>*) |