Summary
- merged
- simplified;
- obsolete;
- isabelle console -r" helps to bootstrap Isabelle/Pure;
- discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
- proper return code (cf. faa452d8e265);
- clarified isabelle_process;
- clarified modules; tuned signature;
- clarified modules;
- clarified modules;
- removed junk;
- discontinued polyml-5.3.0;
The file was modified | src/Doc/System/Basics.thy (diff) |
The file was modified | src/HOL/Mirabelle/lib/scripts/mirabelle.pl (diff) |
The file was modified | src/Tools/Code/code_ml.ML (diff) |
The file was modified | src/Pure/ML/ml_name_space.ML (diff) |
The file was modified | NEWS (diff) |
The file was modified | lib/Tools/console (diff) |
The file was modified | src/Doc/System/Misc.thy (diff) |
The file was added | src/Pure/Concurrent/multithreading.ML |
The file was added | src/Pure/Concurrent/unsynchronized.ML |
The file was added | src/Pure/General/exn.ML |
The file was added | src/Pure/General/exn.scala |
The file was added | src/Pure/General/secure.ML |
The file was added | src/Pure/ML/fixed_int_dummy.ML |
The file was added | src/Pure/ML/ml_compiler0.ML |
The file was added | src/Pure/ML/ml_debugger.ML |
The file was added | src/Pure/ML/ml_heap.ML |
The file was added | src/Pure/ML/ml_name_space.ML |
The file was added | src/Pure/ML/ml_pretty.ML |
The file was added | src/Pure/ML/ml_profiling.ML |
The file was added | src/Pure/ML/ml_system.ML |
The file was modified | src/Pure/ROOT (diff) |
The file was modified | src/Pure/ROOT.ML (diff) |
The file was modified | src/Pure/Tools/build.scala (diff) |
The file was modified | src/Pure/build-jars (diff) |
The file was removed | src/Pure/RAW/ROOT_polyml.ML |
The file was removed | src/Pure/RAW/exn.ML |
The file was removed | src/Pure/RAW/exn.scala |
The file was removed | src/Pure/RAW/fixed_int_dummy.ML |
The file was removed | src/Pure/RAW/ml_compiler0.ML |
The file was removed | src/Pure/RAW/ml_debugger.ML |
The file was removed | src/Pure/RAW/ml_heap.ML |
The file was removed | src/Pure/RAW/ml_name_space.ML |
The file was removed | src/Pure/RAW/ml_pretty.ML |
The file was removed | src/Pure/RAW/ml_profiling.ML |
The file was removed | src/Pure/RAW/ml_system.ML |
The file was removed | src/Pure/RAW/multithreading.ML |
The file was removed | src/Pure/RAW/secure.ML |
The file was removed | src/Pure/RAW/unsynchronized.ML |
The file was modified | bin/isabelle_process (diff) |
The file was modified | NEWS (diff) |
The file was modified | bin/isabelle_process (diff) |
The file was modified | lib/scripts/recode.pl (diff) |
The file was modified | src/Doc/System/Basics.thy (diff) |
The file was removed | lib/scripts/run-polyml |
The file was modified | src/Doc/Implementation/ML.thy (diff) |
The file was modified | src/HOL/Matrix_LP/Cplex_tools.ML (diff) |
The file was modified | src/HOL/Mirabelle/Tools/mirabelle.ML (diff) |
The file was modified | src/HOL/Nitpick_Examples/Mono_Nits.thy (diff) |
The file was modified | src/HOL/TPTP/TPTP_Interpret_Test.thy (diff) |
The file was modified | src/HOL/TPTP/TPTP_Test.thy (diff) |
The file was modified | src/HOL/Tools/Old_Datatype/old_datatype.ML (diff) |
The file was modified | src/HOL/Tools/Sledgehammer/sledgehammer.ML (diff) |
The file was modified | src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML (diff) |
The file was modified | src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML (diff) |
The file was modified | src/Pure/Concurrent/bash.ML (diff) |
The file was modified | src/Pure/Concurrent/bash_windows.ML (diff) |
The file was modified | src/Pure/Concurrent/future.ML (diff) |
The file was modified | src/Pure/Concurrent/par_exn.ML (diff) |
The file was modified | src/Pure/Concurrent/par_list.ML (diff) |
The file was modified | src/Pure/Concurrent/single_assignment.ML (diff) |
The file was modified | src/Pure/Concurrent/standard_thread.ML (diff) |
The file was modified | src/Pure/Concurrent/synchronized.ML (diff) |
The file was modified | src/Pure/General/basics.ML (diff) |
The file was modified | src/Pure/Isar/runtime.ML (diff) |
The file was modified | src/Pure/Isar/toplevel.ML (diff) |
The file was modified | src/Pure/ML/ml_compiler.ML (diff) |
The file was modified | src/Pure/PIDE/command.ML (diff) |
The file was modified | src/Pure/PIDE/document.ML (diff) |
The file was modified | src/Pure/PIDE/protocol.ML (diff) |
The file was modified | src/Pure/RAW/ROOT_polyml.ML (diff) |
The file was modified | src/Pure/RAW/exn.ML (diff) |
The file was modified | src/Pure/RAW/ml_compiler0.ML (diff) |
The file was modified | src/Pure/ROOT (diff) |
The file was modified | src/Pure/Syntax/syntax_phases.ML (diff) |
The file was modified | src/Pure/System/invoke_scala.ML (diff) |
The file was modified | src/Pure/System/isabelle_process.ML (diff) |
The file was modified | src/Pure/Tools/debugger.ML (diff) |
The file was modified | src/Pure/Tools/simplifier_trace.ML (diff) |
The file was modified | src/Pure/morphism.ML (diff) |
The file was modified | src/Tools/try.ML (diff) |
The file was removed | src/Pure/RAW/exn_trace.ML |
The file was modified | src/Pure/RAW/ROOT_polyml.ML (diff) |
The file was modified | src/Pure/RAW/ml_compiler0.ML (diff) |
The file was modified | src/Pure/RAW/ml_name_space.ML (diff) |
The file was modified | src/Pure/ROOT (diff) |
The file was modified | src/Pure/Tools/debugger.ML (diff) |
The file was removed | src/Pure/RAW/ml_positions.ML |
The file was modified | src/Pure/General/linear_set.ML (diff) |
The file was modified | src/Pure/General/table.ML (diff) |
The file was modified | src/Pure/ML/exn_output.ML (diff) |
The file was modified | src/Pure/ML/install_pp_polyml.ML (diff) |
The file was modified | src/Pure/ML/ml_compiler.ML (diff) |
The file was modified | src/Pure/RAW/ROOT_polyml.ML (diff) |
The file was modified | src/Pure/RAW/ml_debugger.ML (diff) |
The file was modified | src/Pure/RAW/ml_pretty.ML (diff) |
The file was modified | src/HOL/Nat.thy (diff) |
The file was added | src/Pure/RAW/ml_name_space.ML |
The file was added | src/Pure/RAW/ml_profiling.ML |
The file was modified | Admin/Release/CHECKLIST (diff) |
The file was modified | Admin/isatest/settings/at-poly (diff) |
The file was modified | NEWS (diff) |
The file was modified | src/Pure/Concurrent/standard_thread.ML (diff) |
The file was modified | src/Pure/ML/ml_compiler.ML (diff) |
The file was modified | src/Pure/RAW/ROOT_polyml.ML (diff) |
The file was modified | src/Pure/RAW/ml_compiler0.ML (diff) |
The file was modified | src/Pure/RAW/ml_debugger.ML (diff) |
The file was modified | src/Pure/RAW/multithreading.ML (diff) |
The file was modified | src/Pure/ROOT (diff) |
The file was modified | src/Pure/ROOT.ML (diff) |
The file was modified | src/Pure/System/system_channel.ML (diff) |
The file was removed | lib/scripts/run-polyml-5.3.0 |
The file was removed | src/Pure/RAW/ROOT_polyml-5.6.ML |
The file was removed | src/Pure/RAW/exn_trace_raw.ML |
The file was removed | src/Pure/RAW/ml_compiler_parameters.ML |
The file was removed | src/Pure/RAW/ml_compiler_parameters_polyml-5.6.ML |
The file was removed | src/Pure/RAW/ml_debugger_polyml-5.6.ML |
The file was removed | src/Pure/RAW/ml_heap_polyml-5.3.0.ML |
The file was removed | src/Pure/RAW/ml_name_space_polyml-5.6.ML |
The file was removed | src/Pure/RAW/ml_name_space_polyml.ML |
The file was removed | src/Pure/RAW/ml_parse_tree.ML |
The file was removed | src/Pure/RAW/ml_parse_tree_polyml-5.6.ML |
The file was removed | src/Pure/RAW/ml_profiling_polyml-5.6.ML |
The file was removed | src/Pure/RAW/ml_profiling_polyml.ML |
The file was removed | src/Pure/RAW/ml_stack_dummy.ML |
The file was removed | src/Pure/RAW/ml_stack_polyml-5.6.ML |
The file was removed | src/Pure/RAW/single_assignment_polyml.ML |