| author | huffman |
| Thu, 26 Feb 2009 08:48:33 -0800 | |
| changeset 30130 | e23770bc97c8 |
| parent 29730 | 924c1fd5f303 |
| child 30167 | faf7b2ba1fef |
| permissions | -rw-r--r-- |
| 29720 | 1 |
set quick_and_dirty; |
| 26844 | 2 |
set ThyOutput.source; |
| 26741 | 3 |
use "../../antiquote_setup.ML"; |
| 26844 | 4 |
|
| 27035 | 5 |
use_thy "Introduction"; |
|
29716
b6266c4c68fe
basic setup for chapter "The Isabelle/Isar Framework";
wenzelm
parents:
28838
diff
changeset
|
6 |
use_thy "Framework"; |
|
29730
924c1fd5f303
added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents:
29720
diff
changeset
|
7 |
use_thy "First_Order_Logic"; |
| 27037 | 8 |
use_thy "Outer_Syntax"; |
| 28751 | 9 |
use_thy "Document_Preparation"; |
|
26869
3bc332135aa7
added chapters for "Specifications" and "Proofs";
wenzelm
parents:
26846
diff
changeset
|
10 |
use_thy "Spec"; |
|
3bc332135aa7
added chapters for "Specifications" and "Proofs";
wenzelm
parents:
26846
diff
changeset
|
11 |
use_thy "Proof"; |
|
28762
f5d79aeffd81
separate chapter "Inner syntax --- the term language";
wenzelm
parents:
28751
diff
changeset
|
12 |
use_thy "Inner_Syntax"; |
| 27048 | 13 |
use_thy "Misc"; |
| 26782 | 14 |
use_thy "Generic"; |
| 26840 | 15 |
use_thy "HOL_Specific"; |
|
26779
35809287ab23
converted refcard.tex to Thy/Quick_Reference.thy;
wenzelm
parents:
26767
diff
changeset
|
16 |
use_thy "Quick_Reference"; |
|
28838
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
28762
diff
changeset
|
17 |
use_thy "Symbols"; |
|
26846
2e6726015771
removed obsolete conversion guide -- converted only section on tactics;
wenzelm
parents:
26844
diff
changeset
|
18 |
use_thy "ML_Tactic"; |