isabelle: src/Pure/ROOT.ML@3956e8b6a9c9 (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";
77847 3bb6468d202e more operations, following Isabelle/ML conventions; wenzelm parents: 77846 diff changeset	22	ML_file "General/string.ML";
77846 5ba68d3bd741 more operations, following Isabelle/ML conventions; wenzelm parents: 77842 diff changeset	23	ML_file "General/vector.ML";
77887 dae8b7a9a89a more operations, following Isabelle/ML conventions; wenzelm parents: 77847 diff changeset	24	ML_file "General/array.ML";
63932 6040db6b929d more tight implementation of symbol explode operation (without support for raw symbols); wenzelm parents: 63806 diff changeset	25	ML_file "General/symbol_explode.ML";
62508 d0b68218ea55 discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM; wenzelm parents: 62501 diff changeset	26
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	27	ML_file "Concurrent/multithreading.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	28	ML_file "Concurrent/unsynchronized.ML";
62918 2fcbd4abc021 clarified modules; wenzelm parents: 62912 diff changeset	29	ML_file "Concurrent/synchronized.ML";
2fcbd4abc021 clarified modules; wenzelm parents: 62912 diff changeset	30	ML_file "Concurrent/counter.ML";
78711 3a3a70d4d422 clarified order of modules: early access to interrupt management of Isabelle_Threads; wenzelm parents: 78677 diff changeset	31	ML_file "Concurrent/single_assignment.ML";
3a3a70d4d422 clarified order of modules: early access to interrupt management of Isabelle_Threads; wenzelm parents: 78677 diff changeset	32	ML_file "Concurrent/isabelle_thread.ML";
62508 d0b68218ea55 discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM; wenzelm parents: 62501 diff changeset	33
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	34	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	35	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	36	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	37	ML_file "ML/ml_compiler0.ML";
62508 d0b68218ea55 discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM; wenzelm parents: 62501 diff changeset	38
d0b68218ea55 discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM; wenzelm parents: 62501 diff changeset	39
62912 745d31e63c21 section headings for ROOT.ML; wenzelm parents: 62911 diff changeset	40	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	41
62912 745d31e63c21 section headings for ROOT.ML; wenzelm parents: 62911 diff changeset	42	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	43
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	44	ML_file "library.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	45	ML_file "General/print_mode.ML";
77768 65008644d394 tuned: prefer "build" combinator; wenzelm parents: 77722 diff changeset	46	ML_file "General/integer.ML";
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	47	ML_file "General/alist.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	48	ML_file "General/table.ML";
79074 7f24c5be57bd compact representation of sets of integers; wenzelm parents: 79049 diff changeset	49	ML_file "General/bitset.ML";
77722 8faf28a80a7f efficient representation of sets: more compact than Table.set; wenzelm parents: 77666 diff changeset	50	ML_file "General/set.ML";
43684 85388f5570c4 prefer Synchronized.var; wenzelm parents: 43593 diff changeset	51
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	52	ML_file "General/random.ML";
63806 c54a53ef1873 clarified modules; wenzelm parents: 63639 diff changeset	53	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	54	ML_file "General/properties.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	55	ML_file "General/output.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	56	ML_file "PIDE/markup.ML";
69208 3e4edf43e254 some support for UTF-8 (similar to Isabelle/Scala version); wenzelm parents: 68839 diff changeset	57	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	58	ML_file "General/scan.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	59	ML_file "General/source.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	60	ML_file "General/symbol.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	61	ML_file "General/position.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	62	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	63	ML_file "General/input.ML";
67425 7d4a088dbc0e clarified modules: uniform notion of formal comments; wenzelm parents: 67386 diff changeset	64	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	65	ML_file "General/antiquote.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	66	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	67	ML_file "ML/ml_compiler1.ML";
56288 bf1bdf335ea0 tuned comments; wenzelm parents: 56287 diff changeset	68
59054 61b723761dff load simple_thread.ML later, such that it benefits from redefined print_exception_trace; wenzelm parents: 59026 diff changeset	69
62912 745d31e63c21 section headings for ROOT.ML; wenzelm parents: 62911 diff changeset	70	section "Bootstrap phase 2: towards ML within Isar context";
56288 bf1bdf335ea0 tuned comments; wenzelm parents: 56287 diff changeset	71
62912 745d31e63c21 section headings for ROOT.ML; wenzelm parents: 62911 diff changeset	72	subsection "Library of general tools";
56288 bf1bdf335ea0 tuned comments; wenzelm parents: 56287 diff changeset	73
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	74	ML_file "General/stack.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	75	ML_file "General/queue.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	76	ML_file "General/heap.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	77	ML_file "General/same.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	78	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	79	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	80	ML_file "General/linear_set.ML";
77842 0eb54e7004eb compact representation of long name "chunks", with bitmask to suppress elements (i.e. "accesses" in name space terminology); wenzelm parents: 77768 diff changeset	81	ML_file "General/change_table.ML";
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	82	ML_file "General/buffer.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	83	ML_file "General/pretty.ML";
63209 82cd1d481eb9 ML pp for Rat.rat; wenzelm parents: 63197 diff changeset	84	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	85	ML_file "PIDE/xml.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	86	ML_file "General/path.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	87	ML_file "General/url.ML";
73264 440546ea20e6 clarified modules; wenzelm parents: 73263 diff changeset	88	ML_file "System/bash.ML";
75615 4494cd69f97f clarified modules; wenzelm parents: 75567 diff changeset	89	ML_file "General/file_stream.ML";
4494cd69f97f clarified modules; wenzelm parents: 75567 diff changeset	90	ML_file "General/bytes.ML";
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	91	ML_file "General/file.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	92	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	93	ML_file "General/binding.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	94	ML_file "General/seq.ML";
73383 6b104dc069de clarified signature --- augment existing structure Time; wenzelm parents: 73371 diff changeset	95	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	96	ML_file "General/timing.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	97	ML_file "General/sha1.ML";
35628 f1456d045151 Digesting strings according to SHA-1. wenzelm parents: 35626 diff changeset	98
73558 a5d1d1e2f109 tuned signature; wenzelm parents: 73523 diff changeset	99	ML_file "PIDE/yxml.ML";
73835 5dae03d50db1 more formal ML profiling messages; wenzelm parents: 73834 diff changeset	100	ML_file "ML/ml_profiling.ML";
69448 51e696887b81 more uniform multi-language operations; wenzelm parents: 69441 diff changeset	101	ML_file "PIDE/byte_message.ML";
70907 7e3f25a0cee4 proper protocol_message for bootstrap proofs; wenzelm parents: 70893 diff changeset	102	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	103	ML_file "PIDE/document_id.ML";
44698 0385292321a0 moved XML/YXML to src/Pure/PIDE; wenzelm parents: 44549 diff changeset	104
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	105	ML_file "General/graph.ML";
49560 11430dd89e35 added graph encode/decode operations; wenzelm parents: 49041 diff changeset	106
71675 55cb4271858b less redundant markup reports; wenzelm parents: 71088 diff changeset	107	ML_file "System/options.ML";
55cb4271858b less redundant markup reports; wenzelm parents: 71088 diff changeset	108
60911 858694df711b default ML context for forks, e.g. relevant for debugging and toplevel pretty-printing; wenzelm parents: 60630 diff changeset	109
62912 745d31e63c21 section headings for ROOT.ML; wenzelm parents: 62911 diff changeset	110	subsection "Fundamental structures";
60911 858694df711b default ML context for forks, e.g. relevant for debugging and toplevel pretty-printing; wenzelm parents: 60630 diff changeset	111
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	112	ML_file "name.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	113	ML_file "term.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	114	ML_file "context.ML";
71680 e20e117c3735 tuned -- prefer Config.T over Data; wenzelm parents: 71675 diff changeset	115	ML_file "config.ML";
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	116	ML_file "context_position.ML";
70364 b2bedb022a75 support for a soft-type system within the Isabelle logical framework; wenzelm parents: 69887 diff changeset	117	ML_file "soft_type_system.ML";
51947 3301612c4893 support for system options as context-sensitive config options; wenzelm parents: 51933 diff changeset	118
31432 9858f32f9569 just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources; wenzelm parents: 31335 diff changeset	119
62912 745d31e63c21 section headings for ROOT.ML; wenzelm parents: 62911 diff changeset	120	subsection "Concurrency within the ML runtime";
28120 dd4297f5b495 added Concurrent/schedule.ML; wenzelm parents: 27642 diff changeset	121
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	122	ML_file "ML/exn_properties.ML";
71086 aedd11603fb4 tuned modules; wenzelm parents: 70907 diff changeset	123	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	124
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	125	ML_file "Concurrent/thread_data_virtual.ML";
59054 61b723761dff load simple_thread.ML later, such that it benefits from redefined print_exception_trace; wenzelm parents: 59026 diff changeset	126
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	127	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	128	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	129	ML_file "Concurrent/future.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	130	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	131	ML_file "Concurrent/timeout.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	132	ML_file "Concurrent/lazy.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	133	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	134
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	135	ML_file "Concurrent/mailbox.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	136	ML_file "Concurrent/cache.ML";
32840 75dff0bd4d5d Concurrently cached values. wenzelm parents: 32816 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 "PIDE/active.ML";
79502 c7a98469c0e7 clarified directories; wenzelm parents: 79329 diff changeset	139	ML_file "Build/export.ML";
50500 c94bba7906d2 identify dialogs via official serial and maintain as result message; wenzelm parents: 50498 diff changeset	140
31432 9858f32f9569 just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources; wenzelm parents: 31335 diff changeset	141
62912 745d31e63c21 section headings for ROOT.ML; wenzelm parents: 62911 diff changeset	142	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	143
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	144	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	145	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	146	ML_file "Syntax/lexicon.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	147	ML_file "Syntax/ast.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	148	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	149	ML_file "Syntax/parser.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	150	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	151	ML_file "Syntax/mixfix.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	152	ML_file "Syntax/printer.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	153	ML_file "Syntax/syntax.ML";
22679 68cd69a388e2 removed Pure/Syntax/ROOT.ML; wenzelm parents: 22592 diff changeset	154
31432 9858f32f9569 just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources; wenzelm parents: 31335 diff changeset	155
62912 745d31e63c21 section headings for ROOT.ML; wenzelm parents: 62911 diff changeset	156	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	157
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	158	ML_file "term_ord.ML";
74270 ad2899cdd528 clarified modules; wenzelm parents: 74143 diff changeset	159	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	160	ML_file "term_subst.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	161	ML_file "General/completion.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	162	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	163	ML_file "sorts.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	164	ML_file "type.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	165	ML_file "logic.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	166	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	167	ML_file "net.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	168	ML_file "item_net.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	169	ML_file "envir.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	170	ML_file "consts.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	171	ML_file "primitive_defs.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	172	ML_file "sign.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	173	ML_file "defs.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	174	ML_file "pattern.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	175	ML_file "unify.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	176	ML_file "theory.ML";
79111 8fb4013f2ac2 clarified bootstrap --- modules related to proofterm.ML; wenzelm parents: 79098 diff changeset	177	ML_file "term_sharing.ML";
8fb4013f2ac2 clarified bootstrap --- modules related to proofterm.ML; wenzelm parents: 79098 diff changeset	178	ML_file "term_xml.ML";
79329 992c494bda25 proper thm_name for stored zproof; wenzelm parents: 79111 diff changeset	179	ML_file "thm_name.ML";
79111 8fb4013f2ac2 clarified bootstrap --- modules related to proofterm.ML; wenzelm parents: 79098 diff changeset	180	ML_file "zterm.ML";
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	181	ML_file "proofterm.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	182	ML_file "thm.ML";
74270 ad2899cdd528 clarified modules; wenzelm parents: 74143 diff changeset	183	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	184	ML_file "more_pattern.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	185	ML_file "more_unify.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	186	ML_file "more_thm.ML";
70443 a21a96eda033 clarified modules; wenzelm parents: 70396 diff changeset	187
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	188	ML_file "facts.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	189	ML_file "global_theory.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	190	ML_file "pure_thy.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	191	ML_file "drule.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	192	ML_file "morphism.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	193	ML_file "variable.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	194	ML_file "conv.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	195	ML_file "goal_display.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	196	ML_file "tactical.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	197	ML_file "search.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	198	ML_file "tactic.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	199	ML_file "raw_simplifier.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	200	ML_file "conjunction.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	201	ML_file "assumption.ML";
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	202
31432 9858f32f9569 just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources; wenzelm parents: 31335 diff changeset	203
62912 745d31e63c21 section headings for ROOT.ML; wenzelm parents: 62911 diff changeset	204	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	205
56303 4cc3f4db3447 clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler; wenzelm parents: 56288 diff changeset	206	(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	207	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	208	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	209	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	210	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	211	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	212	ML_file "PIDE/execution.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	213	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	214
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	215	ML_file "skip_proof.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	216	ML_file "goal.ML";
49041 9edfd36a0355 more informative error message from failed goal forks (violating old-style TTY protocol!); wenzelm parents: 48990 diff changeset	217
63639 4302f86920fe clarified bootstrap; wenzelm parents: 63209 diff changeset	218	(outer syntax)
4302f86920fe clarified bootstrap; wenzelm parents: 63209 diff changeset	219	ML_file "Isar/keyword.ML";
4302f86920fe clarified bootstrap; wenzelm parents: 63209 diff changeset	220	ML_file "Isar/token.ML";
4302f86920fe clarified bootstrap; wenzelm parents: 63209 diff changeset	221	ML_file "Isar/parse.ML";
69876 b49bd228ac8a clarified modules; wenzelm parents: 69449 diff changeset	222	ML_file "Thy/document_source.ML";
63639 4302f86920fe clarified bootstrap; wenzelm parents: 63209 diff changeset	223	ML_file "Thy/thy_header.ML";
69887 b9985133805d added semantic document markers; wenzelm parents: 69876 diff changeset	224	ML_file "Thy/document_marker.ML";
63639 4302f86920fe clarified bootstrap; wenzelm parents: 63209 diff changeset	225
31432 9858f32f9569 just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources; wenzelm parents: 31335 diff changeset	226	(proof context)
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	227	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	228	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	229	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	230	ML_file "type_infer.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	231	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	232	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	233	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	234	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	235	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	236
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	237	(theory specifications)
63639 4302f86920fe clarified bootstrap; wenzelm parents: 63209 diff changeset	238	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	239	ML_file "Isar/local_theory.ML";
63090 7aa9ac5165e4 common entity definitions within a global or local theory context; wenzelm parents: 63064 diff changeset	240	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	241	ML_file "PIDE/command_span.ML";
68839 d8251a61cce8 clarified modules; wenzelm parents: 68154 diff changeset	242	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	243	ML_file "Thy/markdown.ML";
79503 c67b47cd41dc clarified directories; wenzelm parents: 79502 diff changeset	244	ML_file "General/latex.ML";
31432 9858f32f9569 just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources; wenzelm parents: 31335 diff changeset	245
56203 76c72f4d0667 clarified bootstrap process: switch to ML with context and antiquotations earlier; wenzelm parents: 56072 diff changeset	246	(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	247	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	248	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	249	ML_file "ML/ml_compiler2.ML";
74559 9189d949abb9 clarified modules; wenzelm parents: 74270 diff changeset	250	ML_file "ML/ml_antiquotations.ML";
56434 7acc933bd7cc clarified ML bootstrap; wenzelm parents: 56303 diff changeset	251
56288 bf1bdf335ea0 tuned comments; wenzelm parents: 56287 diff changeset	252
62912 745d31e63c21 section headings for ROOT.ML; wenzelm parents: 62911 diff changeset	253	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	254
31432 9858f32f9569 just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources; wenzelm parents: 31335 diff changeset	255	(basic proof engine)
70521 9ddd66d53130 added SUBPROOFS / "subproofs" method combinator, for more compact proofterms; wenzelm parents: 70520 diff changeset	256	ML_file "par_tactical.ML";
70520 11d8517d9384 clarified modules; wenzelm parents: 70447 diff changeset	257	ML_file "context_tactic.ML";
76065 6dc5968b9a86 clarified modules; wenzelm parents: 75985 diff changeset	258	ML_file "Isar/attrib.ML";
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	259	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	260	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	261	ML_file "Isar/method.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	262	ML_file "Isar/proof.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	263	ML_file "Isar/element.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	264	ML_file "Isar/obtain.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	265	ML_file "Isar/subgoal.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	266	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	267
9858f32f9569 just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources; wenzelm parents: 31335 diff changeset	268	(local theories and targets)
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	269	ML_file "Isar/locale.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	270	ML_file "Isar/generic_target.ML";
72536 589645894305 bundle mixins for locale and class specifications haftmann parents: 72453 diff changeset	271	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	272	ML_file "Isar/overloading.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	273	ML_file "axclass.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	274	ML_file "Isar/class.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	275	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	276	ML_file "Isar/expression.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	277	ML_file "Isar/interpretation.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	278	ML_file "Isar/class_declaration.ML";
72453 e4dde7beab39 dedicated module for toplevel target handling haftmann parents: 72052 diff changeset	279	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	280	ML_file "Isar/experiment.ML";
78812 d769a183d51d simprocs may be distinguished via 'identifier': only works for ML antiquotation (see also 13252110a6fe); wenzelm parents: 78780 diff changeset	281	ML_file "ML/ml_thms.ML";
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	282	ML_file "simplifier.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	283	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	284
9858f32f9569 just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources; wenzelm parents: 31335 diff changeset	285	(executable theory content)
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	286	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	287
9858f32f9569 just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources; wenzelm parents: 31335 diff changeset	288	(specifications)
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	289	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	290	ML_file "Isar/specification.ML";
63064 2f18172214c8 support 'assumes' in specifications, e.g. 'definition', 'inductive'; wenzelm parents: 62943 diff changeset	291	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	292	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	293
9858f32f9569 just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources; wenzelm parents: 31335 diff changeset	294	(toplevel transactions)
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	295	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	296	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	297
56206 7adec2a527f5 clarified module arrangement; wenzelm parents: 56205 diff changeset	298	(proof term operations)
71088 4b45d592ce29 clarified modules; wenzelm parents: 71086 diff changeset	299	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	300	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	301	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	302	ML_file "Proof/extraction.ML";
56206 7adec2a527f5 clarified module arrangement; wenzelm parents: 56205 diff changeset	303
62584 6cd36a0d2a28 clarified files; wenzelm parents: 62573 diff changeset	304	(Isabelle system)
79049 10b6add456d0 support for Unix-domain sockets, using java.nio.channels.ServerSocketChannel; wenzelm parents: 79013 diff changeset	305	ML_file "General/socket_io.ML";
73225 3ab0cedaccad clarified modules: allow early definition of protocol commands; wenzelm parents: 73136 diff changeset	306	ML_file "PIDE/protocol_command.ML";
75682 b6f3db86f9c7 support for Java language; wenzelm parents: 75660 diff changeset	307	ML_file "System/java.ML";
73226 4c8edf348c4e clarified modules: allow early invocation of Scala functions; wenzelm parents: 73225 diff changeset	308	ML_file "System/scala.ML";
73275 f0db1e4c89bc clarified signature, following Isabelle/Scala; wenzelm parents: 73265 diff changeset	309	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	310	ML_file "System/isabelle_system.ML";
62584 6cd36a0d2a28 clarified files; wenzelm parents: 62573 diff changeset	311
62845 31177a9c3025 clarified modules; wenzelm parents: 62825 diff changeset	312
38271 36187e8443dd Isar_Document command input via native Isabelle_Process commands, using YXML and XML_Data representation; wenzelm parents: 38266 diff changeset	313	(theory documents)
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	314	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	315	ML_file "Isar/outer_syntax.ML";
67386 998e01d6f8fd clarified modules; wenzelm parents: 67275 diff changeset	316	ML_file "Thy/document_antiquotation.ML";
73761 ef1a18e20ace clarified modules; wenzelm parents: 73613 diff changeset	317	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	318	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	319	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	320	ML_file "pure_syn.ML";
79502 c7a98469c0e7 clarified directories; wenzelm parents: 79329 diff changeset	321	ML_file "Build/resources.ML";
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	322	ML_file "PIDE/command.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	323	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	324	ML_file "Thy/thy_info.ML";
70893 ce1e27dcc9f4 clarified files; wenzelm parents: 70784 diff changeset	325	ML_file "thm_deps.ML";
79502 c7a98469c0e7 clarified directories; wenzelm parents: 79329 diff changeset	326	ML_file "Build/export_theory.ML";
c7a98469c0e7 clarified directories; wenzelm parents: 79329 diff changeset	327	ML_file "Build/sessions.ML";
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	328	ML_file "PIDE/session.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	329	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	330
74600 c6610137a092 tuned modules; wenzelm parents: 74593 diff changeset	331	(ML add-ons)
c6610137a092 tuned modules; wenzelm parents: 74593 diff changeset	332	ML_file "ML/ml_pp.ML";
c6610137a092 tuned modules; wenzelm parents: 74593 diff changeset	333	ML_file "ML/ml_instantiate.ML";
c6610137a092 tuned modules; wenzelm parents: 74593 diff changeset	334	ML_file "ML/ml_file.ML";
c6610137a092 tuned modules; wenzelm parents: 74593 diff changeset	335	ML_file "ML/ml_pid.ML";
c6610137a092 tuned modules; wenzelm parents: 74593 diff changeset	336
31432 9858f32f9569 just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources; wenzelm parents: 31335 diff changeset	337	(theory and proof operations)
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	338	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	339
9858f32f9569 just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources; wenzelm parents: 31335 diff changeset	340
62912 745d31e63c21 section headings for ROOT.ML; wenzelm parents: 62911 diff changeset	341	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	342
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	343	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	344	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	345	ML_file "System/isabelle_process.ML";
71888 feb37a43ace6 clarified signature; wenzelm parents: 71881 diff changeset	346	ML_file "System/scala_compiler.ML";
72763 3cc73d00553c added document antiquotation @{tool}; wenzelm parents: 72760 diff changeset	347	ML_file "System/isabelle_tool.ML";
79504 958d7b118c7b clarified bootstrap; wenzelm parents: 79503 diff changeset	348	ML_file "Build/build.ML";
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	349	ML_file "PIDE/protocol.ML";
62930 51ac6bc389e8 shared output primitives of physical/virtual Pure; wenzelm parents: 62923 diff changeset	350	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	351
31432 9858f32f9569 just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources; wenzelm parents: 31335 diff changeset	352
62912 745d31e63c21 section headings for ROOT.ML; wenzelm parents: 62911 diff changeset	353	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	354
75621 aeb412065742 prefer antiquotations; wenzelm parents: 75620 diff changeset	355	ML_file "General/base64.ML";
79504 958d7b118c7b clarified bootstrap; wenzelm parents: 79503 diff changeset	356	ML_file "General/bibtex.ML";
75621 aeb412065742 prefer antiquotations; wenzelm parents: 75620 diff changeset	357	ML_file "General/xz.ML";
76351 2cee31cd92f0 generic support for XZ and Zstd compression in Isabelle/Scala; wenzelm parents: 76347 diff changeset	358	ML_file "General/zstd.ML";
76514 2615cf68f6f4 ML support for the Prism.js syntax highlighter -- via Isabelle/Scala; wenzelm parents: 76351 diff changeset	359	ML_file "Tools/prismjs.ML";
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	360	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	361	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	362	ML_file "Tools/rail.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	363	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	364	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	365	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	366	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	367	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	368	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	369	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	370	ML_file "Tools/named_theorems.ML";
72760 042180540068 clarified protocol: Doc.check at run-time via Scala function; wenzelm parents: 72696 diff changeset	371	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	372	ML_file "Tools/jedit.ML";
69209 3f4210c13356 support for GHC: string literals; wenzelm parents: 69208 diff changeset	373	ML_file "Tools/ghc.ML";
75660 45d3497c0baa support for Isabelle/Scala/Java modules in Isabelle/ML; wenzelm parents: 75621 diff changeset	374	ML_file "Tools/generated_files.ML";

author	wenzelm
	Fri, 24 May 2024 16:15:27 +0200
changeset 80188	3956e8b6a9c9
parent 80131	68fc6839679e
child 80395	46135b44b1a3
permissions	-rw-r--r--