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

author	wenzelm
	Thu, 07 Apr 2016 22:09:23 +0200
changeset 62912	745d31e63c21
parent 62911	78e03d8bf1c4
child 62918	2fcbd4abc021
permissions	-rw-r--r--