1(* Title: Pure/ROOT.ML 2 Author: Makarius 3 4Main entry point for the Isabelle/Pure bootstrap process. 5 6Note: When this file is open in the Prover IDE, the ML files of 7Isabelle/Pure can be explored interactively. This is a separate copy of 8Pure within Pure: it does not affect the running logic session. 9*) 10 11chapter "Isabelle/Pure bootstrap"; 12 13ML_file "ML/ml_name_space.ML"; 14 15 16section "Bootstrap phase 0: Poly/ML setup"; 17 18ML_file "ML/ml_init.ML"; 19ML_file "ML/ml_system.ML"; 20ML_file "System/distribution.ML"; 21 22ML_file "General/basics.ML"; 23ML_file "General/symbol_explode.ML"; 24 25ML_file "Concurrent/multithreading.ML"; 26ML_file "Concurrent/unsynchronized.ML"; 27ML_file "Concurrent/synchronized.ML"; 28ML_file "Concurrent/counter.ML"; 29 30ML_file "ML/ml_heap.ML"; 31ML_file "ML/ml_profiling.ML"; 32ML_file "ML/ml_print_depth0.ML"; 33ML_file "ML/ml_pretty.ML"; 34ML_file "ML/ml_compiler0.ML"; 35 36 37section "Bootstrap phase 1: towards ML within position context"; 38 39subsection "Library of general tools"; 40 41ML_file "library.ML"; 42ML_file "General/print_mode.ML"; 43ML_file "General/alist.ML"; 44ML_file "General/table.ML"; 45 46ML_file "General/random.ML"; 47ML_file "General/value.ML"; 48ML_file "General/properties.ML"; 49ML_file "General/output.ML"; 50ML_file "PIDE/markup.ML"; 51ML_file "General/scan.ML"; 52ML_file "General/source.ML"; 53ML_file "General/symbol.ML"; 54ML_file "General/position.ML"; 55ML_file "General/symbol_pos.ML"; 56ML_file "General/input.ML"; 57ML_file "General/comment.ML"; 58ML_file "General/antiquote.ML"; 59ML_file "ML/ml_lex.ML"; 60ML_file "ML/ml_compiler1.ML"; 61 62 63section "Bootstrap phase 2: towards ML within Isar context"; 64 65subsection "Library of general tools"; 66 67ML_file "General/integer.ML"; 68ML_file "General/stack.ML"; 69ML_file "General/queue.ML"; 70ML_file "General/heap.ML"; 71ML_file "General/same.ML"; 72ML_file "General/ord_list.ML"; 73ML_file "General/balanced_tree.ML"; 74ML_file "General/linear_set.ML"; 75ML_file "General/buffer.ML"; 76ML_file "General/pretty.ML"; 77ML_file "General/rat.ML"; 78ML_file "PIDE/xml.ML"; 79ML_file "General/path.ML"; 80ML_file "General/url.ML"; 81ML_file "System/bash_syntax.ML"; 82ML_file "General/file.ML"; 83ML_file "General/long_name.ML"; 84ML_file "General/binding.ML"; 85ML_file "General/socket_io.ML"; 86ML_file "General/seq.ML"; 87ML_file "General/timing.ML"; 88ML_file "General/sha1.ML"; 89 90ML_file "PIDE/yxml.ML"; 91ML_file "PIDE/document_id.ML"; 92 93ML_file "General/change_table.ML"; 94ML_file "General/graph.ML"; 95 96 97subsection "Fundamental structures"; 98 99ML_file "name.ML"; 100ML_file "term.ML"; 101ML_file "context.ML"; 102ML_file "context_position.ML"; 103ML_file "System/options.ML"; 104ML_file "config.ML"; 105 106 107subsection "Concurrency within the ML runtime"; 108 109ML_file "ML/exn_properties.ML"; 110 111ML_file "ML/ml_statistics.ML"; 112 113ML_file "Concurrent/thread_data_virtual.ML"; 114ML_file "Concurrent/standard_thread.ML"; 115ML_file "Concurrent/single_assignment.ML"; 116 117ML_file "Concurrent/par_exn.ML"; 118ML_file "Concurrent/task_queue.ML"; 119ML_file "Concurrent/future.ML"; 120ML_file "Concurrent/event_timer.ML"; 121ML_file "Concurrent/timeout.ML"; 122ML_file "Concurrent/lazy.ML"; 123ML_file "Concurrent/par_list.ML"; 124 125ML_file "Concurrent/mailbox.ML"; 126ML_file "Concurrent/cache.ML"; 127 128ML_file "PIDE/active.ML"; 129 130 131subsection "Inner syntax"; 132 133ML_file "Syntax/type_annotation.ML"; 134ML_file "Syntax/term_position.ML"; 135ML_file "Syntax/lexicon.ML"; 136ML_file "Syntax/ast.ML"; 137ML_file "Syntax/syntax_ext.ML"; 138ML_file "Syntax/parser.ML"; 139ML_file "Syntax/syntax_trans.ML"; 140ML_file "Syntax/mixfix.ML"; 141ML_file "Syntax/printer.ML"; 142ML_file "Syntax/syntax.ML"; 143 144 145subsection "Core of tactical proof system"; 146 147ML_file "term_ord.ML"; 148ML_file "term_subst.ML"; 149ML_file "term_xml.ML"; 150ML_file "General/completion.ML"; 151ML_file "General/name_space.ML"; 152ML_file "sorts.ML"; 153ML_file "type.ML"; 154ML_file "logic.ML"; 155ML_file "Syntax/simple_syntax.ML"; 156ML_file "net.ML"; 157ML_file "item_net.ML"; 158ML_file "envir.ML"; 159ML_file "consts.ML"; 160ML_file "primitive_defs.ML"; 161ML_file "sign.ML"; 162ML_file "defs.ML"; 163ML_file "term_sharing.ML"; 164ML_file "pattern.ML"; 165ML_file "unify.ML"; 166ML_file "theory.ML"; 167ML_file "proofterm.ML"; 168ML_file "thm.ML"; 169ML_file "more_pattern.ML"; 170ML_file "more_unify.ML"; 171ML_file "more_thm.ML"; 172ML_file "facts.ML"; 173ML_file "global_theory.ML"; 174ML_file "pure_thy.ML"; 175ML_file "drule.ML"; 176ML_file "morphism.ML"; 177ML_file "variable.ML"; 178ML_file "conv.ML"; 179ML_file "goal_display.ML"; 180ML_file "tactical.ML"; 181ML_file "search.ML"; 182ML_file "tactic.ML"; 183ML_file "raw_simplifier.ML"; 184ML_file "conjunction.ML"; 185ML_file "assumption.ML"; 186 187 188subsection "Isar -- Intelligible Semi-Automated Reasoning"; 189 190(*ML support and global execution*) 191ML_file "ML/ml_syntax.ML"; 192ML_file "ML/ml_env.ML"; 193ML_file "ML/ml_options.ML"; 194ML_file "ML/ml_print_depth.ML"; 195ML_file_no_debug "ML/exn_debugger.ML"; 196ML_file_no_debug "Isar/runtime.ML"; 197ML_file "PIDE/execution.ML"; 198ML_file "ML/ml_compiler.ML"; 199 200ML_file "skip_proof.ML"; 201ML_file "goal.ML"; 202 203(*outer syntax*) 204ML_file "Isar/keyword.ML"; 205ML_file "Isar/token.ML"; 206ML_file "Isar/parse.ML"; 207ML_file "Thy/thy_header.ML"; 208 209(*proof context*) 210ML_file "Isar/object_logic.ML"; 211ML_file "Isar/rule_cases.ML"; 212ML_file "Isar/auto_bind.ML"; 213ML_file "type_infer.ML"; 214ML_file "Syntax/local_syntax.ML"; 215ML_file "Isar/proof_context.ML"; 216ML_file "type_infer_context.ML"; 217ML_file "Syntax/syntax_phases.ML"; 218ML_file "Isar/args.ML"; 219 220(*theory specifications*) 221ML_file "Isar/local_defs.ML"; 222ML_file "Isar/local_theory.ML"; 223ML_file "Isar/entity.ML"; 224ML_file "PIDE/command_span.ML"; 225ML_file "Thy/thy_syntax.ML"; 226ML_file "Thy/markdown.ML"; 227ML_file "Thy/html.ML"; 228ML_file "Thy/latex.ML"; 229 230(*ML with context and antiquotations*) 231ML_file "ML/ml_context.ML"; 232ML_file "ML/ml_antiquotation.ML"; 233ML_file "ML/ml_compiler2.ML"; 234 235 236section "Bootstrap phase 3: towards theory Pure and final ML toplevel setup"; 237 238(*basic proof engine*) 239ML_file "par_tactical.ML"; 240ML_file "Isar/proof_display.ML"; 241ML_file "Isar/attrib.ML"; 242ML_file "Isar/context_rules.ML"; 243ML_file "Isar/method.ML"; 244ML_file "Isar/proof.ML"; 245ML_file "Isar/element.ML"; 246ML_file "Isar/obtain.ML"; 247ML_file "Isar/subgoal.ML"; 248ML_file "Isar/calculation.ML"; 249 250(*local theories and targets*) 251ML_file "Isar/locale.ML"; 252ML_file "Isar/generic_target.ML"; 253ML_file "Isar/overloading.ML"; 254ML_file "axclass.ML"; 255ML_file "Isar/class.ML"; 256ML_file "Isar/named_target.ML"; 257ML_file "Isar/expression.ML"; 258ML_file "Isar/interpretation.ML"; 259ML_file "Isar/class_declaration.ML"; 260ML_file "Isar/bundle.ML"; 261ML_file "Isar/experiment.ML"; 262 263ML_file "simplifier.ML"; 264ML_file "Tools/plugin.ML"; 265 266(*executable theory content*) 267ML_file "Isar/code.ML"; 268 269(*specifications*) 270ML_file "Isar/spec_rules.ML"; 271ML_file "Isar/specification.ML"; 272ML_file "Isar/parse_spec.ML"; 273ML_file "Isar/typedecl.ML"; 274 275(*toplevel transactions*) 276ML_file "Isar/proof_node.ML"; 277ML_file "Isar/toplevel.ML"; 278 279(*proof term operations*) 280ML_file "Proof/reconstruct.ML"; 281ML_file "Proof/proof_syntax.ML"; 282ML_file "Proof/proof_rewrite_rules.ML"; 283ML_file "Proof/proof_checker.ML"; 284ML_file "Proof/extraction.ML"; 285 286(*Isabelle system*) 287ML_file "System/bash.ML"; 288ML_file "System/isabelle_system.ML"; 289 290 291(*theory documents*) 292ML_file "Thy/term_style.ML"; 293ML_file "Isar/outer_syntax.ML"; 294ML_file "ML/ml_antiquotations.ML"; 295ML_file "Thy/document_antiquotation.ML"; 296ML_file "Thy/thy_output.ML"; 297ML_file "Thy/document_antiquotations.ML"; 298ML_file "General/graph_display.ML"; 299ML_file "pure_syn.ML"; 300ML_file "PIDE/command.ML"; 301ML_file "PIDE/query_operation.ML"; 302ML_file "PIDE/resources.ML"; 303ML_file "Thy/export.ML"; 304ML_file "Thy/present.ML"; 305ML_file "Thy/thy_info.ML"; 306ML_file "Thy/export_theory.ML"; 307ML_file "Thy/sessions.ML"; 308ML_file "PIDE/session.ML"; 309ML_file "PIDE/protocol_message.ML"; 310ML_file "PIDE/document.ML"; 311 312(*theory and proof operations*) 313ML_file "Isar/isar_cmd.ML"; 314 315 316subsection "Isabelle/Isar system"; 317 318ML_file "System/command_line.ML"; 319ML_file "System/system_channel.ML"; 320ML_file "System/message_channel.ML"; 321ML_file "System/isabelle_process.ML"; 322ML_file "System/invoke_scala.ML"; 323ML_file "Thy/bibtex.ML"; 324ML_file "PIDE/protocol.ML"; 325ML_file "General/output_primitives_virtual.ML"; 326 327 328subsection "Miscellaneous tools and packages for Pure Isabelle"; 329 330ML_file "ML/ml_pp.ML"; 331ML_file "ML/ml_thms.ML"; 332ML_file "ML/ml_file.ML"; 333 334ML_file "Tools/build.ML"; 335ML_file "Tools/named_thms.ML"; 336ML_file "Tools/print_operation.ML"; 337ML_file "Tools/rail.ML"; 338ML_file "Tools/rule_insts.ML"; 339ML_file "Tools/thm_deps.ML"; 340ML_file "Tools/thy_deps.ML"; 341ML_file "Tools/class_deps.ML"; 342ML_file "Tools/find_theorems.ML"; 343ML_file "Tools/find_consts.ML"; 344ML_file "Tools/simplifier_trace.ML"; 345ML_file_no_debug "Tools/debugger.ML"; 346ML_file "Tools/named_theorems.ML"; 347ML_file "Tools/jedit.ML"; 348