doc-src/TutorialI/ROOT.ML
author wenzelm
Thu, 26 Jul 2012 17:16:02 +0200
changeset 48519 5deda0549f97
child 48521 0e4bb86c74fd
permissions -rw-r--r--
simplified Tutorial sessions; moved original version of generated .tex sources;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
48519
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
     1
Thy_Output.indent_default := 5;
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
     2
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
     3
use_thy "ToyList/ToyList";
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
     4
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
     5
use_thy "Ifexpr/Ifexpr";
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
     6
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
     7
use_thy "CodeGen/CodeGen";
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
     8
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
     9
use_thy "Trie/Trie";
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
    10
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
    11
use_thy "Datatype/ABexpr";
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
    12
use_thy "Datatype/unfoldnested";
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
    13
use_thy "Datatype/Nested";
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
    14
use_thy "Datatype/Fundata";
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
    15
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
    16
use_thy "Fun/fun0";
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
    17
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
    18
use_thy "Advanced/simp2";
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
    19
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
    20
use_thy "CTL/PDL";
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
    21
use_thy "CTL/CTL";
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
    22
use_thy "CTL/CTLind";
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
    23
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
    24
use_thy "Inductive/Even";
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
    25
use_thy "Inductive/Mutual";
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
    26
use_thy "Inductive/Star";
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
    27
use_thy "Inductive/AB";
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
    28
use_thy "Inductive/Advanced";
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
    29
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
    30
no_document use_thy "Types/Setup";
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
    31
use_thy "Types/Numbers";
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
    32
use_thy "Types/Pairs";
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
    33
use_thy "Types/Records";
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
    34
use_thy "Types/Typedefs";
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
    35
use_thy "Types/Overloading";
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
    36
use_thy "Types/Axioms";
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
    37
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
    38
use_thy "Misc/Tree";
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
    39
use_thy "Misc/Tree2";
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
    40
use_thy "Misc/Plus";
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
    41
use_thy "Misc/case_exprs";
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
    42
use_thy "Misc/fakenat";
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
    43
use_thy "Misc/natsum";
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
    44
use_thy "Misc/pairs";
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
    45
use_thy "Misc/Option2";
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
    46
use_thy "Misc/types";
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
    47
use_thy "Misc/prime_def";
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
    48
use_thy "Misc/simp";
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
    49
use_thy "Misc/Itrev";
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
    50
use_thy "Misc/AdvancedInd";
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
    51
use_thy "Misc/appendix";
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
    52
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
    53
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
    54
Thy_Output.indent_default := 0;
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
    55
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
    56
use_thy "Rules/Basic";
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
    57
use_thy "Rules/Blast";
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
    58
use_thy "Rules/Force";
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
    59
use_thy "Rules/Forward";
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
    60
use_thy "Rules/Tacticals";
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
    61
use_thy "Rules/find2";
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
    62
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
    63
use_thy "Sets/Examples";
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
    64
use_thy "Sets/Functions";
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
    65
use_thy "Sets/Relations";
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
    66
use_thy "Sets/Recur";
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
    67
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
    68
use_thy "Protocol/NS_Public";
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
    69
5deda0549f97 simplified Tutorial sessions;
wenzelm
parents:
diff changeset
    70
use_thy "Documents/Documents";