isabelle: src/Pure/ROOT.ML@0135a0c77b64 (annotated)

67588 f3a68e350ab6 more accessible src/Pure/ROOT.ML; wenzelm parents: 67425 diff changeset	1	(* Title: Pure/ROOT.ML
f3a68e350ab6 more accessible src/Pure/ROOT.ML; wenzelm parents: 67425 diff changeset	2	Author: Makarius
f3a68e350ab6 more accessible src/Pure/ROOT.ML; wenzelm parents: 67425 diff changeset	3
f3a68e350ab6 more accessible src/Pure/ROOT.ML; wenzelm parents: 67425 diff changeset	4	Main entry point for the Isabelle/Pure bootstrap process.
f3a68e350ab6 more accessible src/Pure/ROOT.ML; wenzelm parents: 67425 diff changeset	5
f3a68e350ab6 more accessible src/Pure/ROOT.ML; wenzelm parents: 67425 diff changeset	6	Note: When this file is open in the Prover IDE, the ML files of
f3a68e350ab6 more accessible src/Pure/ROOT.ML; wenzelm parents: 67425 diff changeset	7	Isabelle/Pure can be explored interactively. This is a separate copy of
f3a68e350ab6 more accessible src/Pure/ROOT.ML; wenzelm parents: 67425 diff changeset	8	Pure within Pure: it does not affect the running logic session.
f3a68e350ab6 more accessible src/Pure/ROOT.ML; wenzelm parents: 67425 diff changeset	9	*)
f3a68e350ab6 more accessible src/Pure/ROOT.ML; wenzelm parents: 67425 diff changeset	10
62912 745d31e63c21 section headings for ROOT.ML; wenzelm parents: 62911 diff changeset	11	chapter "Isabelle/Pure bootstrap";
62508 d0b68218ea55 discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM; wenzelm parents: 62501 diff changeset	12
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	13	ML_file "ML/ml_name_space.ML";
62883 b04e9fe29223 clarified ML bootstrap; wenzelm parents: 62880 diff changeset	14
b04e9fe29223 clarified ML bootstrap; wenzelm parents: 62880 diff changeset	15
62912 745d31e63c21 section headings for ROOT.ML; wenzelm parents: 62911 diff changeset	16	section "Bootstrap phase 0: Poly/ML setup";
62508 d0b68218ea55 discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM; wenzelm parents: 62501 diff changeset	17
67205 06c91eac25f2 clarified file name; wenzelm parents: 67138 diff changeset	18	ML_file "ML/ml_init.ML";
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	19	ML_file "ML/ml_system.ML";
62508 d0b68218ea55 discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM; wenzelm parents: 62501 diff changeset	20
62918 2fcbd4abc021 clarified modules; wenzelm parents: 62912 diff changeset	21	ML_file "General/basics.ML";
63932 6040db6b929d more tight implementation of symbol explode operation (without support for raw symbols); wenzelm parents: 63806 diff changeset	22	ML_file "General/symbol_explode.ML";
62508 d0b68218ea55 discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM; wenzelm parents: 62501 diff changeset	23
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	24	ML_file "Concurrent/multithreading.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	25	ML_file "Concurrent/unsynchronized.ML";
62918 2fcbd4abc021 clarified modules; wenzelm parents: 62912 diff changeset	26	ML_file "Concurrent/synchronized.ML";
2fcbd4abc021 clarified modules; wenzelm parents: 62912 diff changeset	27	ML_file "Concurrent/counter.ML";
62508 d0b68218ea55 discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM; wenzelm parents: 62501 diff changeset	28
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	29	ML_file "ML/ml_heap.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	30	ML_file "ML/ml_print_depth0.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	31	ML_file "ML/ml_pretty.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	32	ML_file "ML/ml_compiler0.ML";
62508 d0b68218ea55 discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM; wenzelm parents: 62501 diff changeset	33
d0b68218ea55 discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM; wenzelm parents: 62501 diff changeset	34
62912 745d31e63c21 section headings for ROOT.ML; wenzelm parents: 62911 diff changeset	35	section "Bootstrap phase 1: towards ML within position context";
62508 d0b68218ea55 discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM; wenzelm parents: 62501 diff changeset	36
62912 745d31e63c21 section headings for ROOT.ML; wenzelm parents: 62911 diff changeset	37	subsection "Library of general tools";
31432 9858f32f9569 just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources; wenzelm parents: 31335 diff changeset	38
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	39	ML_file "library.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	40	ML_file "General/print_mode.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	41	ML_file "General/alist.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	42	ML_file "General/table.ML";
43684 85388f5570c4 prefer Synchronized.var; wenzelm parents: 43593 diff changeset	43
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	44	ML_file "General/random.ML";
63806 c54a53ef1873 clarified modules; wenzelm parents: 63639 diff changeset	45	ML_file "General/value.ML";
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	46	ML_file "General/properties.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	47	ML_file "General/output.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	48	ML_file "PIDE/markup.ML";
69208 3e4edf43e254 some support for UTF-8 (similar to Isabelle/Scala version); wenzelm parents: 68839 diff changeset	49	ML_file "General/utf8.ML";
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	50	ML_file "General/scan.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	51	ML_file "General/source.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	52	ML_file "General/symbol.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	53	ML_file "General/position.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	54	ML_file "General/symbol_pos.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	55	ML_file "General/input.ML";
67425 7d4a088dbc0e clarified modules: uniform notion of formal comments; wenzelm parents: 67386 diff changeset	56	ML_file "General/comment.ML";
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	57	ML_file "General/antiquote.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	58	ML_file "ML/ml_lex.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	59	ML_file "ML/ml_compiler1.ML";
56288 bf1bdf335ea0 tuned comments; wenzelm parents: 56287 diff changeset	60
59054 61b723761dff load simple_thread.ML later, such that it benefits from redefined print_exception_trace; wenzelm parents: 59026 diff changeset	61
62912 745d31e63c21 section headings for ROOT.ML; wenzelm parents: 62911 diff changeset	62	section "Bootstrap phase 2: towards ML within Isar context";
56288 bf1bdf335ea0 tuned comments; wenzelm parents: 56287 diff changeset	63
62912 745d31e63c21 section headings for ROOT.ML; wenzelm parents: 62911 diff changeset	64	subsection "Library of general tools";
56288 bf1bdf335ea0 tuned comments; wenzelm parents: 56287 diff changeset	65
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	66	ML_file "General/integer.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	67	ML_file "General/stack.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	68	ML_file "General/queue.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	69	ML_file "General/heap.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	70	ML_file "General/same.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	71	ML_file "General/ord_list.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	72	ML_file "General/balanced_tree.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	73	ML_file "General/linear_set.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	74	ML_file "General/buffer.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	75	ML_file "General/pretty.ML";
63209 82cd1d481eb9 ML pp for Rat.rat; wenzelm parents: 63197 diff changeset	76	ML_file "General/rat.ML";
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	77	ML_file "PIDE/xml.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	78	ML_file "General/path.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	79	ML_file "General/url.ML";
73264 440546ea20e6 clarified modules; wenzelm parents: 73263 diff changeset	80	ML_file "System/bash.ML";
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	81	ML_file "General/file.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	82	ML_file "General/long_name.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	83	ML_file "General/binding.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	84	ML_file "General/seq.ML";
73383 6b104dc069de clarified signature --- augment existing structure Time; wenzelm parents: 73371 diff changeset	85	ML_file "General/time.ML";
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	86	ML_file "General/timing.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	87	ML_file "General/sha1.ML";
35628 f1456d045151 Digesting strings according to SHA-1. wenzelm parents: 35626 diff changeset	88
73558 a5d1d1e2f109 tuned signature; wenzelm parents: 73523 diff changeset	89	ML_file "PIDE/yxml.ML";
73835 5dae03d50db1 more formal ML profiling messages; wenzelm parents: 73834 diff changeset	90	ML_file "ML/ml_profiling.ML";
69448 51e696887b81 more uniform multi-language operations; wenzelm parents: 69441 diff changeset	91	ML_file "PIDE/byte_message.ML";
70907 7e3f25a0cee4 proper protocol_message for bootstrap proofs; wenzelm parents: 70893 diff changeset	92	ML_file "PIDE/protocol_message.ML";
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	93	ML_file "PIDE/document_id.ML";
74143 8d20b1cf0d5d clarified signature; wenzelm parents: 73835 diff changeset	94	ML_file "General/socket_io.ML";
44698 0385292321a0 moved XML/YXML to src/Pure/PIDE; wenzelm parents: 44549 diff changeset	95
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	96	ML_file "General/change_table.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	97	ML_file "General/graph.ML";
49560 11430dd89e35 added graph encode/decode operations; wenzelm parents: 49041 diff changeset	98
71675 55cb4271858b less redundant markup reports; wenzelm parents: 71088 diff changeset	99	ML_file "System/options.ML";
55cb4271858b less redundant markup reports; wenzelm parents: 71088 diff changeset	100
60911 858694df711b default ML context for forks, e.g. relevant for debugging and toplevel pretty-printing; wenzelm parents: 60630 diff changeset	101
62912 745d31e63c21 section headings for ROOT.ML; wenzelm parents: 62911 diff changeset	102	subsection "Fundamental structures";
60911 858694df711b default ML context for forks, e.g. relevant for debugging and toplevel pretty-printing; wenzelm parents: 60630 diff changeset	103
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	104	ML_file "name.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	105	ML_file "term.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	106	ML_file "context.ML";
71680 e20e117c3735 tuned -- prefer Config.T over Data; wenzelm parents: 71675 diff changeset	107	ML_file "config.ML";
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	108	ML_file "context_position.ML";
70364 b2bedb022a75 support for a soft-type system within the Isabelle logical framework; wenzelm parents: 69887 diff changeset	109	ML_file "soft_type_system.ML";
51947 3301612c4893 support for system options as context-sensitive config options; wenzelm parents: 51933 diff changeset	110
31432 9858f32f9569 just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources; wenzelm parents: 31335 diff changeset	111
62912 745d31e63c21 section headings for ROOT.ML; wenzelm parents: 62911 diff changeset	112	subsection "Concurrency within the ML runtime";
28120 dd4297f5b495 added Concurrent/schedule.ML; wenzelm parents: 27642 diff changeset	113
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	114	ML_file "ML/exn_properties.ML";
71086 aedd11603fb4 tuned modules; wenzelm parents: 70907 diff changeset	115	ML_file_no_debug "ML/exn_debugger.ML";
50911 ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset; wenzelm parents: 50800 diff changeset	116
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	117	ML_file "Concurrent/thread_data_virtual.ML";
71692 f8e52c0152fe clarified names; wenzelm parents: 71680 diff changeset	118	ML_file "Concurrent/isabelle_thread.ML";
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	119	ML_file "Concurrent/single_assignment.ML";
59054 61b723761dff load simple_thread.ML later, such that it benefits from redefined print_exception_trace; wenzelm parents: 59026 diff changeset	120
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	121	ML_file "Concurrent/par_exn.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	122	ML_file "Concurrent/task_queue.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	123	ML_file "Concurrent/future.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	124	ML_file "Concurrent/event_timer.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	125	ML_file "Concurrent/timeout.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	126	ML_file "Concurrent/lazy.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	127	ML_file "Concurrent/par_list.ML";
31432 9858f32f9569 just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources; wenzelm parents: 31335 diff changeset	128
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	129	ML_file "Concurrent/mailbox.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	130	ML_file "Concurrent/cache.ML";
32840 75dff0bd4d5d Concurrently cached values. wenzelm parents: 32816 diff changeset	131
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	132	ML_file "PIDE/active.ML";
70396 425c5f9bc61a support export_proofs, prune_proofs; wenzelm parents: 70364 diff changeset	133	ML_file "Thy/export.ML";
50500 c94bba7906d2 identify dialogs via official serial and maintain as result message; wenzelm parents: 50498 diff changeset	134
31432 9858f32f9569 just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources; wenzelm parents: 31335 diff changeset	135
62912 745d31e63c21 section headings for ROOT.ML; wenzelm parents: 62911 diff changeset	136	subsection "Inner syntax";
31432 9858f32f9569 just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources; wenzelm parents: 31335 diff changeset	137
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	138	ML_file "Syntax/type_annotation.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	139	ML_file "Syntax/term_position.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	140	ML_file "Syntax/lexicon.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	141	ML_file "Syntax/ast.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	142	ML_file "Syntax/syntax_ext.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	143	ML_file "Syntax/parser.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	144	ML_file "Syntax/syntax_trans.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	145	ML_file "Syntax/mixfix.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	146	ML_file "Syntax/printer.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	147	ML_file "Syntax/syntax.ML";
22679 68cd69a388e2 removed Pure/Syntax/ROOT.ML; wenzelm parents: 22592 diff changeset	148
31432 9858f32f9569 just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources; wenzelm parents: 31335 diff changeset	149
62912 745d31e63c21 section headings for ROOT.ML; wenzelm parents: 62911 diff changeset	150	subsection "Core of tactical proof system";
31432 9858f32f9569 just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources; wenzelm parents: 31335 diff changeset	151
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	152	ML_file "term_ord.ML";
74270 ad2899cdd528 clarified modules; wenzelm parents: 74143 diff changeset	153	ML_file "term_items.ML";
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	154	ML_file "term_subst.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	155	ML_file "General/completion.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	156	ML_file "General/name_space.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	157	ML_file "sorts.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	158	ML_file "type.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	159	ML_file "logic.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	160	ML_file "Syntax/simple_syntax.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	161	ML_file "net.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	162	ML_file "item_net.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	163	ML_file "envir.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	164	ML_file "consts.ML";
70784 799437173553 Term_XML.Encode/Decode.term uses Const "typargs"; wenzelm parents: 70574 diff changeset	165	ML_file "term_xml.ML";
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	166	ML_file "primitive_defs.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	167	ML_file "sign.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	168	ML_file "defs.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	169	ML_file "term_sharing.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	170	ML_file "pattern.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	171	ML_file "unify.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	172	ML_file "theory.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	173	ML_file "proofterm.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	174	ML_file "thm.ML";
74270 ad2899cdd528 clarified modules; wenzelm parents: 74143 diff changeset	175	ML_file "cterm_items.ML";
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	176	ML_file "more_pattern.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	177	ML_file "more_unify.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	178	ML_file "more_thm.ML";
70443 a21a96eda033 clarified modules; wenzelm parents: 70396 diff changeset	179
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	180	ML_file "facts.ML";
70574 503ca64329cc clarified modules; wenzelm parents: 70556 diff changeset	181	ML_file "thm_name.ML";
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	182	ML_file "global_theory.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	183	ML_file "pure_thy.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	184	ML_file "drule.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	185	ML_file "morphism.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	186	ML_file "variable.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	187	ML_file "conv.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	188	ML_file "goal_display.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	189	ML_file "tactical.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	190	ML_file "search.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	191	ML_file "tactic.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	192	ML_file "raw_simplifier.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	193	ML_file "conjunction.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	194	ML_file "assumption.ML";
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	195
31432 9858f32f9569 just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources; wenzelm parents: 31335 diff changeset	196
62912 745d31e63c21 section headings for ROOT.ML; wenzelm parents: 62911 diff changeset	197	subsection "Isar -- Intelligible Semi-Automated Reasoning";
31432 9858f32f9569 just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources; wenzelm parents: 31335 diff changeset	198
56303 4cc3f4db3447 clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler; wenzelm parents: 56288 diff changeset	199	(ML support and global execution)
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	200	ML_file "ML/ml_syntax.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	201	ML_file "ML/ml_env.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	202	ML_file "ML/ml_options.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	203	ML_file "ML/ml_print_depth.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	204	ML_file_no_debug "Isar/runtime.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	205	ML_file "PIDE/execution.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	206	ML_file "ML/ml_compiler.ML";
49041 9edfd36a0355 more informative error message from failed goal forks (violating old-style TTY protocol!); wenzelm parents: 48990 diff changeset	207
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	208	ML_file "skip_proof.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	209	ML_file "goal.ML";
49041 9edfd36a0355 more informative error message from failed goal forks (violating old-style TTY protocol!); wenzelm parents: 48990 diff changeset	210
63639 4302f86920fe clarified bootstrap; wenzelm parents: 63209 diff changeset	211	(outer syntax)
4302f86920fe clarified bootstrap; wenzelm parents: 63209 diff changeset	212	ML_file "Isar/keyword.ML";
4302f86920fe clarified bootstrap; wenzelm parents: 63209 diff changeset	213	ML_file "Isar/token.ML";
4302f86920fe clarified bootstrap; wenzelm parents: 63209 diff changeset	214	ML_file "Isar/parse.ML";
69876 b49bd228ac8a clarified modules; wenzelm parents: 69449 diff changeset	215	ML_file "Thy/document_source.ML";
63639 4302f86920fe clarified bootstrap; wenzelm parents: 63209 diff changeset	216	ML_file "Thy/thy_header.ML";
69887 b9985133805d added semantic document markers; wenzelm parents: 69876 diff changeset	217	ML_file "Thy/document_marker.ML";
63639 4302f86920fe clarified bootstrap; wenzelm parents: 63209 diff changeset	218
31432 9858f32f9569 just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources; wenzelm parents: 31335 diff changeset	219	(proof context)
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	220	ML_file "Isar/object_logic.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	221	ML_file "Isar/rule_cases.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	222	ML_file "Isar/auto_bind.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	223	ML_file "type_infer.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	224	ML_file "Syntax/local_syntax.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	225	ML_file "Isar/proof_context.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	226	ML_file "type_infer_context.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	227	ML_file "Syntax/syntax_phases.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	228	ML_file "Isar/args.ML";
31432 9858f32f9569 just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources; wenzelm parents: 31335 diff changeset	229
57926 59b2572e8e93 load local_theory.ML before attrib.ML, with subtle change of semantics due to canonical Local_Theory.map_contexts instead of private Local_Theory.map_top; wenzelm parents: 57905 diff changeset	230	(theory specifications)
63639 4302f86920fe clarified bootstrap; wenzelm parents: 63209 diff changeset	231	ML_file "Isar/local_defs.ML";
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	232	ML_file "Isar/local_theory.ML";
63090 7aa9ac5165e4 common entity definitions within a global or local theory context; wenzelm parents: 63064 diff changeset	233	ML_file "Isar/entity.ML";
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	234	ML_file "PIDE/command_span.ML";
68839 d8251a61cce8 clarified modules; wenzelm parents: 68154 diff changeset	235	ML_file "Thy/thy_element.ML";
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	236	ML_file "Thy/markdown.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	237	ML_file "Thy/latex.ML";
31432 9858f32f9569 just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources; wenzelm parents: 31335 diff changeset	238
56203 76c72f4d0667 clarified bootstrap process: switch to ML with context and antiquotations earlier; wenzelm parents: 56072 diff changeset	239	(ML with context and antiquotations)
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	240	ML_file "ML/ml_context.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	241	ML_file "ML/ml_antiquotation.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	242	ML_file "ML/ml_compiler2.ML";
73613 c1d8cd6d1a49 early definition of ML antiquotations; wenzelm parents: 73587 diff changeset	243	ML_file "ML/ml_antiquotations1.ML";
56434 7acc933bd7cc clarified ML bootstrap; wenzelm parents: 56303 diff changeset	244
56288 bf1bdf335ea0 tuned comments; wenzelm parents: 56287 diff changeset	245
62912 745d31e63c21 section headings for ROOT.ML; wenzelm parents: 62911 diff changeset	246	section "Bootstrap phase 3: towards theory Pure and final ML toplevel setup";
56203 76c72f4d0667 clarified bootstrap process: switch to ML with context and antiquotations earlier; wenzelm parents: 56072 diff changeset	247
31432 9858f32f9569 just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources; wenzelm parents: 31335 diff changeset	248	(basic proof engine)
70521 9ddd66d53130 added SUBPROOFS / "subproofs" method combinator, for more compact proofterms; wenzelm parents: 70520 diff changeset	249	ML_file "par_tactical.ML";
70520 11d8517d9384 clarified modules; wenzelm parents: 70447 diff changeset	250	ML_file "context_tactic.ML";
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	251	ML_file "Isar/proof_display.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	252	ML_file "Isar/attrib.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	253	ML_file "Isar/context_rules.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	254	ML_file "Isar/method.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	255	ML_file "Isar/proof.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	256	ML_file "Isar/element.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	257	ML_file "Isar/obtain.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	258	ML_file "Isar/subgoal.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	259	ML_file "Isar/calculation.ML";
31432 9858f32f9569 just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources; wenzelm parents: 31335 diff changeset	260
9858f32f9569 just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources; wenzelm parents: 31335 diff changeset	261	(local theories and targets)
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	262	ML_file "Isar/locale.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	263	ML_file "Isar/generic_target.ML";
72536 589645894305 bundle mixins for locale and class specifications haftmann parents: 72453 diff changeset	264	ML_file "Isar/bundle.ML";
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	265	ML_file "Isar/overloading.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	266	ML_file "axclass.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	267	ML_file "Isar/class.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	268	ML_file "Isar/named_target.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	269	ML_file "Isar/expression.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	270	ML_file "Isar/interpretation.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	271	ML_file "Isar/class_declaration.ML";
72453 e4dde7beab39 dedicated module for toplevel target handling haftmann parents: 72052 diff changeset	272	ML_file "Isar/target_context.ML";
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	273	ML_file "Isar/experiment.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	274	ML_file "simplifier.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	275	ML_file "Tools/plugin.ML";
31432 9858f32f9569 just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources; wenzelm parents: 31335 diff changeset	276
9858f32f9569 just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources; wenzelm parents: 31335 diff changeset	277	(executable theory content)
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	278	ML_file "Isar/code.ML";
31432 9858f32f9569 just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources; wenzelm parents: 31335 diff changeset	279
9858f32f9569 just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources; wenzelm parents: 31335 diff changeset	280	(specifications)
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	281	ML_file "Isar/spec_rules.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	282	ML_file "Isar/specification.ML";
63064 2f18172214c8 support 'assumes' in specifications, e.g. 'definition', 'inductive'; wenzelm parents: 62943 diff changeset	283	ML_file "Isar/parse_spec.ML";
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	284	ML_file "Isar/typedecl.ML";
31432 9858f32f9569 just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources; wenzelm parents: 31335 diff changeset	285
9858f32f9569 just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources; wenzelm parents: 31335 diff changeset	286	(toplevel transactions)
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	287	ML_file "Isar/proof_node.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	288	ML_file "Isar/toplevel.ML";
31432 9858f32f9569 just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources; wenzelm parents: 31335 diff changeset	289
56206 7adec2a527f5 clarified module arrangement; wenzelm parents: 56205 diff changeset	290	(proof term operations)
71088 4b45d592ce29 clarified modules; wenzelm parents: 71086 diff changeset	291	ML_file "Proof/proof_rewrite_rules.ML";
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	292	ML_file "Proof/proof_syntax.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	293	ML_file "Proof/proof_checker.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	294	ML_file "Proof/extraction.ML";
56206 7adec2a527f5 clarified module arrangement; wenzelm parents: 56205 diff changeset	295
62584 6cd36a0d2a28 clarified files; wenzelm parents: 62573 diff changeset	296	(Isabelle system)
73225 3ab0cedaccad clarified modules: allow early definition of protocol commands; wenzelm parents: 73136 diff changeset	297	ML_file "PIDE/protocol_command.ML";
73226 4c8edf348c4e clarified modules: allow early invocation of Scala functions; wenzelm parents: 73225 diff changeset	298	ML_file "System/scala.ML";
73275 f0db1e4c89bc clarified signature, following Isabelle/Scala; wenzelm parents: 73265 diff changeset	299	ML_file "System/process_result.ML";
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	300	ML_file "System/isabelle_system.ML";
62584 6cd36a0d2a28 clarified files; wenzelm parents: 62573 diff changeset	301
62845 31177a9c3025 clarified modules; wenzelm parents: 62825 diff changeset	302
38271 36187e8443dd Isar_Document command input via native Isabelle_Process commands, using YXML and XML_Data representation; wenzelm parents: 38266 diff changeset	303	(theory documents)
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	304	ML_file "Thy/term_style.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	305	ML_file "Isar/outer_syntax.ML";
73613 c1d8cd6d1a49 early definition of ML antiquotations; wenzelm parents: 73587 diff changeset	306	ML_file "ML/ml_antiquotations2.ML";
73587 d1767bcb79ec clarified conditional ML; wenzelm parents: 73558 diff changeset	307	ML_file "ML/ml_pid.ML";
67386 998e01d6f8fd clarified modules; wenzelm parents: 67275 diff changeset	308	ML_file "Thy/document_antiquotation.ML";
73761 ef1a18e20ace clarified modules; wenzelm parents: 73613 diff changeset	309	ML_file "Thy/document_output.ML";
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	310	ML_file "Thy/document_antiquotations.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	311	ML_file "General/graph_display.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	312	ML_file "pure_syn.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	313	ML_file "PIDE/command.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	314	ML_file "PIDE/query_operation.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	315	ML_file "PIDE/resources.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	316	ML_file "Thy/thy_info.ML";
70893 ce1e27dcc9f4 clarified files; wenzelm parents: 70784 diff changeset	317	ML_file "thm_deps.ML";
68154 42d63ea39161 some export of foundational theory content; wenzelm parents: 68090 diff changeset	318	ML_file "Thy/export_theory.ML";
67215 03d0c958d65a PIDE markup for session ROOT files; wenzelm parents: 67205 diff changeset	319	ML_file "Thy/sessions.ML";
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	320	ML_file "PIDE/session.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	321	ML_file "PIDE/document.ML";
31432 9858f32f9569 just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources; wenzelm parents: 31335 diff changeset	322
9858f32f9569 just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources; wenzelm parents: 31335 diff changeset	323	(theory and proof operations)
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	324	ML_file "Isar/isar_cmd.ML";
31432 9858f32f9569 just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources; wenzelm parents: 31335 diff changeset	325
9858f32f9569 just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources; wenzelm parents: 31335 diff changeset	326
62912 745d31e63c21 section headings for ROOT.ML; wenzelm parents: 62911 diff changeset	327	subsection "Isabelle/Isar system";
31432 9858f32f9569 just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources; wenzelm parents: 31335 diff changeset	328
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	329	ML_file "System/command_line.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	330	ML_file "System/message_channel.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	331	ML_file "System/isabelle_process.ML";
71888 feb37a43ace6 clarified signature; wenzelm parents: 71881 diff changeset	332	ML_file "System/scala_compiler.ML";
72763 3cc73d00553c added document antiquotation @{tool}; wenzelm parents: 72760 diff changeset	333	ML_file "System/isabelle_tool.ML";
67275 5e427586cb57 check bibtex database on ML side -- for semantic PIDE editing; wenzelm parents: 67274 diff changeset	334	ML_file "Thy/bibtex.ML";
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	335	ML_file "PIDE/protocol.ML";
62930 51ac6bc389e8 shared output primitives of physical/virtual Pure; wenzelm parents: 62923 diff changeset	336	ML_file "General/output_primitives_virtual.ML";
30173 eabece26b89b moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands); wenzelm parents: 29269 diff changeset	337
31432 9858f32f9569 just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources; wenzelm parents: 31335 diff changeset	338
62912 745d31e63c21 section headings for ROOT.ML; wenzelm parents: 62911 diff changeset	339	subsection "Miscellaneous tools and packages for Pure Isabelle";
31432 9858f32f9569 just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources; wenzelm parents: 31335 diff changeset	340
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	341	ML_file "ML/ml_pp.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	342	ML_file "ML/ml_thms.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	343	ML_file "ML/ml_file.ML";
62849 caaa2fc4040d clarified bootstrap -- avoid 'ML_file' in Pure.thy for uniformity; wenzelm parents: 62848 diff changeset	344
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	345	ML_file "Tools/build.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	346	ML_file "Tools/named_thms.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	347	ML_file "Tools/print_operation.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	348	ML_file "Tools/rail.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	349	ML_file "Tools/rule_insts.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	350	ML_file "Tools/thy_deps.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	351	ML_file "Tools/class_deps.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	352	ML_file "Tools/find_theorems.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	353	ML_file "Tools/find_consts.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	354	ML_file "Tools/simplifier_trace.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	355	ML_file_no_debug "Tools/debugger.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	356	ML_file "Tools/named_theorems.ML";
72760 042180540068 clarified protocol: Doc.check at run-time via Scala function; wenzelm parents: 72696 diff changeset	357	ML_file "Tools/doc.ML";
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	358	ML_file "Tools/jedit.ML";
69209 3f4210c13356 support for GHC: string literals; wenzelm parents: 69208 diff changeset	359	ML_file "Tools/ghc.ML";
69383 747f8b052e59 clarified modules; wenzelm parents: 69381 diff changeset	360	ML_file "Tools/generated_files.ML"

author	wenzelm
	Fri, 24 Sep 2021 22:23:26 +0200
changeset 74362	0135a0c77b64
parent 74270	ad2899cdd528
child 74559	9189d949abb9
permissions	-rw-r--r--