isabelle: src/Pure/ROOT.ML@7ef1c5dada12 (annotated)

62912 745d31e63c21 section headings for ROOT.ML; wenzelm parents: 62911 diff changeset	1	chapter "Isabelle/Pure bootstrap";
62508 d0b68218ea55 discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM; wenzelm parents: 62501 diff changeset	2
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	3	ML_file "ML/ml_name_space.ML";
62883 b04e9fe29223 clarified ML bootstrap; wenzelm parents: 62880 diff changeset	4
b04e9fe29223 clarified ML bootstrap; wenzelm parents: 62880 diff changeset	5
62912 745d31e63c21 section headings for ROOT.ML; wenzelm parents: 62911 diff changeset	6	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	7
67205 06c91eac25f2 clarified file name; wenzelm parents: 67138 diff changeset	8	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	9	ML_file "ML/ml_system.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	10	ML_file "System/distribution.ML";
62508 d0b68218ea55 discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM; wenzelm parents: 62501 diff changeset	11
62918 2fcbd4abc021 clarified modules; wenzelm parents: 62912 diff changeset	12	ML_file "General/basics.ML";
63932 6040db6b929d more tight implementation of symbol explode operation (without support for raw symbols); wenzelm parents: 63806 diff changeset	13	ML_file "General/symbol_explode.ML";
62508 d0b68218ea55 discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM; wenzelm parents: 62501 diff changeset	14
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	15	ML_file "Concurrent/multithreading.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	16	ML_file "Concurrent/unsynchronized.ML";
62918 2fcbd4abc021 clarified modules; wenzelm parents: 62912 diff changeset	17	ML_file "Concurrent/synchronized.ML";
2fcbd4abc021 clarified modules; wenzelm parents: 62912 diff changeset	18	ML_file "Concurrent/counter.ML";
62508 d0b68218ea55 discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM; wenzelm parents: 62501 diff changeset	19
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	20	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	21	ML_file "ML/ml_profiling.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	22	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	23	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	24	ML_file "ML/ml_compiler0.ML";
62508 d0b68218ea55 discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM; wenzelm parents: 62501 diff changeset	25
d0b68218ea55 discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM; wenzelm parents: 62501 diff changeset	26
62912 745d31e63c21 section headings for ROOT.ML; wenzelm parents: 62911 diff changeset	27	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	28
62912 745d31e63c21 section headings for ROOT.ML; wenzelm parents: 62911 diff changeset	29	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	30
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	31	ML_file "library.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	32	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	33	ML_file "General/alist.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	34	ML_file "General/table.ML";
43684 85388f5570c4 prefer Synchronized.var; wenzelm parents: 43593 diff changeset	35
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	36	ML_file "General/random.ML";
63806 c54a53ef1873 clarified modules; wenzelm parents: 63639 diff changeset	37	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	38	ML_file "General/properties.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	39	ML_file "General/output.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	40	ML_file "PIDE/markup.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	41	ML_file "General/scan.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	42	ML_file "General/source.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	43	ML_file "General/symbol.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	44	ML_file "General/position.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	45	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	46	ML_file "General/input.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	47	ML_file "General/antiquote.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	48	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	49	ML_file "ML/ml_compiler1.ML";
56288 bf1bdf335ea0 tuned comments; wenzelm parents: 56287 diff changeset	50
59054 61b723761dff load simple_thread.ML later, such that it benefits from redefined print_exception_trace; wenzelm parents: 59026 diff changeset	51
62912 745d31e63c21 section headings for ROOT.ML; wenzelm parents: 62911 diff changeset	52	section "Bootstrap phase 2: towards ML within Isar context";
56288 bf1bdf335ea0 tuned comments; wenzelm parents: 56287 diff changeset	53
62912 745d31e63c21 section headings for ROOT.ML; wenzelm parents: 62911 diff changeset	54	subsection "Library of general tools";
56288 bf1bdf335ea0 tuned comments; wenzelm parents: 56287 diff changeset	55
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	56	ML_file "General/integer.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	57	ML_file "General/stack.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	58	ML_file "General/queue.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	59	ML_file "General/heap.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	60	ML_file "General/same.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	61	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	62	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	63	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	64	ML_file "General/buffer.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	65	ML_file "General/pretty.ML";
63209 82cd1d481eb9 ML pp for Rat.rat; wenzelm parents: 63197 diff changeset	66	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	67	ML_file "PIDE/xml.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	68	ML_file "General/path.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	69	ML_file "General/url.ML";
64304 96bc94c87a81 clarified modules; wenzelm parents: 63932 diff changeset	70	ML_file "System/bash_syntax.ML";
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	71	ML_file "General/file.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	72	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	73	ML_file "General/binding.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	74	ML_file "General/socket_io.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	75	ML_file "General/seq.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	76	ML_file "General/timing.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	77	ML_file "General/sha1.ML";
35628 f1456d045151 Digesting strings according to SHA-1. wenzelm parents: 35626 diff changeset	78
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	79	ML_file "PIDE/yxml.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	80	ML_file "PIDE/document_id.ML";
44698 0385292321a0 moved XML/YXML to src/Pure/PIDE; wenzelm parents: 44549 diff changeset	81
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	82	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	83	ML_file "General/graph.ML";
49560 11430dd89e35 added graph encode/decode operations; wenzelm parents: 49041 diff changeset	84
60911 858694df711b default ML context for forks, e.g. relevant for debugging and toplevel pretty-printing; wenzelm parents: 60630 diff changeset	85
62912 745d31e63c21 section headings for ROOT.ML; wenzelm parents: 62911 diff changeset	86	subsection "Fundamental structures";
60911 858694df711b default ML context for forks, e.g. relevant for debugging and toplevel pretty-printing; wenzelm parents: 60630 diff changeset	87
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	88	ML_file "name.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	89	ML_file "term.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	90	ML_file "context.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	91	ML_file "context_position.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	92	ML_file "System/options.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	93	ML_file "config.ML";
51947 3301612c4893 support for system options as context-sensitive config options; wenzelm parents: 51933 diff changeset	94
31432 9858f32f9569 just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources; wenzelm parents: 31335 diff changeset	95
62912 745d31e63c21 section headings for ROOT.ML; wenzelm parents: 62911 diff changeset	96	subsection "Concurrency within the ML runtime";
28120 dd4297f5b495 added Concurrent/schedule.ML; wenzelm parents: 27642 diff changeset	97
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	98	ML_file "ML/exn_properties.ML";
50911 ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset; wenzelm parents: 50800 diff changeset	99
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	100	ML_file "ML/ml_statistics.ML";
50255 d0ec1f0d1d7d some support for ML runtime statistics; wenzelm parents: 50217 diff changeset	101
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	102	ML_file "Concurrent/thread_data_virtual.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	103	ML_file "Concurrent/standard_thread.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	104	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	105
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	106	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	107	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	108	ML_file "Concurrent/future.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	109	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	110	ML_file "Concurrent/timeout.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	111	ML_file "Concurrent/lazy.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	112	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	113
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	114	ML_file "Concurrent/mailbox.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	115	ML_file "Concurrent/cache.ML";
32840 75dff0bd4d5d Concurrently cached values. wenzelm parents: 32816 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 "PIDE/active.ML";
50500 c94bba7906d2 identify dialogs via official serial and maintain as result message; wenzelm parents: 50498 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 "Inner syntax";
31432 9858f32f9569 just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources; wenzelm parents: 31335 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 "Syntax/type_annotation.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	123	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	124	ML_file "Syntax/lexicon.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	125	ML_file "Syntax/ast.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	126	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	127	ML_file "Syntax/parser.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	128	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	129	ML_file "Syntax/mixfix.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	130	ML_file "Syntax/printer.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	131	ML_file "Syntax/syntax.ML";
22679 68cd69a388e2 removed Pure/Syntax/ROOT.ML; wenzelm parents: 22592 diff changeset	132
31432 9858f32f9569 just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources; wenzelm parents: 31335 diff changeset	133
62912 745d31e63c21 section headings for ROOT.ML; wenzelm parents: 62911 diff changeset	134	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	135
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	136	ML_file "term_ord.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	137	ML_file "term_subst.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	138	ML_file "term_xml.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	139	ML_file "General/completion.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	140	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	141	ML_file "sorts.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	142	ML_file "type.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	143	ML_file "logic.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	144	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	145	ML_file "net.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	146	ML_file "item_net.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	147	ML_file "envir.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	148	ML_file "consts.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	149	ML_file "primitive_defs.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	150	ML_file "sign.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	151	ML_file "defs.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	152	ML_file "term_sharing.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	153	ML_file "pattern.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	154	ML_file "unify.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	155	ML_file "theory.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	156	ML_file "proofterm.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	157	ML_file "thm.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	158	ML_file "more_pattern.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	159	ML_file "more_unify.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	160	ML_file "more_thm.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	161	ML_file "facts.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	162	ML_file "global_theory.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	163	ML_file "pure_thy.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	164	ML_file "drule.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	165	ML_file "morphism.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	166	ML_file "variable.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	167	ML_file "conv.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	168	ML_file "goal_display.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	169	ML_file "tactical.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	170	ML_file "search.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	171	ML_file "tactic.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	172	ML_file "raw_simplifier.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	173	ML_file "conjunction.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	174	ML_file "assumption.ML";
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	175
31432 9858f32f9569 just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources; wenzelm parents: 31335 diff changeset	176
62912 745d31e63c21 section headings for ROOT.ML; wenzelm parents: 62911 diff changeset	177	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	178
56303 4cc3f4db3447 clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler; wenzelm parents: 56288 diff changeset	179	(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	180	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	181	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	182	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	183	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	184	ML_file_no_debug "ML/exn_debugger.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	185	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	186	ML_file "PIDE/execution.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	187	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	188
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	189	ML_file "skip_proof.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	190	ML_file "goal.ML";
49041 9edfd36a0355 more informative error message from failed goal forks (violating old-style TTY protocol!); wenzelm parents: 48990 diff changeset	191
63639 4302f86920fe clarified bootstrap; wenzelm parents: 63209 diff changeset	192	(outer syntax)
4302f86920fe clarified bootstrap; wenzelm parents: 63209 diff changeset	193	ML_file "Isar/keyword.ML";
4302f86920fe clarified bootstrap; wenzelm parents: 63209 diff changeset	194	ML_file "Isar/token.ML";
4302f86920fe clarified bootstrap; wenzelm parents: 63209 diff changeset	195	ML_file "Isar/parse.ML";
4302f86920fe clarified bootstrap; wenzelm parents: 63209 diff changeset	196	ML_file "Thy/thy_header.ML";
4302f86920fe clarified bootstrap; wenzelm parents: 63209 diff changeset	197
31432 9858f32f9569 just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources; wenzelm parents: 31335 diff changeset	198	(proof context)
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	199	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	200	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	201	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	202	ML_file "type_infer.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	203	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	204	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	205	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	206	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	207	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	208
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	209	(theory specifications)
63639 4302f86920fe clarified bootstrap; wenzelm parents: 63209 diff changeset	210	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	211	ML_file "Isar/local_theory.ML";
63090 7aa9ac5165e4 common entity definitions within a global or local theory context; wenzelm parents: 63064 diff changeset	212	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	213	ML_file "PIDE/command_span.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	214	ML_file "Thy/thy_syntax.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	215	ML_file "Thy/markdown.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	216	ML_file "Thy/html.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	217	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	218
56203 76c72f4d0667 clarified bootstrap process: switch to ML with context and antiquotations earlier; wenzelm parents: 56072 diff changeset	219	(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	220	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	221	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	222	ML_file "ML/ml_compiler2.ML";
56434 7acc933bd7cc clarified ML bootstrap; wenzelm parents: 56303 diff changeset	223
56288 bf1bdf335ea0 tuned comments; wenzelm parents: 56287 diff changeset	224
62912 745d31e63c21 section headings for ROOT.ML; wenzelm parents: 62911 diff changeset	225	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	226
31432 9858f32f9569 just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources; wenzelm parents: 31335 diff changeset	227	(basic proof engine)
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	228	ML_file "par_tactical.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	229	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	230	ML_file "Isar/attrib.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	231	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	232	ML_file "Isar/method.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	233	ML_file "Isar/proof.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	234	ML_file "Isar/element.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	235	ML_file "Isar/obtain.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	236	ML_file "Isar/subgoal.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	237	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	238
9858f32f9569 just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources; wenzelm parents: 31335 diff changeset	239	(local theories and targets)
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	240	ML_file "Isar/locale.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	241	ML_file "Isar/generic_target.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	242	ML_file "Isar/overloading.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	243	ML_file "axclass.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	244	ML_file "Isar/class.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	245	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	246	ML_file "Isar/expression.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	247	ML_file "Isar/interpretation.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	248	ML_file "Isar/class_declaration.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	249	ML_file "Isar/bundle.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	250	ML_file "Isar/experiment.ML";
31432 9858f32f9569 just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources; wenzelm parents: 31335 diff changeset	251
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	252	ML_file "simplifier.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	253	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	254
9858f32f9569 just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources; wenzelm parents: 31335 diff changeset	255	(executable theory content)
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	256	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	257
9858f32f9569 just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources; wenzelm parents: 31335 diff changeset	258	(specifications)
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	259	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	260	ML_file "Isar/specification.ML";
63064 2f18172214c8 support 'assumes' in specifications, e.g. 'definition', 'inductive'; wenzelm parents: 62943 diff changeset	261	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	262	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	263
9858f32f9569 just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources; wenzelm parents: 31335 diff changeset	264	(toplevel transactions)
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	265	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	266	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	267
56206 7adec2a527f5 clarified module arrangement; wenzelm parents: 56205 diff changeset	268	(proof term operations)
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	269	ML_file "Proof/reconstruct.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	270	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	271	ML_file "Proof/proof_rewrite_rules.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	272	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	273	ML_file "Proof/extraction.ML";
56206 7adec2a527f5 clarified module arrangement; wenzelm parents: 56205 diff changeset	274
62584 6cd36a0d2a28 clarified files; wenzelm parents: 62573 diff changeset	275	(Isabelle system)
62911 78e03d8bf1c4 back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space; wenzelm parents: 62908 diff changeset	276	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	277	ML_file "System/isabelle_system.ML";
62584 6cd36a0d2a28 clarified files; wenzelm parents: 62573 diff changeset	278
62845 31177a9c3025 clarified modules; wenzelm parents: 62825 diff changeset	279
38271 36187e8443dd Isar_Document command input via native Isabelle_Process commands, using YXML and XML_Data representation; wenzelm parents: 38266 diff changeset	280	(theory documents)
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	281	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	282	ML_file "Isar/outer_syntax.ML";
67138 82283d52b4d6 system option for default command tags; wenzelm parents: 65505 diff changeset	283	ML_file "ML/ml_antiquotations.ML";
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	284	ML_file "Thy/thy_output.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	285	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	286	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	287	ML_file "pure_syn.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	288	ML_file "PIDE/command.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	289	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	290	ML_file "PIDE/resources.ML";
65505 741fad555d82 exclude theories from other sessions; wenzelm parents: 64304 diff changeset	291	ML_file "Thy/present.ML";
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	292	ML_file "Thy/thy_info.ML";
67215 03d0c958d65a PIDE markup for session ROOT files; wenzelm parents: 67205 diff changeset	293	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	294	ML_file "PIDE/session.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	295	ML_file "PIDE/protocol_message.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	296	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	297
9858f32f9569 just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources; wenzelm parents: 31335 diff changeset	298	(theory and proof operations)
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	299	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	300
9858f32f9569 just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources; wenzelm parents: 31335 diff changeset	301
62912 745d31e63c21 section headings for ROOT.ML; wenzelm parents: 62911 diff changeset	302	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	303
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	304	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	305	ML_file "System/system_channel.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	306	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	307	ML_file "System/isabelle_process.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	308	ML_file "System/invoke_scala.ML";
67275 5e427586cb57 check bibtex database on ML side -- for semantic PIDE editing; wenzelm parents: 67274 diff changeset	309	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	310	ML_file "PIDE/protocol.ML";
62930 51ac6bc389e8 shared output primitives of physical/virtual Pure; wenzelm parents: 62923 diff changeset	311	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	312
31432 9858f32f9569 just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources; wenzelm parents: 31335 diff changeset	313
62912 745d31e63c21 section headings for ROOT.ML; wenzelm parents: 62911 diff changeset	314	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	315
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	316	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	317	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	318	ML_file "ML/ml_file.ML";
62849 caaa2fc4040d clarified bootstrap -- avoid 'ML_file' in Pure.thy for uniformity; wenzelm parents: 62848 diff changeset	319
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	320	ML_file "Tools/build.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	321	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	322	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	323	ML_file "Tools/rail.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	324	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	325	ML_file "Tools/thm_deps.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	326	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	327	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	328	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	329	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	330	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	331	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	332	ML_file "Tools/named_theorems.ML";
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62896 diff changeset	333	ML_file "Tools/jedit.ML";

author	wenzelm
	Thu, 28 Dec 2017 12:36:11 +0100
changeset 67287	7ef1c5dada12
parent 67275	5e427586cb57
child 67386	998e01d6f8fd
permissions	-rw-r--r--