| author | zhangx | 
| Sun, 07 Feb 2016 21:21:53 +0800 | |
| changeset 112 | b3795b1f030b | 
| parent 64 | b4bcd1edbb6d | 
| child 195 | 6b26b1fd4da5 | 
| permissions | -rw-r--r-- | 
| 
18
 
598409a21f4c
added nasa talk
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
1  | 
session "PIP" = HOL +  | 
| 
59
 
0a069a667301
removed some fixes about which Isabelle complains
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
45 
diff
changeset
 | 
2  | 
theories [document = false, quick_and_dirty]  | 
| 
64
 
b4bcd1edbb6d
renamed files
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
59 
diff
changeset
 | 
3  | 
"Implementation"  | 
| 
 
b4bcd1edbb6d
renamed files
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
59 
diff
changeset
 | 
4  | 
"Correctness"  | 
| 
45
 
fc83f79009bd
updated for Isabelle 2015
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
43 
diff
changeset
 | 
5  | 
"Test"  | 
| 
18
 
598409a21f4c
added nasa talk
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
6  | 
|
| 
 
598409a21f4c
added nasa talk
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
7  | 
session "Slides2" in "Slides" = PIP +  | 
| 
20
 
b56616fd88dd
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
18 
diff
changeset
 | 
8  | 
options [document_variants="slides2"]  | 
| 
18
 
598409a21f4c
added nasa talk
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
9  | 
theories [document = false]  | 
| 
 
598409a21f4c
added nasa talk
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
10  | 
"~~/src/HOL/Library/LaTeXsugar"  | 
| 
 
598409a21f4c
added nasa talk
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
11  | 
theories[document = true]  | 
| 
 
598409a21f4c
added nasa talk
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
12  | 
"Slides2"  | 
| 
 
598409a21f4c
added nasa talk
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
13  | 
files  | 
| 
 
598409a21f4c
added nasa talk
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
14  | 
"document/build"  | 
| 
 
598409a21f4c
added nasa talk
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
15  | 
|
| 
 
598409a21f4c
added nasa talk
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
16  | 
session "Slides3" in "Slides" = PIP +  | 
| 
 
598409a21f4c
added nasa talk
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
17  | 
options [document = pdf, browser_info = false, document_output = "..", document_variants="slides3"]  | 
| 
 
598409a21f4c
added nasa talk
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
18  | 
theories [document = false]  | 
| 
 
598409a21f4c
added nasa talk
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
19  | 
"~~/src/HOL/Library/LaTeXsugar"  | 
| 
 
598409a21f4c
added nasa talk
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
20  | 
theories[document = true, show_question_marks = false]  | 
| 
 
598409a21f4c
added nasa talk
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
21  | 
"Slides3"  | 
| 
 
598409a21f4c
added nasa talk
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
22  | 
files  | 
| 
20
 
b56616fd88dd
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
18 
diff
changeset
 | 
23  | 
"document/build"  | 
| 
 
b56616fd88dd
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
18 
diff
changeset
 | 
24  | 
|
| 
 
b56616fd88dd
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
18 
diff
changeset
 | 
25  | 
session "Slides4" in "Slides" = PIP +  | 
| 
 
b56616fd88dd
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
18 
diff
changeset
 | 
26  | 
options [document = pdf, browser_info = false, document_output = "..",  | 
| 
 
b56616fd88dd
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
18 
diff
changeset
 | 
27  | 
document_variants="slides4"]  | 
| 
 
b56616fd88dd
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
18 
diff
changeset
 | 
28  | 
theories [document = false]  | 
| 
 
b56616fd88dd
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
18 
diff
changeset
 | 
29  | 
"~~/src/HOL/Library/LaTeXsugar"  | 
| 
 
b56616fd88dd
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
18 
diff
changeset
 | 
30  | 
theories[document = true, show_question_marks = false]  | 
| 
 
b56616fd88dd
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
18 
diff
changeset
 | 
31  | 
"Slides4"  | 
| 
 
b56616fd88dd
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
18 
diff
changeset
 | 
32  | 
files  | 
| 
 
b56616fd88dd
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
18 
diff
changeset
 | 
33  | 
"document/build"  | 
| 
 
b56616fd88dd
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
18 
diff
changeset
 | 
34  | 
|
| 
 
b56616fd88dd
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
18 
diff
changeset
 | 
35  | 
|
| 
 
b56616fd88dd
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
18 
diff
changeset
 | 
36  | 
session Journal in "Journal" = PIP +  | 
| 
 
b56616fd88dd
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
18 
diff
changeset
 | 
37  | 
options [document = pdf, document_output = "..", document_variants="journal"]  | 
| 
 
b56616fd88dd
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
18 
diff
changeset
 | 
38  | 
theories  | 
| 
 
b56616fd88dd
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
18 
diff
changeset
 | 
39  | 
"~~/src/HOL/Library/LaTeXsugar"  | 
| 
 
b56616fd88dd
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
18 
diff
changeset
 | 
40  | 
"Paper"  | 
| 
34
 
313acffe63b6
updated ROOT file
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
20 
diff
changeset
 | 
41  | 
document_files  | 
| 
 
313acffe63b6
updated ROOT file
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
20 
diff
changeset
 | 
42  | 
"root.bib"  | 
| 
 
313acffe63b6
updated ROOT file
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
20 
diff
changeset
 | 
43  | 
"root.tex"  | 
| 
 
313acffe63b6
updated ROOT file
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
20 
diff
changeset
 | 
44  |