wenzelm@31432: (** Pure Isabelle **) clasohm@0: wenzelm@26109: structure Distribution = (*filled-in by makedist*) wenzelm@26109: struct wenzelm@32361: val version = "unidentified repository version"; wenzelm@27642: val is_official = false; wenzelm@26109: end; wenzelm@11835: wenzelm@12248: print_depth 10; clasohm@0: wenzelm@31432: wenzelm@31432: (* library of general tools *) wenzelm@31432: wenzelm@21396: use "General/basics.ML"; clasohm@0: use "library.ML"; wenzelm@31432: use "General/print_mode.ML"; wenzelm@31432: use "General/alist.ML"; wenzelm@31432: use "General/table.ML"; wenzelm@43684: wenzelm@43684: use "Concurrent/simple_thread.ML"; wenzelm@43684: wenzelm@43684: use "Concurrent/synchronized.ML"; wenzelm@43684: if Multithreading.available then () wenzelm@43684: else use "Concurrent/synchronized_sequential.ML"; wenzelm@43684: wenzelm@43746: use "General/properties.ML"; wenzelm@31432: use "General/output.ML"; wenzelm@45670: use "PIDE/markup.ML"; wenzelm@50201: fun legacy_feature s = warning (Markup.markup Markup.legacy ("Legacy feature! " ^ s)); wenzelm@51606: use "General/timing.ML"; wenzelm@31432: use "General/scan.ML"; wenzelm@31432: use "General/source.ML"; wenzelm@31432: use "General/symbol.ML"; wenzelm@31432: use "General/seq.ML"; wenzelm@31432: use "General/position.ML"; wenzelm@31432: use "General/symbol_pos.ML"; wenzelm@31432: use "General/antiquote.ML"; wenzelm@31432: use "ML/ml_lex.ML"; wenzelm@31432: use "ML/ml_parse.ML"; wenzelm@31432: use "General/secure.ML"; wenzelm@32015: (*^^^^^ end of basic ML bootstrap ^^^^^*) wenzelm@31432: use "General/integer.ML"; wenzelm@31432: use "General/stack.ML"; wenzelm@31432: use "General/queue.ML"; wenzelm@31432: use "General/heap.ML"; wenzelm@32015: use "General/same.ML"; wenzelm@31432: use "General/ord_list.ML"; wenzelm@31432: use "General/balanced_tree.ML"; wenzelm@38448: use "General/linear_set.ML"; wenzelm@43593: use "General/buffer.ML"; wenzelm@43791: use "General/pretty.ML"; wenzelm@31432: use "General/path.ML"; wenzelm@31432: use "General/url.ML"; wenzelm@31432: use "General/file.ML"; wenzelm@43547: use "General/long_name.ML"; wenzelm@43547: use "General/binding.ML"; wenzelm@50800: use "General/socket_io.ML"; wenzelm@22592: wenzelm@35628: use "General/sha1.ML"; wenzelm@43948: if ML_System.is_polyml then use "General/sha1_polyml.ML" else (); wenzelm@35628: wenzelm@44698: use "PIDE/xml.ML"; wenzelm@44698: use "PIDE/yxml.ML"; wenzelm@44698: wenzelm@49560: use "General/graph.ML"; wenzelm@49560: wenzelm@51947: use "System/options.ML"; wenzelm@51947: wenzelm@31432: wenzelm@31432: (* concurrency within the ML runtime *) wenzelm@28120: wenzelm@52050: use "Concurrent/event_timer.ML"; wenzelm@52050: wenzelm@50911: if ML_System.is_polyml wenzelm@50911: then use "ML/exn_properties_polyml.ML" wenzelm@50911: else use "ML/exn_properties_dummy.ML"; wenzelm@50911: wenzelm@50255: if ML_System.name = "polyml-5.5.0" wenzelm@50255: then use "ML/ml_statistics_polyml-5.5.0.ML" wenzelm@50255: else use "ML/ml_statistics_dummy.ML"; wenzelm@50255: wenzelm@35014: use "Concurrent/single_assignment.ML"; wenzelm@35014: if Multithreading.available then () wenzelm@35014: else use "Concurrent/single_assignment_sequential.ML"; wenzelm@35014: wenzelm@47980: if ML_System.is_polyml then use "Concurrent/time_limit.ML" else (); wenzelm@41710: wenzelm@40748: if Multithreading.available wenzelm@40748: then use "Concurrent/bash.ML" wenzelm@40748: else use "Concurrent/bash_sequential.ML"; wenzelm@40748: wenzelm@44247: use "Concurrent/par_exn.ML"; wenzelm@31432: use "Concurrent/task_queue.ML"; wenzelm@31432: use "Concurrent/future.ML"; wenzelm@32840: wenzelm@32815: use "Concurrent/lazy.ML"; wenzelm@32815: if Multithreading.available then () wenzelm@32815: else use "Concurrent/lazy_sequential.ML"; wenzelm@32840: wenzelm@31432: use "Concurrent/par_list.ML"; wenzelm@32815: if Multithreading.available then () wenzelm@32816: else use "Concurrent/par_list_sequential.ML"; wenzelm@31432: wenzelm@44247: use "Concurrent/mailbox.ML"; wenzelm@32840: use "Concurrent/cache.ML"; wenzelm@32840: wenzelm@50500: use "PIDE/active.ML"; wenzelm@50500: wenzelm@31432: wenzelm@31432: (* fundamental structures *) wenzelm@31432: wenzelm@20075: use "name.ML"; clasohm@0: use "term.ML"; wenzelm@28404: use "context.ML"; wenzelm@47813: use "context_position.ML"; wenzelm@39508: use "config.ML"; wenzelm@19: wenzelm@52059: val quick_and_dirty_raw = Config.declare_option "quick_and_dirty"; wenzelm@52059: val quick_and_dirty = Config.bool quick_and_dirty_raw; wenzelm@52059: wenzelm@31432: wenzelm@31432: (* inner syntax *) wenzelm@31432: wenzelm@52211: use "Syntax/type_annotation.ML"; wenzelm@42264: use "Syntax/term_position.ML"; wenzelm@42264: use "Syntax/lexicon.ML"; wenzelm@22679: use "Syntax/ast.ML"; wenzelm@42288: use "Syntax/syntax_ext.ML"; wenzelm@22679: use "Syntax/parser.ML"; wenzelm@42284: use "Syntax/syntax_trans.ML"; wenzelm@22679: use "Syntax/mixfix.ML"; wenzelm@22679: use "Syntax/printer.ML"; wenzelm@22679: use "Syntax/syntax.ML"; wenzelm@22679: wenzelm@31432: wenzelm@31432: (* core of tactical proof system *) wenzelm@31432: wenzelm@42382: use "term_ord.ML"; wenzelm@42382: use "term_subst.ML"; wenzelm@43729: use "term_xml.ML"; wenzelm@42382: use "General/name_space.ML"; wenzelm@42382: use "sorts.ML"; wenzelm@42382: use "type.ML"; wenzelm@42382: use "logic.ML"; wenzelm@42382: use "Syntax/simple_syntax.ML"; wenzelm@30559: use "net.ML"; wenzelm@30559: use "item_net.ML"; wenzelm@18934: use "envir.ML"; wenzelm@18059: use "consts.ML"; wenzelm@24257: use "primitive_defs.ML"; haftmann@27546: use "defs.ML"; clasohm@0: use "sign.ML"; wenzelm@43795: use "term_sharing.ML"; clasohm@0: use "pattern.ML"; clasohm@0: use "unify.ML"; paulson@1528: use "theory.ML"; wenzelm@24664: use "interpretation.ML"; berghofe@11511: use "proofterm.ML"; clasohm@0: use "thm.ML"; wenzelm@22361: use "more_thm.ML"; wenzelm@26279: use "facts.ML"; wenzelm@39557: use "global_theory.ML"; wenzelm@3986: use "pure_thy.ML"; clasohm@0: use "drule.ML"; wenzelm@22233: use "morphism.ML"; wenzelm@19898: use "variable.ML"; wenzelm@24833: use "conv.ML"; wenzelm@32187: use "goal_display.ML"; wenzelm@32169: use "tactical.ML"; paulson@1582: use "search.ML"; wenzelm@21708: use "tactic.ML"; wenzelm@41228: use "raw_simplifier.ML"; wenzelm@19417: use "conjunction.ML"; wenzelm@20225: use "assumption.ML"; wenzelm@32089: use "display.ML"; clasohm@0: wenzelm@31432: wenzelm@31432: (* Isar -- Intelligible Semi-Automated Reasoning *) wenzelm@31432: wenzelm@49041: (*ML support*) wenzelm@49041: use "ML/ml_syntax.ML"; wenzelm@49041: use "ML/ml_env.ML"; wenzelm@49041: use "Isar/runtime.ML"; wenzelm@49041: use "ML/ml_compiler.ML"; wenzelm@49041: if ML_System.is_polyml then use "ML/ml_compiler_polyml.ML" else (); wenzelm@49041: wenzelm@51551: use "skip_proof.ML"; wenzelm@49041: use "goal.ML"; wenzelm@49041: wenzelm@31432: (*proof context*) wenzelm@31432: use "Isar/object_logic.ML"; wenzelm@31432: use "Isar/rule_cases.ML"; wenzelm@31432: use "Isar/auto_bind.ML"; wenzelm@42241: use "type_infer.ML"; wenzelm@42240: use "Syntax/local_syntax.ML"; wenzelm@31432: use "Isar/proof_context.ML"; wenzelm@42405: use "type_infer_context.ML"; wenzelm@42243: use "Syntax/syntax_phases.ML"; wenzelm@31432: use "Isar/local_defs.ML"; wenzelm@31432: wenzelm@31432: (*proof term operations*) wenzelm@31432: use "Proof/reconstruct.ML"; wenzelm@31432: use "Proof/proof_syntax.ML"; wenzelm@31432: use "Proof/proof_rewrite_rules.ML"; wenzelm@44062: use "Proof/proof_checker.ML"; wenzelm@31432: wenzelm@31432: (*outer syntax*) wenzelm@36959: use "Isar/token.ML"; wenzelm@36949: use "Isar/keyword.ML"; wenzelm@36949: use "Isar/parse.ML"; wenzelm@31432: use "Isar/args.ML"; wenzelm@31432: use "ML/ml_context.ML"; wenzelm@31432: wenzelm@31432: (*theory sources*) wenzelm@31432: use "Thy/thy_header.ML"; wenzelm@51265: use "Thy/thy_syntax.ML"; wenzelm@31432: use "Thy/html.ML"; wenzelm@31432: use "Thy/latex.ML"; wenzelm@31432: wenzelm@31432: (*basic proof engine*) wenzelm@31432: use "Isar/proof_display.ML"; wenzelm@31432: use "Isar/attrib.ML"; wenzelm@31432: use "ML/ml_antiquote.ML"; wenzelm@31432: use "Isar/context_rules.ML"; wenzelm@31432: use "Isar/method.ML"; wenzelm@31432: use "Isar/proof.ML"; wenzelm@31432: use "Isar/element.ML"; wenzelm@31432: wenzelm@31432: (*derived theory and proof elements*) wenzelm@31432: use "Isar/calculation.ML"; wenzelm@31432: use "Isar/obtain.ML"; wenzelm@31432: wenzelm@31432: (*local theories and targets*) haftmann@52140: use "Isar/locale.ML"; wenzelm@31432: use "Isar/local_theory.ML"; haftmann@38307: use "Isar/generic_target.ML"; wenzelm@31432: use "Isar/overloading.ML"; wenzelm@35669: use "axclass.ML"; haftmann@38379: use "Isar/class.ML"; haftmann@38350: use "Isar/named_target.ML"; wenzelm@31432: use "Isar/expression.ML"; haftmann@38379: use "Isar/class_declaration.ML"; wenzelm@47057: use "Isar/bundle.ML"; wenzelm@31432: wenzelm@31432: use "simplifier.ML"; wenzelm@31432: wenzelm@31432: (*executable theory content*) wenzelm@31432: use "Isar/code.ML"; wenzelm@31432: wenzelm@31432: (*specifications*) wenzelm@36952: use "Isar/parse_spec.ML"; wenzelm@33374: use "Isar/spec_rules.ML"; wenzelm@31432: use "Isar/specification.ML"; wenzelm@35626: use "Isar/typedecl.ML"; wenzelm@45592: use "ML/ml_thms.ML"; wenzelm@31432: wenzelm@31432: (*toplevel transactions*) wenzelm@31432: use "Isar/proof_node.ML"; wenzelm@52536: use "PIDE/document_id.ML"; wenzelm@31432: use "Isar/toplevel.ML"; wenzelm@31432: wenzelm@38271: (*theory documents*) wenzelm@40743: use "System/isabelle_system.ML"; wenzelm@31432: use "Thy/term_style.ML"; wenzelm@31432: use "Thy/thy_output.ML"; wenzelm@31432: use "Isar/outer_syntax.ML"; wenzelm@49561: use "General/graph_display.ML"; wenzelm@43712: use "Thy/present.ML"; wenzelm@52510: use "PIDE/command.ML"; wenzelm@43712: use "Thy/thy_load.ML"; wenzelm@31432: use "Thy/thy_info.ML"; wenzelm@44185: use "PIDE/document.ML"; wenzelm@42504: use "Thy/rail.ML"; wenzelm@31432: wenzelm@31432: (*theory and proof operations*) wenzelm@31432: use "Isar/rule_insts.ML"; wenzelm@31432: use "Thy/thm_deps.ML"; wenzelm@31432: use "Isar/isar_cmd.ML"; wenzelm@31432: wenzelm@20207: use "subgoal.ML"; wenzelm@5834: berghofe@13402: use "Proof/extraction.ML"; berghofe@11511: wenzelm@31432: wenzelm@31432: (* Isabelle/Isar system *) wenzelm@31432: wenzelm@30173: use "System/session.ML"; wenzelm@48681: use "System/command_line.ML"; wenzelm@45029: use "System/system_channel.ML"; wenzelm@38412: use "System/isabelle_process.ML"; wenzelm@43748: use "System/invoke_scala.ML"; wenzelm@45709: use "PIDE/protocol.ML"; wenzelm@30173: use "System/isar.ML"; wenzelm@30173: wenzelm@31432: wenzelm@31432: (* miscellaneous tools and packages for Pure Isabelle *) wenzelm@31432: wenzelm@50686: use "Tools/build.ML"; wenzelm@31432: use "Tools/named_thms.ML"; wenzelm@52009: use "Tools/proof_general.ML"; wenzelm@50217: use "Tools/legacy_xml_syntax.ML"; wenzelm@31432: wenzelm@31432: wenzelm@48732: (* ML toplevel pretty printing *) wenzelm@48732: wenzelm@48732: toplevel_pp ["Pretty", "T"] "(fn _: Pretty.T => Pretty.str \"\")"; wenzelm@48732: toplevel_pp ["Task_Queue", "task"] "Pretty.str o Task_Queue.str_of_task"; wenzelm@48732: toplevel_pp ["Task_Queue", "group"] "Pretty.str o Task_Queue.str_of_group"; wenzelm@48732: toplevel_pp ["Position", "T"] "Pretty.position"; wenzelm@48732: toplevel_pp ["Binding", "binding"] "Pretty.str o Binding.print"; wenzelm@48732: toplevel_pp ["Thm", "thm"] "Proof_Display.pp_thm"; wenzelm@48732: toplevel_pp ["Thm", "cterm"] "Proof_Display.pp_cterm"; wenzelm@48732: toplevel_pp ["Thm", "ctyp"] "Proof_Display.pp_ctyp"; wenzelm@48732: toplevel_pp ["Context", "theory"] "Context.pretty_thy"; wenzelm@48732: toplevel_pp ["Context", "theory_ref"] "Context.pretty_thy o Theory.deref"; wenzelm@48732: toplevel_pp ["Context", "Proof", "context"] "Proof_Display.pp_context"; wenzelm@48732: toplevel_pp ["Ast", "ast"] "Ast.pretty_ast"; wenzelm@48732: toplevel_pp ["Path", "T"] "Path.pretty"; wenzelm@48732: toplevel_pp ["SHA1", "digest"] "Pretty.str o quote o SHA1.rep"; wenzelm@48732: toplevel_pp ["Proof", "state"] "(fn _: Proof.state => Pretty.str \"\")"; wenzelm@48732: toplevel_pp ["Toplevel", "state"] "Toplevel.pretty_abstract"; wenzelm@48732: wenzelm@48732: if ML_System.is_polyml then use "ML/install_pp_polyml.ML" else (); wenzelm@48732: wenzelm@48732: wenzelm@49862: (* the Pure theory *) wenzelm@49862: wenzelm@49862: use "pure_syn.ML"; wenzelm@49862: Toplevel.program (fn () => Thy_Info.use_thy ("Pure", Position.none)); wenzelm@49862: Context.set_thread_data NONE; wenzelm@49862: structure Pure = struct val thy = Thy_Info.get_theory "Pure" end; wenzelm@49862: wenzelm@49862: toplevel_pp ["typ"] "Proof_Display.pp_typ Pure.thy"; wenzelm@49862: wenzelm@49862: wenzelm@48879: (* ML toplevel commands *) wenzelm@48879: wenzelm@48879: fun use name = Toplevel.program (fn () => Thy_Load.use_ml (Path.explode name)); wenzelm@48879: wenzelm@48927: fun use_thys args = Toplevel.program (fn () => Thy_Info.use_thys (map (rpair Position.none) args)); wenzelm@48927: val use_thy = use_thys o single; wenzelm@48732: wenzelm@48732: val cd = File.cd o Path.explode; wenzelm@48732: wenzelm@52487: Proofterm.proofs := 0; wenzelm@48879: Multithreading.max_threads := 0; wenzelm@30639: