isabelle: src/Pure/ROOT@31d810570879 (annotated)

51397 03b586ee5930 support for 'chapter' specifications within session ROOT; wenzelm parents: 50911 diff changeset	1	chapter Pure
03b586ee5930 support for 'chapter' specifications within session ROOT; wenzelm parents: 50911 diff changeset	2
48738 f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default; wenzelm parents: 48732 diff changeset	3	session RAW =
48916 f45ccc0d1ace clarified syntax boundary cases and errors; wenzelm parents: 48879 diff changeset	4	theories
48347 8bb27ab9e841 more explicit treatment of initial Pure sessions; wenzelm parents: diff changeset	5	files
8bb27ab9e841 more explicit treatment of initial Pure sessions; wenzelm parents: diff changeset	6	"General/exn.ML"
8bb27ab9e841 more explicit treatment of initial Pure sessions; wenzelm parents: diff changeset	7	"ML-Systems/compiler_polyml.ML"
59470 31d810570879 tuned bootstrap; wenzelm parents: 59172 diff changeset	8	"ML-Systems/exn_trace_polyml-5.5.1.ML"
48347 8bb27ab9e841 more explicit treatment of initial Pure sessions; wenzelm parents: diff changeset	9	"ML-Systems/ml_name_space.ML"
56435 28b34e8e4a80 approximate ML antiquotation @{here} for Isabelle/Pure bootstrap; wenzelm parents: 56303 diff changeset	10	"ML-Systems/ml_positions.ML"
48347 8bb27ab9e841 more explicit treatment of initial Pure sessions; wenzelm parents: diff changeset	11	"ML-Systems/ml_pretty.ML"
8bb27ab9e841 more explicit treatment of initial Pure sessions; wenzelm parents: diff changeset	12	"ML-Systems/ml_system.ML"
8bb27ab9e841 more explicit treatment of initial Pure sessions; wenzelm parents: diff changeset	13	"ML-Systems/multithreading.ML"
8bb27ab9e841 more explicit treatment of initial Pure sessions; wenzelm parents: diff changeset	14	"ML-Systems/multithreading_polyml.ML"
8bb27ab9e841 more explicit treatment of initial Pure sessions; wenzelm parents: diff changeset	15	"ML-Systems/overloading_smlnj.ML"
8bb27ab9e841 more explicit treatment of initial Pure sessions; wenzelm parents: diff changeset	16	"ML-Systems/polyml.ML"
54723 124432e77ecf simplified polyml-5.5.2 setup -- implicit upgrade of Thread.numProcessors; wenzelm parents: 54717 diff changeset	17	"ML-Systems/polyml-5.5.2.ML"
58470 890d8286fd4e pro-forma support for polyml-5.5.3 (presently SVN 1960); wenzelm parents: 58009 diff changeset	18	"ML-Systems/polyml-5.5.3.ML"
48347 8bb27ab9e841 more explicit treatment of initial Pure sessions; wenzelm parents: diff changeset	19	"ML-Systems/pp_dummy.ML"
8bb27ab9e841 more explicit treatment of initial Pure sessions; wenzelm parents: diff changeset	20	"ML-Systems/proper_int.ML"
8bb27ab9e841 more explicit treatment of initial Pure sessions; wenzelm parents: diff changeset	21	"ML-Systems/single_assignment.ML"
8bb27ab9e841 more explicit treatment of initial Pure sessions; wenzelm parents: diff changeset	22	"ML-Systems/single_assignment_polyml.ML"
52711 155f02cacb2d old Poly/ML 5.3.0 cannot share the massive heap of HOL anymore (after introduction of immutable theory in 38466f4f3483); wenzelm parents: 52605 diff changeset	23	"ML-Systems/share_common_data_polyml-5.3.0.ML"
48347 8bb27ab9e841 more explicit treatment of initial Pure sessions; wenzelm parents: diff changeset	24	"ML-Systems/smlnj.ML"
8bb27ab9e841 more explicit treatment of initial Pure sessions; wenzelm parents: diff changeset	25	"ML-Systems/thread_dummy.ML"
8bb27ab9e841 more explicit treatment of initial Pure sessions; wenzelm parents: diff changeset	26	"ML-Systems/universal.ML"
8bb27ab9e841 more explicit treatment of initial Pure sessions; wenzelm parents: diff changeset	27	"ML-Systems/unsynchronized.ML"
8bb27ab9e841 more explicit treatment of initial Pure sessions; wenzelm parents: diff changeset	28	"ML-Systems/use_context.ML"
8bb27ab9e841 more explicit treatment of initial Pure sessions; wenzelm parents: diff changeset	29
48738 f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default; wenzelm parents: 48732 diff changeset	30	session Pure =
56801 8dd9df88f647 some support for session-qualified theories: allow to refer to resources via qualified name instead of odd file-system path; wenzelm parents: 56435 diff changeset	31	global_theories Pure
48514 84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	32	files
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	33	"General/exn.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	34	"ML-Systems/compiler_polyml.ML"
59470 31d810570879 tuned bootstrap; wenzelm parents: 59172 diff changeset	35	"ML-Systems/exn_trace_polyml-5.5.1.ML"
48514 84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	36	"ML-Systems/ml_name_space.ML"
56435 28b34e8e4a80 approximate ML antiquotation @{here} for Isabelle/Pure bootstrap; wenzelm parents: 56303 diff changeset	37	"ML-Systems/ml_positions.ML"
48514 84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	38	"ML-Systems/ml_pretty.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	39	"ML-Systems/ml_system.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	40	"ML-Systems/multithreading.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	41	"ML-Systems/multithreading_polyml.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	42	"ML-Systems/overloading_smlnj.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	43	"ML-Systems/polyml.ML"
54723 124432e77ecf simplified polyml-5.5.2 setup -- implicit upgrade of Thread.numProcessors; wenzelm parents: 54717 diff changeset	44	"ML-Systems/polyml-5.5.2.ML"
58470 890d8286fd4e pro-forma support for polyml-5.5.3 (presently SVN 1960); wenzelm parents: 58009 diff changeset	45	"ML-Systems/polyml-5.5.3.ML"
48514 84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	46	"ML-Systems/pp_dummy.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	47	"ML-Systems/proper_int.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	48	"ML-Systems/single_assignment.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	49	"ML-Systems/single_assignment_polyml.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	50	"ML-Systems/smlnj.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	51	"ML-Systems/thread_dummy.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	52	"ML-Systems/universal.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	53	"ML-Systems/unsynchronized.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	54	"ML-Systems/use_context.ML"
48347 8bb27ab9e841 more explicit treatment of initial Pure sessions; wenzelm parents: diff changeset	55
48514 84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	56	"Concurrent/bash.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	57	"Concurrent/bash_sequential.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	58	"Concurrent/cache.ML"
52050 b40ed9dcf903 event timer as separate service thread; wenzelm parents: 52010 diff changeset	59	"Concurrent/event_timer.ML"
48514 84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	60	"Concurrent/future.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	61	"Concurrent/lazy.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	62	"Concurrent/lazy_sequential.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	63	"Concurrent/mailbox.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	64	"Concurrent/par_exn.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	65	"Concurrent/par_list.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	66	"Concurrent/par_list_sequential.ML"
59172 d1c500e0a722 separate module Random; wenzelm parents: 59064 diff changeset	67	"Concurrent/random.ML"
48514 84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	68	"Concurrent/simple_thread.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	69	"Concurrent/single_assignment.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	70	"Concurrent/single_assignment_sequential.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	71	"Concurrent/synchronized.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	72	"Concurrent/synchronized_sequential.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	73	"Concurrent/task_queue.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	74	"Concurrent/time_limit.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	75	"General/alist.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	76	"General/antiquote.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	77	"General/balanced_tree.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	78	"General/basics.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	79	"General/binding.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	80	"General/buffer.ML"
56053 030531cc4c62 tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates; wenzelm parents: 55672 diff changeset	81	"General/change_table.ML"
55672 5e25cc741ab9 support for completion within the formal context; wenzelm parents: 55516 diff changeset	82	"General/completion.ML"
48514 84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	83	"General/file.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	84	"General/graph.ML"
49561 26fc70e983c2 separate module Graph_Display; wenzelm parents: 48916 diff changeset	85	"General/graph_display.ML"
48514 84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	86	"General/heap.ML"
59064 a8bcb5a446c8 more abstract type Input.source; wenzelm parents: 59026 diff changeset	87	"General/input.ML"
48514 84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	88	"General/integer.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	89	"General/linear_set.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	90	"General/long_name.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	91	"General/name_space.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	92	"General/ord_list.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	93	"General/output.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	94	"General/path.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	95	"General/position.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	96	"General/pretty.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	97	"General/print_mode.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	98	"General/properties.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	99	"General/queue.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	100	"General/same.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	101	"General/scan.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	102	"General/secure.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	103	"General/seq.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	104	"General/sha1.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	105	"General/sha1_polyml.ML"
53212 387b9f7cb0ac added SHA1 library integrity test, which is invoked at compile time and Isabelle_Process run-time; wenzelm parents: 52926 diff changeset	106	"General/sha1_samples.ML"
50800 c0fb2839d1a9 recovered buffered sockets from 11f622794ad6 -- requires Poly/ML 5.5.x; wenzelm parents: 50686 diff changeset	107	"General/socket_io.ML"
48514 84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	108	"General/source.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	109	"General/stack.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	110	"General/symbol.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	111	"General/symbol_pos.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	112	"General/table.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	113	"General/timing.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	114	"General/url.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	115	"Isar/args.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	116	"Isar/attrib.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	117	"Isar/auto_bind.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	118	"Isar/bundle.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	119	"Isar/class.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	120	"Isar/class_declaration.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	121	"Isar/code.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	122	"Isar/context_rules.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	123	"Isar/element.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	124	"Isar/expression.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	125	"Isar/generic_target.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	126	"Isar/isar_cmd.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	127	"Isar/keyword.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	128	"Isar/local_defs.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	129	"Isar/local_theory.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	130	"Isar/locale.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	131	"Isar/method.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	132	"Isar/named_target.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	133	"Isar/object_logic.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	134	"Isar/obtain.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	135	"Isar/outer_syntax.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	136	"Isar/overloading.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	137	"Isar/parse.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	138	"Isar/parse_spec.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	139	"Isar/proof.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	140	"Isar/proof_context.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	141	"Isar/proof_display.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	142	"Isar/proof_node.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	143	"Isar/rule_cases.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	144	"Isar/runtime.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	145	"Isar/spec_rules.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	146	"Isar/specification.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	147	"Isar/token.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	148	"Isar/toplevel.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	149	"Isar/typedecl.ML"
56303 4cc3f4db3447 clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler; wenzelm parents: 56210 diff changeset	150	"ML/exn_output.ML"
4cc3f4db3447 clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler; wenzelm parents: 56210 diff changeset	151	"ML/exn_output_polyml.ML"
52010 e91359bfc84a tuned; wenzelm parents: 52009 diff changeset	152	"ML/exn_properties_dummy.ML"
e91359bfc84a tuned; wenzelm parents: 52009 diff changeset	153	"ML/exn_properties_polyml.ML"
48514 84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	154	"ML/install_pp_polyml.ML"
56072 31e427387ab5 tuned signature -- clarified module name; wenzelm parents: 56053 diff changeset	155	"ML/ml_antiquotation.ML"
48514 84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	156	"ML/ml_compiler.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	157	"ML/ml_compiler_polyml.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	158	"ML/ml_context.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	159	"ML/ml_env.ML"
58928 23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes; wenzelm parents: 58846 diff changeset	160	"ML/ml_file.ML"
48514 84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	161	"ML/ml_lex.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	162	"ML/ml_parse.ML"
56303 4cc3f4db3447 clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler; wenzelm parents: 56210 diff changeset	163	"ML/ml_options.ML"
50255 d0ec1f0d1d7d some support for ML runtime statistics; wenzelm parents: 50217 diff changeset	164	"ML/ml_statistics_dummy.ML"
d0ec1f0d1d7d some support for ML runtime statistics; wenzelm parents: 50217 diff changeset	165	"ML/ml_statistics_polyml-5.5.0.ML"
48514 84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	166	"ML/ml_syntax.ML"
50450 358b6020f8b6 generalized notion of active area, where sendback is just one application; wenzelm parents: 50255 diff changeset	167	"PIDE/active.ML"
48514 84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	168	"PIDE/command.ML"
57905 c0c5652e796e separate module Command_Span: mostly syntactic representation; wenzelm parents: 56801 diff changeset	169	"PIDE/command_span.ML"
48514 84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	170	"PIDE/document.ML"
52530 99dd8b4ef3fe explicit module Document_ID as source of globally unique identifiers across ML/Scala; wenzelm parents: 52211 diff changeset	171	"PIDE/document_id.ML"
52605 a2a805549c74 clarified module name; wenzelm parents: 52596 diff changeset	172	"PIDE/execution.ML"
48514 84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	173	"PIDE/markup.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	174	"PIDE/protocol.ML"
52865 02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay; wenzelm parents: 52836 diff changeset	175	"PIDE/query_operation.ML"
56208 06cc31dff138 clarifed module name; wenzelm parents: 56072 diff changeset	176	"PIDE/resources.ML"
56210 c7c85cdb725d clarified module arrangement; wenzelm parents: 56208 diff changeset	177	"PIDE/session.ML"
48514 84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	178	"PIDE/xml.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	179	"PIDE/yxml.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	180	"Proof/extraction.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	181	"Proof/proof_checker.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	182	"Proof/proof_rewrite_rules.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	183	"Proof/proof_syntax.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	184	"Proof/reconstruct.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	185	"ROOT.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	186	"Syntax/ast.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	187	"Syntax/lexicon.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	188	"Syntax/local_syntax.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	189	"Syntax/mixfix.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	190	"Syntax/parser.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	191	"Syntax/printer.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	192	"Syntax/simple_syntax.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	193	"Syntax/syntax.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	194	"Syntax/syntax_ext.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	195	"Syntax/syntax_phases.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	196	"Syntax/syntax_trans.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	197	"Syntax/term_position.ML"
52211 66bc827e37f8 explicit support for type annotations within printed syntax trees; wenzelm parents: 52050 diff changeset	198	"Syntax/type_annotation.ML"
48681 181b91e1d1c1 prefer general Command_Line.tool wrapper (cf. Scala version); wenzelm parents: 48646 diff changeset	199	"System/command_line.ML"
48514 84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	200	"System/invoke_scala.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	201	"System/isabelle_process.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	202	"System/isabelle_system.ML"
52584 5cad4a5f5615 more abstract message channel; wenzelm parents: 52530 diff changeset	203	"System/message_channel.ML"
48514 84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	204	"System/options.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	205	"System/system_channel.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	206	"Thy/html.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	207	"Thy/latex.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	208	"Thy/present.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	209	"Thy/term_style.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	210	"Thy/thy_header.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	211	"Thy/thy_info.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	212	"Thy/thy_output.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	213	"Thy/thy_syntax.ML"
50686 d703e3aafa8c moved files; wenzelm parents: 50450 diff changeset	214	"Tools/build.ML"
48514 84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	215	"Tools/named_thms.ML"
58660 8d4aebb9e327 clarified load order; wenzelm parents: 58470 diff changeset	216	"Tools/plugin.ML"
48514 84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	217	"assumption.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	218	"axclass.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	219	"config.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	220	"conjunction.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	221	"consts.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	222	"context.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	223	"context_position.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	224	"conv.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	225	"defs.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	226	"display.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	227	"drule.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	228	"envir.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	229	"facts.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	230	"global_theory.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	231	"goal.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	232	"goal_display.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	233	"item_net.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	234	"library.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	235	"logic.ML"
59026 30b8a5825a9c removed some add-ons from modules that are relevant for the inference kernel; wenzelm parents: 58928 diff changeset	236	"more_pattern.ML"
48514 84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	237	"more_thm.ML"
59026 30b8a5825a9c removed some add-ons from modules that are relevant for the inference kernel; wenzelm parents: 58928 diff changeset	238	"more_unify.ML"
48514 84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	239	"morphism.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	240	"name.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	241	"net.ML"
58009 987c848d509b clarified modules; wenzelm parents: 57934 diff changeset	242	"par_tactical.ML"
48514 84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	243	"pattern.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	244	"primitive_defs.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	245	"proofterm.ML"
48879 cb5cdbb645cd clarified bootstrapping of Pure; wenzelm parents: 48738 diff changeset	246	"pure_syn.ML"
48514 84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	247	"pure_thy.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	248	"raw_simplifier.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	249	"search.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	250	"sign.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	251	"simplifier.ML"
51551 88d1d19fb74f tuned signature and module arrangement; wenzelm parents: 51397 diff changeset	252	"skip_proof.ML"
48514 84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	253	"sorts.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	254	"subgoal.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	255	"tactic.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	256	"tactical.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	257	"term.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	258	"term_ord.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	259	"term_sharing.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	260	"term_subst.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	261	"term_xml.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	262	"theory.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	263	"thm.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	264	"type.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	265	"type_infer.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	266	"type_infer_context.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	267	"unify.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	268	"variable.ML"
84df8858c8ac more files for session Pure; wenzelm parents: 48422 diff changeset	269

author	wenzelm
	Thu, 29 Jan 2015 16:16:01 +0100
changeset 59470	31d810570879
parent 59172	d1c500e0a722
child 59714	ae322325adbb
permissions	-rw-r--r--