src/Pure/ROOT
author wenzelm
Tue Aug 19 18:11:04 2014 +0200 (2014-08-19)
changeset 58009 987c848d509b
parent 57934 5e500c0e7eca
child 58470 890d8286fd4e
permissions -rw-r--r--
clarified modules;
     1 chapter Pure
     2 
     3 session RAW =
     4   theories
     5   files
     6     "General/exn.ML"
     7     "ML-Systems/compiler_polyml.ML"
     8     "ML-Systems/ml_name_space.ML"
     9     "ML-Systems/ml_positions.ML"
    10     "ML-Systems/ml_pretty.ML"
    11     "ML-Systems/ml_system.ML"
    12     "ML-Systems/multithreading.ML"
    13     "ML-Systems/multithreading_polyml.ML"
    14     "ML-Systems/overloading_smlnj.ML"
    15     "ML-Systems/polyml.ML"
    16     "ML-Systems/polyml-5.5.2.ML"
    17     "ML-Systems/pp_dummy.ML"
    18     "ML-Systems/proper_int.ML"
    19     "ML-Systems/single_assignment.ML"
    20     "ML-Systems/single_assignment_polyml.ML"
    21     "ML-Systems/share_common_data_polyml-5.3.0.ML"
    22     "ML-Systems/smlnj.ML"
    23     "ML-Systems/thread_dummy.ML"
    24     "ML-Systems/universal.ML"
    25     "ML-Systems/unsynchronized.ML"
    26     "ML-Systems/use_context.ML"
    27 
    28 session Pure =
    29   global_theories Pure
    30   files
    31     "General/exn.ML"
    32     "ML-Systems/compiler_polyml.ML"
    33     "ML-Systems/ml_name_space.ML"
    34     "ML-Systems/ml_positions.ML"
    35     "ML-Systems/ml_pretty.ML"
    36     "ML-Systems/ml_system.ML"
    37     "ML-Systems/multithreading.ML"
    38     "ML-Systems/multithreading_polyml.ML"
    39     "ML-Systems/overloading_smlnj.ML"
    40     "ML-Systems/polyml.ML"
    41     "ML-Systems/polyml-5.5.2.ML"
    42     "ML-Systems/pp_dummy.ML"
    43     "ML-Systems/proper_int.ML"
    44     "ML-Systems/single_assignment.ML"
    45     "ML-Systems/single_assignment_polyml.ML"
    46     "ML-Systems/smlnj.ML"
    47     "ML-Systems/thread_dummy.ML"
    48     "ML-Systems/universal.ML"
    49     "ML-Systems/unsynchronized.ML"
    50     "ML-Systems/use_context.ML"
    51 
    52     "Concurrent/bash.ML"
    53     "Concurrent/bash_sequential.ML"
    54     "Concurrent/cache.ML"
    55     "Concurrent/event_timer.ML"
    56     "Concurrent/future.ML"
    57     "Concurrent/lazy.ML"
    58     "Concurrent/lazy_sequential.ML"
    59     "Concurrent/mailbox.ML"
    60     "Concurrent/par_exn.ML"
    61     "Concurrent/par_list.ML"
    62     "Concurrent/par_list_sequential.ML"
    63     "Concurrent/simple_thread.ML"
    64     "Concurrent/single_assignment.ML"
    65     "Concurrent/single_assignment_sequential.ML"
    66     "Concurrent/synchronized.ML"
    67     "Concurrent/synchronized_sequential.ML"
    68     "Concurrent/task_queue.ML"
    69     "Concurrent/time_limit.ML"
    70     "General/alist.ML"
    71     "General/antiquote.ML"
    72     "General/balanced_tree.ML"
    73     "General/basics.ML"
    74     "General/binding.ML"
    75     "General/buffer.ML"
    76     "General/change_table.ML"
    77     "General/completion.ML"
    78     "General/file.ML"
    79     "General/graph.ML"
    80     "General/graph_display.ML"
    81     "General/heap.ML"
    82     "General/integer.ML"
    83     "General/linear_set.ML"
    84     "General/long_name.ML"
    85     "General/name_space.ML"
    86     "General/ord_list.ML"
    87     "General/output.ML"
    88     "General/path.ML"
    89     "General/position.ML"
    90     "General/pretty.ML"
    91     "General/print_mode.ML"
    92     "General/properties.ML"
    93     "General/queue.ML"
    94     "General/same.ML"
    95     "General/scan.ML"
    96     "General/secure.ML"
    97     "General/seq.ML"
    98     "General/sha1.ML"
    99     "General/sha1_polyml.ML"
   100     "General/sha1_samples.ML"
   101     "General/socket_io.ML"
   102     "General/source.ML"
   103     "General/stack.ML"
   104     "General/symbol.ML"
   105     "General/symbol_pos.ML"
   106     "General/table.ML"
   107     "General/timing.ML"
   108     "General/url.ML"
   109     "Isar/args.ML"
   110     "Isar/attrib.ML"
   111     "Isar/auto_bind.ML"
   112     "Isar/bundle.ML"
   113     "Isar/class.ML"
   114     "Isar/class_declaration.ML"
   115     "Isar/code.ML"
   116     "Isar/context_rules.ML"
   117     "Isar/element.ML"
   118     "Isar/expression.ML"
   119     "Isar/generic_target.ML"
   120     "Isar/isar_cmd.ML"
   121     "Isar/keyword.ML"
   122     "Isar/local_defs.ML"
   123     "Isar/local_theory.ML"
   124     "Isar/locale.ML"
   125     "Isar/method.ML"
   126     "Isar/named_target.ML"
   127     "Isar/object_logic.ML"
   128     "Isar/obtain.ML"
   129     "Isar/outer_syntax.ML"
   130     "Isar/overloading.ML"
   131     "Isar/parse.ML"
   132     "Isar/parse_spec.ML"
   133     "Isar/proof.ML"
   134     "Isar/proof_context.ML"
   135     "Isar/proof_display.ML"
   136     "Isar/proof_node.ML"
   137     "Isar/rule_cases.ML"
   138     "Isar/runtime.ML"
   139     "Isar/spec_rules.ML"
   140     "Isar/specification.ML"
   141     "Isar/token.ML"
   142     "Isar/toplevel.ML"
   143     "Isar/typedecl.ML"
   144     "ML/exn_output.ML"
   145     "ML/exn_output_polyml.ML"
   146     "ML/exn_properties_dummy.ML"
   147     "ML/exn_properties_polyml.ML"
   148     "ML/exn_trace_polyml-5.5.1.ML"
   149     "ML/install_pp_polyml.ML"
   150     "ML/ml_antiquotation.ML"
   151     "ML/ml_compiler.ML"
   152     "ML/ml_compiler_polyml.ML"
   153     "ML/ml_context.ML"
   154     "ML/ml_env.ML"
   155     "ML/ml_lex.ML"
   156     "ML/ml_parse.ML"
   157     "ML/ml_options.ML"
   158     "ML/ml_statistics_dummy.ML"
   159     "ML/ml_statistics_polyml-5.5.0.ML"
   160     "ML/ml_syntax.ML"
   161     "PIDE/active.ML"
   162     "PIDE/command.ML"
   163     "PIDE/command_span.ML"
   164     "PIDE/document.ML"
   165     "PIDE/document_id.ML"
   166     "PIDE/execution.ML"
   167     "PIDE/markup.ML"
   168     "PIDE/protocol.ML"
   169     "PIDE/query_operation.ML"
   170     "PIDE/resources.ML"
   171     "PIDE/session.ML"
   172     "PIDE/xml.ML"
   173     "PIDE/yxml.ML"
   174     "Proof/extraction.ML"
   175     "Proof/proof_checker.ML"
   176     "Proof/proof_rewrite_rules.ML"
   177     "Proof/proof_syntax.ML"
   178     "Proof/reconstruct.ML"
   179     "ROOT.ML"
   180     "Syntax/ast.ML"
   181     "Syntax/lexicon.ML"
   182     "Syntax/local_syntax.ML"
   183     "Syntax/mixfix.ML"
   184     "Syntax/parser.ML"
   185     "Syntax/printer.ML"
   186     "Syntax/simple_syntax.ML"
   187     "Syntax/syntax.ML"
   188     "Syntax/syntax_ext.ML"
   189     "Syntax/syntax_phases.ML"
   190     "Syntax/syntax_trans.ML"
   191     "Syntax/term_position.ML"
   192     "Syntax/type_annotation.ML"
   193     "System/command_line.ML"
   194     "System/invoke_scala.ML"
   195     "System/isabelle_process.ML"
   196     "System/isabelle_system.ML"
   197     "System/isar.ML"
   198     "System/message_channel.ML"
   199     "System/options.ML"
   200     "System/system_channel.ML"
   201     "Thy/html.ML"
   202     "Thy/latex.ML"
   203     "Thy/present.ML"
   204     "Thy/term_style.ML"
   205     "Thy/thy_header.ML"
   206     "Thy/thy_info.ML"
   207     "Thy/thy_output.ML"
   208     "Thy/thy_syntax.ML"
   209     "Tools/build.ML"
   210     "Tools/named_thms.ML"
   211     "Tools/proof_general.ML"
   212     "assumption.ML"
   213     "axclass.ML"
   214     "config.ML"
   215     "conjunction.ML"
   216     "consts.ML"
   217     "context.ML"
   218     "context_position.ML"
   219     "conv.ML"
   220     "defs.ML"
   221     "display.ML"
   222     "drule.ML"
   223     "envir.ML"
   224     "facts.ML"
   225     "global_theory.ML"
   226     "goal.ML"
   227     "goal_display.ML"
   228     "interpretation.ML"
   229     "item_net.ML"
   230     "library.ML"
   231     "logic.ML"
   232     "more_thm.ML"
   233     "morphism.ML"
   234     "name.ML"
   235     "net.ML"
   236     "par_tactical.ML"
   237     "pattern.ML"
   238     "primitive_defs.ML"
   239     "proofterm.ML"
   240     "pure_syn.ML"
   241     "pure_thy.ML"
   242     "raw_simplifier.ML"
   243     "search.ML"
   244     "sign.ML"
   245     "simplifier.ML"
   246     "skip_proof.ML"
   247     "sorts.ML"
   248     "subgoal.ML"
   249     "tactic.ML"
   250     "tactical.ML"
   251     "term.ML"
   252     "term_ord.ML"
   253     "term_sharing.ML"
   254     "term_subst.ML"
   255     "term_xml.ML"
   256     "theory.ML"
   257     "thm.ML"
   258     "type.ML"
   259     "type_infer.ML"
   260     "type_infer_context.ML"
   261     "unify.ML"
   262     "variable.ML"
   263