doc-src/Codegen/Thy/ROOT.ML
author wenzelm
Wed, 18 Aug 2010 23:44:50 +0200
changeset 38479 e628da370072
parent 38405 7935b334893e
child 38510 ec0408c7328b
permissions -rw-r--r--
more efficient Markup_Tree, based on branches sorted by quasi-order; renamed markup_node.scala to markup_tree.scala and classes/objects accordingly; Position.Range: produce actual Text.Range; Symbol.Index.decode: convert 1-based Isabelle offsets here; added static Command.range; simplified Command.markup; Document_Model.token_marker: flatten markup at most once; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
20948
9b9910b82645 initial draft
haftmann
parents:
diff changeset
     1
28419
f65e8b318581 re-canibalised manual
haftmann
parents: 28213
diff changeset
     2
no_document use_thy "Setup";
28213
b52f9205a02d New outline for codegen tutorial -- draft
haftmann
parents: 21147
diff changeset
     3
b52f9205a02d New outline for codegen tutorial -- draft
haftmann
parents: 21147
diff changeset
     4
use_thy "Introduction";
38405
7935b334893e sketch of new outline
haftmann
parents: 37613
diff changeset
     5
use_thy "Foundations";
7935b334893e sketch of new outline
haftmann
parents: 37613
diff changeset
     6
use_thy "Refinement";
37613
355ec1b521e6 split off predicate compiler into separate theory
haftmann
parents: 31050
diff changeset
     7
use_thy "Inductive_Predicate";
31050
555b56b66fcf adaptation replaces adaption
haftmann
parents: 30734
diff changeset
     8
use_thy "Adaptation";
28213
b52f9205a02d New outline for codegen tutorial -- draft
haftmann
parents: 21147
diff changeset
     9
use_thy "Further";