#
ab35abfc |
|
11-May-2018 |
wenzelm <none@none> |
some export of foundational theory content;
|
#
f636012e |
|
06-May-2018 |
wenzelm <none@none> |
tuned signature; clarified modules;
|
#
0e94bb02 |
|
10-Feb-2018 |
wenzelm <none@none> |
more accessible src/Pure/ROOT.ML;
|
#
e6395a2a |
|
14-Jan-2018 |
wenzelm <none@none> |
clarified modules: uniform notion of formal comments;
|
#
0ce84d08 |
|
09-Jan-2018 |
wenzelm <none@none> |
clarified modules;
|
#
46e41c4f |
|
24-Dec-2017 |
wenzelm <none@none> |
check bibtex database on ML side -- for semantic PIDE editing; tuned signature;
|
#
72f6cf9d |
|
24-Dec-2017 |
wenzelm <none@none> |
clarified directories; --HG-- rename : src/Pure/Tools/bibtex.ML => src/Pure/Thy/bibtex.ML rename : src/Pure/Tools/bibtex.scala => src/Pure/Thy/bibtex.scala
|
#
dd1da728 |
|
16-Dec-2017 |
wenzelm <none@none> |
PIDE markup for session ROOT files;
|
#
8b9909e2 |
|
14-Dec-2017 |
wenzelm <none@none> |
clarified file name; --HG-- rename : src/Pure/ML/ml_pervasive.ML => src/Pure/ML/ml_init.ML
|
#
7f1efcbe |
|
05-Dec-2017 |
wenzelm <none@none> |
system option for default command tags;
|
#
30fc9a8e |
|
18-Apr-2017 |
wenzelm <none@none> |
exclude theories from other sessions; clarified modules;
|
#
61f649e7 |
|
18-Oct-2016 |
wenzelm <none@none> |
clarified modules;
|
#
3ed788ee |
|
21-Sep-2016 |
wenzelm <none@none> |
more tight implementation of symbol explode operation (without support for raw symbols);
|
#
d6b5ab04 |
|
05-Sep-2016 |
wenzelm <none@none> |
clarified modules; --HG-- rename : src/HOL/Tools/value.ML => src/HOL/Tools/value_command.ML
|
#
7dea8b16 |
|
09-Aug-2016 |
wenzelm <none@none> |
clarified bootstrap;
|
#
1968198b |
|
01-Jun-2016 |
wenzelm <none@none> |
ML pp for Rat.rat;
|
#
ca5b4b9a |
|
31-May-2016 |
wenzelm <none@none> |
rat.ML is now part of Pure to allow tigther integration with Isabelle/ML; --HG-- rename : src/Tools/rat.ML => src/Pure/General/rat.ML
|
#
335fed05 |
|
12-May-2016 |
wenzelm <none@none> |
common entity definitions within a global or local theory context;
|
#
68f9ecca |
|
28-Apr-2016 |
wenzelm <none@none> |
support 'assumes' in specifications, e.g. 'definition', 'inductive'; tuned signatures;
|
#
2a79c460 |
|
10-Apr-2016 |
wenzelm <none@none> |
clarified files; --HG-- rename : src/Pure/ML/ml_pervasive0.ML => src/Pure/ML/ml_pervasive.ML
|
#
fa6ad737 |
|
09-Apr-2016 |
wenzelm <none@none> |
clarified modules; removed unsed exn_id;
|
#
bb099f2e |
|
09-Apr-2016 |
wenzelm <none@none> |
shared output primitives of physical/virtual Pure;
|
#
e5eeadb3 |
|
09-Apr-2016 |
wenzelm <none@none> |
clarified bootstrap;
|
#
e195e62f |
|
09-Apr-2016 |
wenzelm <none@none> |
clarified modules;
|
#
005bf5c3 |
|
07-Apr-2016 |
wenzelm <none@none> |
section headings for ROOT.ML;
|
#
329e641f |
|
07-Apr-2016 |
wenzelm <none@none> |
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
|
#
2eea6c7e |
|
07-Apr-2016 |
wenzelm <none@none> |
clarified mode of ROOT.ML files;
|
#
cd156ec4 |
|
07-Apr-2016 |
wenzelm <none@none> |
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; avoid slowdown of Resources.loaded_files due to command name 'use' in Pure base syntax;
|
#
88f311a7 |
|
07-Apr-2016 |
wenzelm <none@none> |
clarified editor mode;
|
#
f6f948c1 |
|
06-Apr-2016 |
wenzelm <none@none> |
virtual thread data via context, for proper support of Context.>> etc;
|
#
5c02b8f9 |
|
06-Apr-2016 |
wenzelm <none@none> |
clarified bootstrap;
|
#
85397651 |
|
06-Apr-2016 |
wenzelm <none@none> |
clarified modules; tuned signature;
|
#
a6c48975 |
|
06-Apr-2016 |
wenzelm <none@none> |
clarified ML bootstrap; --HG-- rename : src/Pure/ML/ml_pervasive_initial.ML => src/Pure/ML/ml_pervasive0.ML rename : src/Pure/ML/ml_pervasive_final.ML => src/Pure/ML/ml_pervasive1.ML
|
#
f173563a |
|
05-Apr-2016 |
wenzelm <none@none> |
clarified files; --HG-- rename : src/Pure/ML/ML_Root.thy => src/Pure/ML_Root.thy
|
#
58cf84e0 |
|
05-Apr-2016 |
wenzelm <none@none> |
back to static conditional compilation -- simplified bootstrap;
|
#
92e958ff |
|
05-Apr-2016 |
wenzelm <none@none> |
clarified modules -- simplified bootstrap;
|
#
22e77ec1 |
|
05-Apr-2016 |
wenzelm <none@none> |
actually observe ML_system_unsafe, concerning the environment that is stored in theory ML_Root;
|
#
430ea417 |
|
05-Apr-2016 |
wenzelm <none@none> |
prefer antiquotations;
|
#
bc4696c2 |
|
05-Apr-2016 |
wenzelm <none@none> |
proper use_thy;
|
#
c36e1945 |
|
04-Apr-2016 |
wenzelm <none@none> |
more uniform ML file commands;
|
#
d54d78d1 |
|
04-Apr-2016 |
wenzelm <none@none> |
clarified bootstrap -- avoid conditional compilation in ROOT.ML;
|
#
5b0dfdf2 |
|
04-Apr-2016 |
wenzelm <none@none> |
tuned;
|
#
e1066195 |
|
04-Apr-2016 |
wenzelm <none@none> |
clarified modules; --HG-- rename : src/Pure/ML/ml_final.ML => src/Pure/ML/ml_pervasive_final.ML rename : src/Pure/ML/ml_pervasive.ML => src/Pure/ML/ml_pervasive_initial.ML
|
#
a7d79152 |
|
04-Apr-2016 |
wenzelm <none@none> |
clarified conditional compilation;
|
#
97a1298c |
|
04-Apr-2016 |
wenzelm <none@none> |
clarified bootstrap -- avoid 'ML_file' in Pure.thy for uniformity;
|
#
13b5c43b |
|
04-Apr-2016 |
wenzelm <none@none> |
clarified bootstrap -- more uniform use of ML files;
|
#
e45ceaf4 |
|
04-Apr-2016 |
wenzelm <none@none> |
clarified bootstrap;
|
#
39cceb82 |
|
04-Apr-2016 |
wenzelm <none@none> |
clarified final setup of ML environment;
|
#
331761e9 |
|
04-Apr-2016 |
wenzelm <none@none> |
clarified modules;
|
#
fe762f95 |
|
02-Apr-2016 |
wenzelm <none@none> |
structure PolyML is sealed after bootstrap: all ML system access is managed by Isabelle;
|
#
be4465b6 |
|
02-Apr-2016 |
wenzelm <none@none> |
clarified modules;
|
#
2d17444f |
|
02-Apr-2016 |
wenzelm <none@none> |
clarified modules;
|
#
b38efe8a |
|
26-Mar-2016 |
wenzelm <none@none> |
explicit print_depth for the sake of Spec_Check.determine_type;
|
#
4c796807 |
|
25-Mar-2016 |
wenzelm <none@none> |
eliminated duplicate;
|
#
fc0cde3e |
|
18-Mar-2016 |
wenzelm <none@none> |
discontinued slightly odd "secure" mode;
|
#
28e3dd9a |
|
18-Mar-2016 |
wenzelm <none@none> |
clarified modules;
|
#
adf2e75c |
|
18-Mar-2016 |
wenzelm <none@none> |
clarified modules; --HG-- rename : src/Pure/ML/install_pp_polyml.ML => src/Pure/ML/ml_pp.ML
|
#
f0caccd4 |
|
17-Mar-2016 |
wenzelm <none@none> |
@{make_string} is available during Pure bootstrap;
|
#
6b8a9591 |
|
17-Mar-2016 |
wenzelm <none@none> |
clarified modules;
|
#
9ef1c22d |
|
17-Mar-2016 |
wenzelm <none@none> |
hide critical structures of Poly/ML, to make it harder to disrupt the ML environment;
|
#
3619a4a7 |
|
17-Mar-2016 |
wenzelm <none@none> |
obsolete;
|
#
32518342 |
|
17-Mar-2016 |
wenzelm <none@none> |
tuned signature;
|
#
d4c15984 |
|
16-Mar-2016 |
wenzelm <none@none> |
eliminated without magic name;
|
#
240dbecd |
|
10-Mar-2016 |
wenzelm <none@none> |
clarified files; --HG-- rename : src/Pure/Concurrent/random.ML => src/Pure/General/random.ML
|
#
dcabae6a |
|
10-Mar-2016 |
wenzelm <none@none> |
clarified files; --HG-- rename : src/Pure/Concurrent/bash.ML => src/Pure/System/bash.ML rename : src/Pure/Concurrent/bash.scala => src/Pure/System/bash.scala rename : src/Pure/Concurrent/bash_windows.ML => src/Pure/System/bash_windows.ML
|
#
069a632f |
|
09-Mar-2016 |
wenzelm <none@none> |
isabelle.Build uses ML_Process directly; isabelle_process is for batch mode only; removed unused feeder (already part of "isabelle console");
|
#
42d7f45e |
|
07-Mar-2016 |
wenzelm <none@none> |
discontinued cd, pwd;
|
#
c8a3ab07 |
|
05-Mar-2016 |
wenzelm <none@none> |
tuned signature -- clarified modules; --HG-- rename : src/Pure/Concurrent/time_limit.ML => src/Pure/Concurrent/timeout.ML
|
#
73bfea7c |
|
05-Mar-2016 |
wenzelm <none@none> |
tuned signature -- clarified modules;
|
#
866c57fc |
|
03-Mar-2016 |
wenzelm <none@none> |
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM; --HG-- rename : src/Pure/RAW/multithreading.ML => src/Pure/Concurrent/multithreading.ML rename : src/Pure/RAW/unsynchronized.ML => src/Pure/Concurrent/unsynchronized.ML rename : src/Pure/RAW/exn.ML => src/Pure/General/exn.ML rename : src/Pure/RAW/exn.scala => src/Pure/General/exn.scala rename : src/Pure/RAW/secure.ML => src/Pure/General/secure.ML rename : src/Pure/RAW/fixed_int_dummy.ML => src/Pure/ML/fixed_int_dummy.ML rename : src/Pure/RAW/ml_compiler0.ML => src/Pure/ML/ml_compiler0.ML rename : src/Pure/RAW/ml_debugger.ML => src/Pure/ML/ml_debugger.ML rename : src/Pure/RAW/ml_heap.ML => src/Pure/ML/ml_heap.ML rename : src/Pure/RAW/ml_name_space.ML => src/Pure/ML/ml_name_space.ML rename : src/Pure/RAW/ml_pretty.ML => src/Pure/ML/ml_pretty.ML rename : src/Pure/RAW/ml_profiling.ML => src/Pure/ML/ml_profiling.ML rename : src/Pure/RAW/ml_system.ML => src/Pure/ML/ml_system.ML
|
#
a0395a6e |
|
03-Mar-2016 |
wenzelm <none@none> |
discontinued polyml-5.3.0; --HG-- rename : src/Pure/RAW/ml_debugger_polyml-5.6.ML => src/Pure/RAW/ml_debugger.ML rename : src/Pure/RAW/ml_name_space_polyml-5.6.ML => src/Pure/RAW/ml_name_space.ML rename : src/Pure/RAW/ml_profiling_polyml-5.6.ML => src/Pure/RAW/ml_profiling.ML
|
#
ed14f1c4 |
|
02-Mar-2016 |
wenzelm <none@none> |
support for ML_exception_debugger;
|
#
00d0e201 |
|
01-Mar-2016 |
wenzelm <none@none> |
clarified modules; --HG-- rename : src/Pure/RAW/compiler_polyml.ML => src/Pure/RAW/ml_compiler0.ML
|
#
414ef271 |
|
01-Mar-2016 |
wenzelm <none@none> |
load secure.ML earlier; eliminated obsolete ml_parse.ML; tuned signature; --HG-- rename : src/Pure/General/secure.ML => src/Pure/RAW/secure.ML
|
#
a580f772 |
|
01-Mar-2016 |
wenzelm <none@none> |
ML debugger support in Pure (again, see 3565c9f407ec);
|
#
3813a04b |
|
28-Feb-2016 |
wenzelm <none@none> |
support only polyml-5.3.0 and polyml-5.6; --HG-- rename : lib/scripts/run-polyml-5.6 => lib/scripts/run-polyml rename : lib/scripts/run-polyml => lib/scripts/run-polyml-5.3.0 rename : src/Pure/ML/ml_statistics_polyml-5.5.0.ML => src/Pure/ML/ml_statistics.ML rename : src/Pure/RAW/exn_trace_polyml-5.5.1.ML => src/Pure/RAW/exn_trace.ML
|
#
72ec9155 |
|
18-Feb-2016 |
wenzelm <none@none> |
unconditional Multithreading; clarified files;
|
#
31979636 |
|
17-Feb-2016 |
wenzelm <none@none> |
tuned;
|
#
e428edb5 |
|
17-Feb-2016 |
wenzelm <none@none> |
clarified file names; --HG-- rename : src/Pure/ML/exn_output_polyml.ML => src/Pure/ML/exn_output.ML rename : src/Pure/ML/exn_properties_polyml.ML => src/Pure/ML/exn_properties.ML rename : src/Pure/ML/ml_compiler_polyml.ML => src/Pure/ML/ml_compiler.ML
|
#
0d72d301 |
|
17-Feb-2016 |
wenzelm <none@none> |
SML/NJ is no longer supported;
|
#
088de97c |
|
06-Dec-2015 |
wenzelm <none@none> |
discontinued intermediate polyml-5.5.3, assuming the coming release will be polyml-5.6; --HG-- rename : src/Pure/ML-Systems/ml_compiler_parameters_polyml-5.5.3.ML => src/Pure/ML-Systems/ml_compiler_parameters_polyml-5.6.ML rename : src/Pure/ML-Systems/ml_debugger_polyml-5.5.3.ML => src/Pure/ML-Systems/ml_debugger_polyml-5.6.ML rename : src/Pure/ML-Systems/ml_parse_tree_polyml-5.5.3.ML => src/Pure/ML-Systems/ml_parse_tree_polyml-5.6.ML rename : src/Pure/ML-Systems/ml_stack_polyml-5.5.3.ML => src/Pure/ML-Systems/ml_stack_polyml-5.6.ML
|
#
7f298548 |
|
20-Nov-2015 |
wenzelm <none@none> |
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b; --HG-- rename : lib/scripts/run-polyml-5.5.3 => lib/scripts/run-polyml-5.6
|
#
d7bdc08d |
|
14-Nov-2015 |
haftmann <none@none> |
separate ML module for interpretation --HG-- extra : rebase_source : 867de135491ddc9e949d932384cce64f60343123
|
#
166c903e |
|
10-Nov-2015 |
wenzelm <none@none> |
clarified modules;
|
#
ebff3653 |
|
03-Nov-2015 |
wenzelm <none@none> |
clarified modules; --HG-- rename : src/Pure/Concurrent/simple_thread.ML => src/Pure/Concurrent/standard_thread.ML rename : src/Pure/Concurrent/simple_thread.scala => src/Pure/Concurrent/standard_thread.scala
|
#
6c5fbbe2 |
|
15-Oct-2015 |
wenzelm <none@none> |
load markdown.ML into Pure;
|
#
2759308d |
|
25-Sep-2015 |
wenzelm <none@none> |
moved remaining display.ML to more_thm.ML;
|
#
a152ef96 |
|
24-Sep-2015 |
wenzelm <none@none> |
more explicit Defs.context: use proper name spaces as far as possible;
|
#
1faee6a8 |
|
17-Aug-2015 |
wenzelm <none@none> |
basic setup for native Windows (RAW session without image);
|
#
29490e14 |
|
17-Aug-2015 |
wenzelm <none@none> |
no ML_debugger support in Pure -- too complicated;
|
#
716a5130 |
|
17-Aug-2015 |
wenzelm <none@none> |
more careful propagation of ML_debugger option to Pure;
|
#
40997677 |
|
17-Aug-2015 |
wenzelm <none@none> |
support for ML files with/without debugger information;
|
#
609b3d38 |
|
17-Aug-2015 |
wenzelm <none@none> |
explicit debug flag for ML compiler;
|
#
8a5bd15f |
|
15-Aug-2015 |
wenzelm <none@none> |
clarified context;
|
#
916d6795 |
|
11-Aug-2015 |
wenzelm <none@none> |
default ML context for forks, e.g. relevant for debugging and toplevel pretty-printing;
|
#
2176dd38 |
|
01-Jul-2015 |
wenzelm <none@none> |
clarified module; --HG-- rename : src/Pure/subgoal.ML => src/Pure/Isar/subgoal.ML
|
#
2c633c9e |
|
01-Apr-2015 |
wenzelm <none@none> |
added command 'experiment';
|
#
43d1f634 |
|
16-Mar-2015 |
wenzelm <none@none> |
tuned protocol -- resolve command positions in ML;
|
#
60673165 |
|
29-Jan-2015 |
wenzelm <none@none> |
tuned bootstrap; --HG-- rename : src/Pure/ML/exn_trace_polyml-5.5.1.ML => src/Pure/ML-Systems/exn_trace_polyml-5.5.1.ML
|
#
14e4298a |
|
14-Jan-2015 |
wenzelm <none@none> |
added Path.decode in ML, in correspondence to Path.encode in Scala;
|
#
94b840f9 |
|
30-Dec-2014 |
wenzelm <none@none> |
explicit message channel for "legacy", which is nonetheless a variant of "warning";
|
#
a30112e7 |
|
29-Dec-2014 |
wenzelm <none@none> |
more toplevel pretty printing;
|
#
fa47d33f |
|
22-Dec-2014 |
wenzelm <none@none> |
separate module Random; proper Synchronized.var;
|
#
7aa8f74c |
|
03-Dec-2014 |
wenzelm <none@none> |
node-specific keywords, with session base syntax as default;
|
#
9bbace2c |
|
29-Nov-2014 |
wenzelm <none@none> |
more abstract type Input.source;
|
#
42d0b505 |
|
26-Nov-2014 |
wenzelm <none@none> |
load simple_thread.ML later, such that it benefits from redefined print_exception_trace;
|
#
0bca046a |
|
21-Nov-2014 |
wenzelm <none@none> |
removed some add-ons from modules that are relevant for the inference kernel;
|
#
c12ca051 |
|
07-Nov-2014 |
wenzelm <none@none> |
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes; plain value Outer_Syntax within theory: parsing requires current theory context; clarified name of Keyword.is_literal according to its semantics; eliminated pointless type Keyword.T; simplified @{command_spec}; clarified bootstrap keywords and syntax: take it as basis instead of side-branch;
|
#
df4ccf3c |
|
05-Nov-2014 |
wenzelm <none@none> |
explicit type Keyword.keywords; tuned signature;
|
#
135cd98c |
|
31-Oct-2014 |
wenzelm <none@none> |
discontinued Isar TTY loop;
|
#
20c48940 |
|
31-Oct-2014 |
wenzelm <none@none> |
discontinued Proof General;
|
#
b961c819 |
|
13-Oct-2014 |
wenzelm <none@none> |
obsolete;
|
#
5bc8503e |
|
13-Oct-2014 |
wenzelm <none@none> |
clarified load order; tuned signature;
|
#
cc7c3cde |
|
29-Sep-2014 |
wenzelm <none@none> |
pro-forma support for polyml-5.5.3 (presently SVN 1960); --HG-- rename : lib/scripts/run-polyml-5.5.2 => lib/scripts/run-polyml-5.5.3 rename : src/Pure/ML-Systems/polyml-5.5.2.ML => src/Pure/ML-Systems/polyml-5.5.3.ML
|
#
cded37ff |
|
21-Aug-2014 |
wenzelm <none@none> |
clarified ML toplevel pp: avoid ML output to be attached to inlined binding positions;
|
#
25a76e63 |
|
19-Aug-2014 |
wenzelm <none@none> |
clarified modules;
|
#
9c577118 |
|
14-Aug-2014 |
wenzelm <none@none> |
tuned signature -- prefer self-contained user-space tool; --HG-- rename : src/Pure/Thy/thm_deps.ML => src/Pure/Tools/thm_deps.ML
|
#
ef6f11e4 |
|
13-Aug-2014 |
wenzelm <none@none> |
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;
|
#
fec16c8c |
|
11-Aug-2014 |
wenzelm <none@none> |
separate module Command_Span: mostly syntactic representation; potentially prover-specific Output_Syntax.parse_spans;
|
#
992a85bc |
|
24-Jul-2014 |
wenzelm <none@none> |
further distinction of Isabelle distribution: alert for identified release candidates;
|
#
bced7572 |
|
06-Apr-2014 |
wenzelm <none@none> |
more source positions;
|
#
ae5ab206 |
|
06-Apr-2014 |
wenzelm <none@none> |
clarified ML bootstrap;
|
#
52dd9fc9 |
|
27-Mar-2014 |
wenzelm <none@none> |
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
|
#
afa08813 |
|
26-Mar-2014 |
wenzelm <none@none> |
tuned comments;
|
#
0142a712 |
|
26-Mar-2014 |
wenzelm <none@none> |
tuned load order;
|
#
2a0d4ed7 |
|
25-Mar-2014 |
wenzelm <none@none> |
proper configuration option "ML_print_depth"; proper ML_exception_trace for HOL-TPTP;
|
#
51dfa318 |
|
20-Mar-2014 |
wenzelm <none@none> |
tuned error, according to "use" in General/secure.ML;
|
#
80e3346f |
|
18-Mar-2014 |
wenzelm <none@none> |
clarified module arrangement; --HG-- rename : src/Pure/System/session.ML => src/Pure/PIDE/session.ML rename : src/Pure/System/session.scala => src/Pure/PIDE/session.scala
|
#
7216e79c |
|
18-Mar-2014 |
wenzelm <none@none> |
clarifed module name; --HG-- rename : src/Pure/Thy/thy_load.ML => src/Pure/PIDE/resources.ML rename : src/Pure/Thy/thy_load.scala => src/Pure/PIDE/resources.scala rename : src/Tools/jEdit/src/jedit_thy_load.scala => src/Tools/jEdit/src/jedit_resources.scala
|
#
a6d4b230 |
|
18-Mar-2014 |
wenzelm <none@none> |
clarified module arrangement; more antiquotations;
|
#
4049b387 |
|
18-Mar-2014 |
wenzelm <none@none> |
clarified modules; more antiquotations for antiquotations;
|
#
9439d0b7 |
|
18-Mar-2014 |
wenzelm <none@none> |
clarified bootstrap process: switch to ML with context and antiquotations earlier;
|
#
42ab7e1e |
|
12-Mar-2014 |
wenzelm <none@none> |
tuned signature -- clarified module name; --HG-- rename : src/Pure/ML/ml_antiquote.ML => src/Pure/ML/ml_antiquotation.ML
|
#
6a1b9023 |
|
11-Mar-2014 |
wenzelm <none@none> |
tables with changes relative to some common base version -- support for efficient join/merge of big global tables with small local updates;
|
#
5c4e6b56 |
|
22-Feb-2014 |
wenzelm <none@none> |
support for completion within the formal context; tuned signature;
|
#
b4b1992a |
|
16-Feb-2014 |
wenzelm <none@none> |
prefer user-space tool within Pure.thy;
|
#
8f9a4da6 |
|
10-Feb-2014 |
wenzelm <none@none> |
seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
|
#
02bf2383 |
|
25-Jan-2014 |
wenzelm <none@none> |
prefer self-contained user-space tool;
|
#
d8d873e7 |
|
17-Jan-2014 |
wenzelm <none@none> |
prefer user-space tool within Pure.thy; --HG-- rename : src/Pure/Thy/rail.ML => src/Pure/Tools/rail.ML
|
#
116fd647 |
|
13-Dec-2013 |
wenzelm <none@none> |
maintain morphism names for diagnostic purposes;
|
#
335df6bd |
|
11-Dec-2013 |
wenzelm <none@none> |
support for polml-5.5.2; support Thread.numPhysicalProcessors of polyml-5.5.2 (according to SVN 1890); clarified max_threads: store plain value internally, reproduce result only on startup, and thus avoid potential system overhead; --HG-- rename : lib/scripts/run-polyml-5.5.1 => lib/scripts/run-polyml-5.5.2
|
#
c31819c3 |
|
16-Nov-2013 |
wenzelm <none@none> |
toplevel function "use" refers to raw ML bootstrap environment;
|
#
f5bedab5 |
|
18-Sep-2013 |
wenzelm <none@none> |
updated to polyml-5.5.1;
|
#
a5c5c033 |
|
18-Sep-2013 |
wenzelm <none@none> |
improved printing of exception trace in Poly/ML 5.5.1;
|
#
ef9ad215 |
|
18-Sep-2013 |
wenzelm <none@none> |
moved module into plain Isabelle/ML user space; --HG-- rename : src/Pure/Isar/rule_insts.ML => src/Pure/Tools/rule_insts.ML
|
#
7b925cab |
|
26-Aug-2013 |
wenzelm <none@none> |
added SHA1 library integrity test, which is invoked at compile time and Isabelle_Process run-time;
|
#
72d291e6 |
|
25-Aug-2013 |
wenzelm <none@none> |
maintain goal forks as part of global execution; tuned;
|
#
acc454db |
|
08-Aug-2013 |
wenzelm <none@none> |
removed unused YXML_Find_Theorems and Legacy_XML_Syntax;
|
#
3b74d05a |
|
05-Aug-2013 |
wenzelm <none@none> |
slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
|
#
2a3c59e7 |
|
01-Aug-2013 |
wenzelm <none@none> |
exception trace for Poly/ML 5.5.1, using regular Isabelle output;
|
#
ff57adaa |
|
30-Jul-2013 |
wenzelm <none@none> |
recovered delay for Document.start_execution (see also 627fb639a2d9), which potentially improves throughput when many consecutive edits arrive;
|
#
42e9b2b9 |
|
30-Jul-2013 |
wenzelm <none@none> |
type theory is purely value-oriented;
|
#
e2266d97 |
|
12-Jul-2013 |
wenzelm <none@none> |
clarified module name; --HG-- rename : src/Pure/PIDE/exec.ML => src/Pure/PIDE/execution.ML
|
#
14f7fd0d |
|
11-Jul-2013 |
wenzelm <none@none> |
global management of command execution fragments; tuned;
|
#
6b45fd7e |
|
10-Jul-2013 |
wenzelm <none@none> |
more abstract message channel;
|
#
d63600df |
|
05-Jul-2013 |
wenzelm <none@none> |
more uniform Counter in ML and Scala;
|
#
96559435 |
|
05-Jul-2013 |
wenzelm <none@none> |
tuned signature; tuned comments;
|
#
328dbab6 |
|
05-Jul-2013 |
wenzelm <none@none> |
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
|
#
97f6c86b |
|
03-Jul-2013 |
wenzelm <none@none> |
tuned signature;
|
#
87953653 |
|
30-Jun-2013 |
wenzelm <none@none> |
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
|
#
b628a60a |
|
27-Jun-2013 |
wenzelm <none@none> |
manage option "proofs" within theory context -- with minor overhead for primitive inferences;
|
#
15932c08 |
|
28-May-2013 |
wenzelm <none@none> |
explicit support for type annotations within printed syntax trees; eliminated obsolete show_free_types;
|
#
2bfa0899 |
|
25-May-2013 |
haftmann <none@none> |
tuned structure
|
#
366e8a54 |
|
17-May-2013 |
wenzelm <none@none> |
proper option quick_and_dirty;
|
#
edad993e |
|
17-May-2013 |
wenzelm <none@none> |
event timer as separate service thread;
|
#
369d0e7b |
|
15-May-2013 |
wenzelm <none@none> |
moved files; --HG-- rename : src/Pure/ProofGeneral/proof_general.ML => src/Pure/Tools/proof_general.ML rename : src/Pure/ProofGeneral/proof_general_pure.ML => src/Pure/Tools/proof_general_pure.ML
|
#
42c02b01 |
|
15-May-2013 |
wenzelm <none@none> |
maintain ProofGeneral preferences within ProofGeneral module; initialize Isabelle/Pure preferences within normal user space (with antiquotations); tuned;
|
#
cb7d30c4 |
|
15-May-2013 |
wenzelm <none@none> |
just one ProofGeneral module; --HG-- rename : src/Pure/ProofGeneral/proof_general_emacs.ML => src/Pure/ProofGeneral/proof_general.ML
|
#
dbc86b79 |
|
14-May-2013 |
wenzelm <none@none> |
simplified modules and exceptions;
|
#
ae53e370 |
|
13-May-2013 |
wenzelm <none@none> |
more direct output of remaining PGIP rudiments;
|
#
82d90995 |
|
13-May-2013 |
wenzelm <none@none> |
removed obsolete PGIP material;
|
#
d87ed72a |
|
12-May-2013 |
wenzelm <none@none> |
support for system options as context-sensitive config options;
|
#
f93d0093 |
|
11-May-2013 |
wenzelm <none@none> |
removed redundant modules;
|
#
df6ab650 |
|
03-Apr-2013 |
wenzelm <none@none> |
additional timing status for implicitly forked terminal proofs -- proper accounting for interactive Timing dockable etc.;
|
#
c0c9ada8 |
|
27-Mar-2013 |
wenzelm <none@none> |
tuned signature and module arrangement; --HG-- rename : src/Pure/Isar/skip_proof.ML => src/Pure/skip_proof.ML
|
#
bb8f4fbd |
|
25-Feb-2013 |
wenzelm <none@none> |
tuned order of modules;
|
#
ec3ad7b1 |
|
16-Jan-2013 |
wenzelm <none@none> |
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
|
#
c2be72f4 |
|
09-Jan-2013 |
wenzelm <none@none> |
recovered buffered sockets from 11f622794ad6 -- requires Poly/ML 5.5.x;
|
#
7c42c564 |
|
07-Jan-2013 |
wenzelm <none@none> |
slightly odd duplication of Pure options for Proof General (amending cb5cdbb645cd);
|
#
8bcf9439 |
|
02-Jan-2013 |
wenzelm <none@none> |
moved files; --HG-- rename : src/Pure/System/build.ML => src/Pure/Tools/build.ML rename : src/Pure/System/build.scala => src/Pure/Tools/build.scala rename : src/Pure/System/build_dialog.scala => src/Pure/Tools/build_dialog.scala
|
#
ac81bbc5 |
|
13-Dec-2012 |
wenzelm <none@none> |
identify dialogs via official serial and maintain as result message; clarified Protocol.is_inlined: suppress result/tracing/state messages uniformly; cumulate_markup/select_markup depending on command state; explicit Rendering.output_messages; tuned source structure;
|
#
e227f727 |
|
12-Dec-2012 |
wenzelm <none@none> |
support dialog via document content;
|
#
19b3945c |
|
10-Dec-2012 |
wenzelm <none@none> |
generalized notion of active area, where sendback is just one application; some support for graphview via active area; --HG-- rename : src/Pure/PIDE/sendback.ML => src/Pure/PIDE/active.ML rename : src/Tools/jEdit/src/sendback.scala => src/Tools/jEdit/src/active.scala
|
#
4af3fd10 |
|
28-Nov-2012 |
wenzelm <none@none> |
some support for ML runtime statistics;
|
#
65822759 |
|
26-Nov-2012 |
wenzelm <none@none> |
clarified status of Legacy_XML_Syntax, despite lack of Proofterm_XML; --HG-- rename : src/Pure/Tools/xml_syntax.ML => src/Pure/Tools/legacy_xml_syntax.ML
|
#
95d64a2f |
|
25-Nov-2012 |
wenzelm <none@none> |
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
|
#
4b9ea399 |
|
22-Nov-2012 |
wenzelm <none@none> |
more abstract Sendback operations, with explicit id/exec_id properties; purge result messages (again), cf. db58490a68ac, 7b61a539721e;
|
#
997022e7 |
|
16-Oct-2012 |
wenzelm <none@none> |
more friendly handling of Pure.thy bootstrap errors;
|
#
53ab0ad7 |
|
25-Sep-2012 |
wenzelm <none@none> |
separate module Graph_Display; tuned signature;
|
#
231425cc |
|
25-Sep-2012 |
wenzelm <none@none> |
added graph encode/decode operations; tuned signature;
|
#
e0ddc788 |
|
31-Aug-2012 |
wenzelm <none@none> |
more informative error message from failed goal forks (violating old-style TTY protocol!);
|
#
afa905a5 |
|
28-Aug-2012 |
wenzelm <none@none> |
discontinued centralistic changelog;
|
#
45aa577d |
|
26-Aug-2012 |
wenzelm <none@none> |
theory def/ref position reports, which enable hyperlinks etc.; more official header command parsing;
|
#
8773fae9 |
|
21-Aug-2012 |
wenzelm <none@none> |
clarified bootstrapping of Pure;
|
#
7cb377ba |
|
21-Aug-2012 |
wenzelm <none@none> |
more standard Thy_Load.check_thy for Pure.thy, relying on its header; pass uses and keywords from Thy_Load.check_thy to Thy_Info.load_thy; clarified 'ML_file' wrt. Thy_Load.require/provide, which is also relevant for Thy_Load.all_current;
|
#
b912e3db |
|
20-Aug-2012 |
wenzelm <none@none> |
some support for inlining file content into outer syntax token language;
|
#
bfa67b35 |
|
11-Aug-2012 |
wenzelm <none@none> |
clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup;
|
#
0166ea98 |
|
07-Aug-2012 |
wenzelm <none@none> |
simplified Pure bootstrap -- separate pure_setup.ML was required for Alice/ML at some point;
|
#
ba8c61f1 |
|
05-Aug-2012 |
wenzelm <none@none> |
prefer general Command_Line.tool wrapper (cf. Scala version);
|
#
4dd7a184 |
|
01-Aug-2012 |
wenzelm <none@none> |
more official command specifications, including source position;
|
#
f326a9c6 |
|
01-Aug-2012 |
wenzelm <none@none> |
more standard bootstrapping of Pure outer syntax;
|
#
73c44c38 |
|
23-Jul-2012 |
wenzelm <none@none> |
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
|
#
19f189d0 |
|
21-Jul-2012 |
wenzelm <none@none> |
some actual build function on ML side; further imitation of "usedir" shell script;
|
#
1885ca4b |
|
24-May-2012 |
wenzelm <none@none> |
simplified Poly/ML setup -- 5.3.0 is now the common base-line; --HG-- rename : src/Pure/ML-Systems/compiler_polyml-5.3.ML => src/Pure/ML-Systems/compiler_polyml.ML rename : src/Pure/ML/install_pp_polyml-5.3.ML => src/Pure/ML/install_pp_polyml.ML rename : src/Pure/ML/ml_compiler_polyml-5.3.ML => src/Pure/ML/ml_compiler_polyml.ML
|
#
ca40ff3e |
|
24-May-2012 |
wenzelm <none@none> |
discontinued support for Poly/ML 5.2.1;
|
#
936dcace |
|
27-Apr-2012 |
wenzelm <none@none> |
made Context_Position independent from Config;
|
#
808b544d |
|
04-Apr-2012 |
wenzelm <none@none> |
separate module for prover command execution;
|
#
9aa075ed |
|
20-Mar-2012 |
wenzelm <none@none> |
basic support for bundled declarations;
|
#
0c7f4273 |
|
01-Dec-2011 |
wenzelm <none@none> |
clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover; --HG-- rename : src/Pure/PIDE/isabelle_document.ML => src/Pure/PIDE/protocol.ML rename : src/Pure/PIDE/isabelle_document.scala => src/Pure/PIDE/protocol.scala
|
#
23e33658 |
|
29-Nov-2011 |
wenzelm <none@none> |
clarified modules; --HG-- rename : src/Pure/PIDE/isar_document.ML => src/Pure/PIDE/isabelle_document.ML rename : src/Pure/PIDE/isar_document.scala => src/Pure/PIDE/isabelle_document.scala
|
#
6ff6ff4b |
|
29-Nov-2011 |
wenzelm <none@none> |
rearranged files; --HG-- rename : src/Pure/General/isabelle_markup.ML => src/Pure/PIDE/isabelle_markup.ML rename : src/Pure/General/isabelle_markup.scala => src/Pure/PIDE/isabelle_markup.scala rename : src/Pure/General/markup.ML => src/Pure/PIDE/markup.ML rename : src/Pure/General/markup.scala => src/Pure/PIDE/markup.scala
|
#
99fd6f8e |
|
28-Nov-2011 |
wenzelm <none@none> |
separate module for concrete Isabelle markup; --HG-- rename : src/Pure/General/markup.ML => src/Pure/General/isabelle_markup.ML rename : src/Pure/General/markup.scala => src/Pure/General/isabelle_markup.scala
|
#
cfe58b3e |
|
19-Nov-2011 |
wenzelm <none@none> |
added ML antiquotation @{attributes};
|
#
485ee157 |
|
23-Sep-2011 |
wenzelm <none@none> |
discontinued stream-based Socket_IO, which causes too many problems with Poly/ML and SML/NJ (reverting major parts of 5c0b0d67f9b1);
|
#
ac86da98 |
|
22-Sep-2011 |
wenzelm <none@none> |
abstract System_Channel in ML (cf. Scala version); back to TextIO for fifo, which is more stable in Poly/ML 5.4.x; explicit block buffering -- BinIO might be subject to old Poly/ML defaults;
|
#
93a3c349 |
|
21-Sep-2011 |
wenzelm <none@none> |
slightly more general Socket_IO as part of Pure; --HG-- rename : src/Tools/WWW_Find/socket_util.ML => src/Tools/WWW_Find/server_socket.ML
|
#
ec656bb9 |
|
04-Sep-2011 |
wenzelm <none@none> |
moved XML/YXML to src/Pure/PIDE; tuned comments; --HG-- rename : src/Pure/General/xml.ML => src/Pure/PIDE/xml.ML rename : src/Pure/General/xml.scala => src/Pure/PIDE/xml.scala rename : src/Pure/General/yxml.ML => src/Pure/PIDE/yxml.ML rename : src/Pure/General/yxml.scala => src/Pure/PIDE/yxml.scala
|
#
63f2d324 |
|
27-Aug-2011 |
wenzelm <none@none> |
explicit markup for legacy warnings;
|
#
fc107ff5 |
|
17-Aug-2011 |
wenzelm <none@none> |
more systematic handling of parallel exceptions; distinguish exception concatanation EXCEPTIONS from parallel Par_Exn;
|
#
424e1a73 |
|
13-Aug-2011 |
wenzelm <none@none> |
provide node header via Scala layer; clarified node edit Clear: retain header information; run_command: node info via document model, error handling within transaction; node names without ".thy" suffix, to coincide with traditional theory loader treatment;
|
#
68ed89ae |
|
10-Aug-2011 |
wenzelm <none@none> |
old term operations are legacy;
|
#
2b741c8a |
|
10-Aug-2011 |
wenzelm <none@none> |
moved old code generator to src/Tools/; --HG-- rename : src/Pure/codegen.ML => src/Tools/codegen.ML
|
#
4bdbfe94 |
|
08-Aug-2011 |
wenzelm <none@none> |
modernized file proof_checker.ML; --HG-- rename : src/Pure/Proof/proofchecker.ML => src/Pure/Proof/proof_checker.ML
|
#
0f726e27 |
|
23-Jul-2011 |
wenzelm <none@none> |
explicit structure ML_System; tunned ML bootstrap;
|
#
d6f37a48 |
|
16-Jul-2011 |
wenzelm <none@none> |
moved bash operations to Isabelle_System (cf. Scala version);
|
#
2aaf4089 |
|
16-Jul-2011 |
wenzelm <none@none> |
more general bash_process, which allows to terminate background processes as well;
|
#
ef30167b |
|
13-Jul-2011 |
wenzelm <none@none> |
recovered some runtime sharing from d6b6c74a8bcf, without the global memory bottleneck;
|
#
628ac0ab |
|
13-Jul-2011 |
wenzelm <none@none> |
sub-structural sharing after Syntax.check phase, with global interning of logical entities (the latter is relevant when bypassing default parsing via YXML); minor tuning;
|
#
de0a3ec5 |
|
13-Jul-2011 |
wenzelm <none@none> |
XML.pretty with depth limit;
|
#
593bd456 |
|
12-Jul-2011 |
wenzelm <none@none> |
discontinued obsolete Isabelle_Syntax and Parse_Value -- superseded by Outer_Syntax.quote_string and XML.Encode, Term_XML.Encode etc.;
|
#
a33bb41d |
|
12-Jul-2011 |
wenzelm <none@none> |
tuned XML modules;
|
#
b960762e |
|
11-Jul-2011 |
wenzelm <none@none> |
JVM method invocation service via Scala layer;
|
#
8191600e |
|
11-Jul-2011 |
wenzelm <none@none> |
some support for raw messages, which bypass standard Symbol/YXML decoding; tuned signature;
|
#
2280ab9c |
|
10-Jul-2011 |
wenzelm <none@none> |
XML data representation of lambda terms;
|
#
56106872 |
|
08-Jul-2011 |
wenzelm <none@none> |
moved Outer_Syntax.load_thy to Thy_Load.load_thy; tuned signatures; tuned module dependencies;
|
#
e077a27a |
|
06-Jul-2011 |
wenzelm <none@none> |
prefer Synchronized.var;
|
#
7864f97c |
|
29-Jun-2011 |
wenzelm <none@none> |
print Path.T with some markup;
|
#
2fb28d40 |
|
25-Jun-2011 |
wenzelm <none@none> |
clarified Binding.pretty/print: no quotes, only markup -- Binding.str_of is rendered obsolete;
|
#
f681e41a |
|
30-Apr-2011 |
wenzelm <none@none> |
railroad diagrams in LaTeX as document antiquotation;
|
#
d72a8bc3 |
|
19-Apr-2011 |
wenzelm <none@none> |
split Type_Infer into early and late part, after Proof_Context; added Type_Infer_Context.const_sorts option, which allows NBE to use regular Syntax.check_term;
|
#
dbff82ee |
|
18-Apr-2011 |
wenzelm <none@none> |
simplified pretty printing context, which is only required for certain kernel operations; disentangled dependencies of structure Pretty;
|
#
79aa2752 |
|
17-Apr-2011 |
wenzelm <none@none> |
provide structure Syntax early (before structure Type), back-patch check/uncheck later;
|
#
6052557e |
|
15-Apr-2011 |
wenzelm <none@none> |
tuned signature, disentangled dependencies;
|
#
ecc6df14 |
|
08-Apr-2011 |
wenzelm <none@none> |
discontinued special treatment of structure Syntax_Ext (formerly Syn_Ext); clarified Syntax.root; --HG-- rename : src/Pure/Syntax/syn_ext.ML => src/Pure/Syntax/syntax_ext.ML
|
#
1c017ad4 |
|
08-Apr-2011 |
wenzelm <none@none> |
explicit structure Syntax_Trans; discontinued old-style constrainAbsC; --HG-- rename : src/Pure/Syntax/syn_trans.ML => src/Pure/Syntax/syntax_trans.ML
|
#
3aaf94cf |
|
06-Apr-2011 |
wenzelm <none@none> |
separate structure Term_Position; dismantled remains of structure Type_Ext;
|
#
a4141037 |
|
06-Apr-2011 |
wenzelm <none@none> |
renamed Standard_Syntax to Syntax_Phases; --HG-- rename : src/Pure/Syntax/standard_syntax.ML => src/Pure/Syntax/syntax_phases.ML
|
#
f9091c3b |
|
05-Apr-2011 |
wenzelm <none@none> |
separate module for standard implementation of inner syntax operations;
|
#
18667ce2 |
|
05-Apr-2011 |
wenzelm <none@none> |
moved Isar/local_syntax.ML to Syntax/local_syntax.ML; --HG-- rename : src/Pure/Isar/local_syntax.ML => src/Pure/Syntax/local_syntax.ML
|
#
8b04ee36 |
|
20-Mar-2011 |
wenzelm <none@none> |
structure Timing: covers former start_timing/end_timing and Output.timeit etc; explicit Timing.message function; eliminated Output.timing flag, cf. Toplevel.timing; tuned;
|
#
8128d8be |
|
08-Feb-2011 |
wenzelm <none@none> |
discontinued support for Poly/ML 5.2, which was the last version without proper multithreading and TimeLimit implementation;
|
#
b621a820 |
|
05-Feb-2011 |
wenzelm <none@none> |
clarified bootstrapping of structure TimeLimit; --HG-- rename : src/Pure/ML-Systems/time_limit.ML => src/Pure/Concurrent/time_limit_dummy.ML
|
#
3272990d |
|
17-Dec-2010 |
wenzelm <none@none> |
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning; --HG-- rename : src/Pure/meta_simplifier.ML => src/Pure/raw_simplifier.ML
|
#
7e4d77d9 |
|
27-Nov-2010 |
wenzelm <none@none> |
removed bash from ML system bootstrap, and past the Secure ML barrier; --HG-- rename : src/Pure/ML-Systems/bash.ML => src/Pure/Concurrent/bash_sequential.ML
|
#
1bfcb69d |
|
27-Nov-2010 |
wenzelm <none@none> |
more explicit Isabelle_System operations;
|
#
308c65f5 |
|
20-Sep-2010 |
wenzelm <none@none> |
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only; --HG-- rename : src/Pure/pure_thy.ML => src/Pure/global_theory.ML
|
#
c79986ca |
|
17-Sep-2010 |
wenzelm <none@none> |
simplified some internal flags using Config.T instead of full-blown Proof_Data;
|
#
bb93d4cb |
|
12-Sep-2010 |
wenzelm <none@none> |
load type_infer.ML later -- proper context for Type_Infer.infer_types; renamed Type_Infer.polymorphicT to Type.mark_polymorphic;
|
#
3a28d1f8 |
|
08-Sep-2010 |
haftmann <none@none> |
removed ancient constdefs command
|
#
1f8a280f |
|
01-Sep-2010 |
wenzelm <none@none> |
eliminated obsolete old-style goal stack package, which was considered the main Isabelle user interface at some point;
|
#
087b560b |
|
30-Aug-2010 |
wenzelm <none@none> |
more careful treatment of nested multi-exceptions, collapsing cumulatively empty list to Interrupt;
|
#
2c233751 |
|
22-Aug-2010 |
wenzelm <none@none> |
recognize more "smlnj" variants;
|
#
fe660f6f |
|
18-Aug-2010 |
wenzelm <none@none> |
moved Isar_Document to Pure/PIDE; --HG-- rename : src/Pure/System/isar_document.ML => src/Pure/PIDE/isar_document.ML rename : src/Pure/System/isar_document.scala => src/Pure/PIDE/isar_document.scala
|
#
32932479 |
|
17-Aug-2010 |
wenzelm <none@none> |
discontinued support for Poly/ML 5.0 and 5.1 versions;
|
#
b4bfba40 |
|
17-Aug-2010 |
wenzelm <none@none> |
added functor Linear_Set, based on former adhoc structures in document.ML; Linear_Set.delete_after (ML): actually delete table entries; Scala Linear_Set: clarified exceptions, according to ML version; simplified Document.node using Linear_Set; ML Document.edit: refer to start via NONE instead of no_id, according to Scala version;
|
#
ab03f51d |
|
15-Aug-2010 |
wenzelm <none@none> |
more explicit / functional ML version of document model; tuned;
|
#
db9fb28f |
|
14-Aug-2010 |
wenzelm <none@none> |
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
|
#
8c728df4 |
|
11-Aug-2010 |
haftmann <none@none> |
more convenient split of class modules: class and class_declaration --HG-- rename : src/Pure/Isar/class_target.ML => src/Pure/Isar/class.ML rename : src/Pure/Isar/class.ML => src/Pure/Isar/class_declaration.ML
|
#
2fa88f89 |
|
11-Aug-2010 |
haftmann <none@none> |
renamed Theory_Target to the more appropriate Named_Target --HG-- rename : src/Pure/Isar/theory_target.ML => src/Pure/Isar/named_target.ML
|
#
2721aef6 |
|
10-Aug-2010 |
haftmann <none@none> |
moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
|
#
89ca23c2 |
|
10-Aug-2010 |
wenzelm <none@none> |
Isar_Document command input via native Isabelle_Process commands, using YXML and XML_Data representation;
|
#
d908aaf3 |
|
10-Aug-2010 |
wenzelm <none@none> |
type XML.body as basic data representation language; tuned;
|
#
8edde8db |
|
10-Aug-2010 |
haftmann <none@none> |
split off structure Generic_Target into separate file
|
#
ef07e3b5 |
|
05-Aug-2010 |
wenzelm <none@none> |
simplified/refined document model: collection of named nodes, without proper dependencies yet; moved basic type definitions for ids and edits from Isar_Document to Document; removed begin_document/end_document for now -- nodes emerge via edits; edits refer to named nodes explicitly;
|
#
17192db8 |
|
23-Jul-2010 |
wenzelm <none@none> |
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state; theory loader: reduced warnings -- thy database can be bypassed in certain situations; Proof/Local_Theory.propagate_ml_env; ML use function: propagate ML environment as well; pervasive type generic_theory;
|
#
a72bbb73 |
|
12-Jul-2010 |
wenzelm <none@none> |
removed legacy aliases;
|
#
7d3b137c |
|
01-Jun-2010 |
wenzelm <none@none> |
uniform ML environment setup for Isar and PG;
|
#
f67c911e |
|
01-Jun-2010 |
wenzelm <none@none> |
keep structure ThyLoad for the sake of Proof General;
|
#
c25c5530 |
|
31-May-2010 |
wenzelm <none@none> |
modernized some structure names, keeping a few legacy aliases;
|
#
5a9d2980 |
|
27-May-2010 |
wenzelm <none@none> |
renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
|
#
b7e81c3e |
|
27-May-2010 |
wenzelm <none@none> |
renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
|
#
a7549876 |
|
17-May-2010 |
wenzelm <none@none> |
do not open Legacy by default;
|
#
90cf947c |
|
17-May-2010 |
wenzelm <none@none> |
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time; eliminated slightly odd alias structure T; --HG-- rename : src/Pure/Isar/outer_lex.ML => src/Pure/Isar/token.ML
|
#
8bd38908 |
|
17-May-2010 |
wenzelm <none@none> |
centralized legacy aliases;
|
#
13dae07e |
|
15-May-2010 |
wenzelm <none@none> |
renamed structure SpecParse to Parse_Spec, keeping the old name as alias for some time; --HG-- rename : src/Pure/Isar/spec_parse.ML => src/Pure/Isar/parse_spec.ML
|
#
b6eb9785 |
|
15-May-2010 |
wenzelm <none@none> |
renamed structure ValueParse to Parse_Value; eliminated old-style structure alias V; --HG-- rename : src/Pure/Isar/value_parse.ML => src/Pure/Isar/parse_value.ML
|
#
8dc785d0 |
|
15-May-2010 |
wenzelm <none@none> |
renamed structure OuterKeyword to Keyword and OuterParse to Parse, keeping the old names as legacy aliases for some time; --HG-- rename : src/Pure/Isar/outer_keyword.ML => src/Pure/Isar/keyword.ML rename : src/Pure/Isar/outer_parse.ML => src/Pure/Isar/parse.ML
|
#
4f42972e |
|
24-Mar-2010 |
wenzelm <none@none> |
slightly more logical bootstrap order -- also helps to sort out proof terms extension;
|
#
f36452c7 |
|
09-Mar-2010 |
wenzelm <none@none> |
added ProofContext.tsig_of -- proforma version for local name space only, not logical content; added ProofContext.read_type_name_proper; localized ProofContext.read_class/read_arity/cert_arity; localized ProofContext.class_space/type_space etc.;
|
#
4eba7f12 |
|
07-Mar-2010 |
wenzelm <none@none> |
Digesting strings according to SHA-1.
|
#
8a4fcc92 |
|
06-Mar-2010 |
wenzelm <none@none> |
separate structure Typedecl;
|
#
c6364819 |
|
06-Feb-2010 |
wenzelm <none@none> |
explicit representation of single-assignment variables;
|
#
33fd6992 |
|
09-Nov-2009 |
wenzelm <none@none> |
setup for official Poly/ML 5.3.0, which is now the default; --HG-- rename : src/Pure/ML-Systems/polyml.ML => src/Pure/ML-Systems/polyml-5.2.ML rename : src/Pure/ML-Systems/polyml-experimental.ML => src/Pure/ML-Systems/polyml.ML
|
#
4bd2d512 |
|
01-Nov-2009 |
wenzelm <none@none> |
Rules that characterize functional/relational specifications.
|
#
59595614 |
|
01-Oct-2009 |
wenzelm <none@none> |
Concurrently cached values.
|
#
fae78383 |
|
01-Oct-2009 |
wenzelm <none@none> |
more official status of sequential implementations; tuned; --HG-- rename : src/Pure/Concurrent/par_list_dummy.ML => src/Pure/Concurrent/par_list_sequential.ML rename : src/Pure/Concurrent/synchronized_dummy.ML => src/Pure/Concurrent/synchronized_sequential.ML
|
#
7599bf5b |
|
01-Oct-2009 |
wenzelm <none@none> |
separate concurrent/sequential versions of lazy evaluation; lazy based on future avoids wasted evaluations; --HG-- rename : src/Pure/General/lazy.ML => src/Pure/Concurrent/lazy.ML
|
#
b9d789f1 |
|
29-Sep-2009 |
wenzelm <none@none> |
explicit indication of Unsynchronized.ref;
|
#
1f0fb01e |
|
28-Sep-2009 |
wenzelm <none@none> |
Dummy version of state variables -- plain refs for sequential access.
|
#
39b718f9 |
|
11-Aug-2009 |
wenzelm <none@none> |
clarified situation about unidentified repository versions -- in a distributed setting there is not "the" repository;
|
#
db497781 |
|
25-Jul-2009 |
wenzelm <none@none> |
renamed structure Display_Goal to Goal_Display; --HG-- rename : src/Pure/display_goal.ML => src/Pure/goal_display.ML
|
#
abfccda1 |
|
23-Jul-2009 |
wenzelm <none@none> |
renamed Pure/tctical.ML to Pure/tactical.ML; --HG-- rename : src/Pure/tctical.ML => src/Pure/tactical.ML
|
#
0fb8f22f |
|
20-Jul-2009 |
wenzelm <none@none> |
moved pretty_goals etc. to Display_Goal (required by tracing tacticals); load display.ML after assumption.ML, to accomodate proper contextual theorem display;
|
#
d1eabe68 |
|
16-Jul-2009 |
wenzelm <none@none> |
Support for copy-avoiding functions on pure values, at the cost of readability.
|
#
fb305543 |
|
06-Jun-2009 |
wenzelm <none@none> |
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
|
#
517206ba |
|
04-Jun-2009 |
wenzelm <none@none> |
just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources;
|
#
27ce9a28 |
|
02-Jun-2009 |
wenzelm <none@none> |
early setup of secure operations (again, cf. deddd77112b7) -- NB: fix_ints is required for bootstrap; late setup of ML_Env and ML_Compiler;
|
#
659f2fa7 |
|
01-Jun-2009 |
wenzelm <none@none> |
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
|
#
73fb2465 |
|
01-Jun-2009 |
wenzelm <none@none> |
slightly later setup of ML and secure operations;
|
#
c9af8b52 |
|
01-Apr-2009 |
wenzelm <none@none> |
tuned comments;
|
#
ef19e570 |
|
22-Mar-2009 |
wenzelm <none@none> |
ML/ml_test.ML: test of advanced ML compiler invocation in Poly/ML 5.3;
|
#
ed733ae1 |
|
17-Mar-2009 |
wenzelm <none@none> |
turned structure NetRules into general Item_Net, which is loaded earlier; --HG-- rename : src/Pure/Isar/net_rules.ML => src/Pure/item_net.ML
|
#
121e82fb |
|
04-Mar-2009 |
blanchet <none@none> |
Merge.
|
#
0003e9ac |
|
28-Feb-2009 |
wenzelm <none@none> |
moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands); --HG-- rename : src/Pure/Tools/isabelle_process.ML => src/Pure/System/isabelle_process.ML rename : src/Pure/Tools/isabelle_process.scala => src/Pure/System/isabelle_process.scala rename : src/Pure/Isar/isar.ML => src/Pure/System/isar.ML rename : src/Pure/Isar/session.ML => src/Pure/System/session.ML
|
#
e154e805 |
|
31-Dec-2008 |
wenzelm <none@none> |
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML); tuned signature of structure Term;
|
#
2bfb8e00 |
|
30-Dec-2008 |
wenzelm <none@none> |
added old_term.ML;
|
#
4423519d |
|
15-Dec-2008 |
haftmann <none@none> |
moved value.ML to src/Tools
|
#
e01ddee4 |
|
04-Dec-2008 |
haftmann <none@none> |
cleaned up binding module and related code
|
#
f21befe1 |
|
03-Dec-2008 |
haftmann <none@none> |
made repository layout more coherent with logical distribution structure; stripped some $Id$s --HG-- rename : src/HOL/Library/Code_Message.thy => src/HOL/Code_Message.thy rename : src/HOL/Complex/Complex.thy => src/HOL/Complex.thy rename : src/HOL/Complex/Complex_Main.thy => src/HOL/Complex_Main.thy rename : src/HOL/Real/ContNotDenum.thy => src/HOL/ContNotDenum.thy rename : src/HOL/Hyperreal/Deriv.thy => src/HOL/Deriv.thy rename : src/HOL/Hyperreal/Fact.thy => src/HOL/Fact.thy rename : src/HOL/Hyperreal/FrechetDeriv.thy => src/HOL/FrechetDeriv.thy rename : src/HOL/Library/GCD.thy => src/HOL/GCD.thy rename : src/HOL/Hyperreal/Integration.thy => src/HOL/Integration.thy rename : src/HOL/Real/Float.thy => src/HOL/Library/Float.thy rename : src/HOL/Hyperreal/Lim.thy => src/HOL/Lim.thy rename : src/HOL/Hyperreal/Ln.thy => src/HOL/Ln.thy rename : src/HOL/Hyperreal/Log.thy => src/HOL/Log.thy rename : src/HOL/Real/Lubs.thy => src/HOL/Lubs.thy rename : src/HOL/Hyperreal/MacLaurin.thy => src/HOL/MacLaurin.thy rename : src/HOL/Hyperreal/NthRoot.thy => src/HOL/NthRoot.thy rename : src/HOL/Library/Order_Relation.thy => src/HOL/Order_Relation.thy rename : src/HOL/Real/PReal.thy => src/HOL/PReal.thy rename : src/HOL/Library/Parity.thy => src/HOL/Parity.thy rename : src/HOL/Real/RComplete.thy => src/HOL/RComplete.thy rename : src/HOL/Real/Rational.thy => src/HOL/Rational.thy rename : src/HOL/Real/Real.thy => src/HOL/Real.thy rename : src/HOL/Real/RealDef.thy => src/HOL/RealDef.thy rename : src/HOL/Real/RealPow.thy => src/HOL/RealPow.thy rename : src/HOL/Hyperreal/Series.thy => src/HOL/Series.thy rename : src/HOL/Hyperreal/Taylor.thy => src/HOL/Taylor.thy rename : src/HOL/arith_data.ML => src/HOL/Tools/arith_data.ML rename : src/HOL/Real/float_arith.ML => src/HOL/Tools/float_arith.ML rename : src/HOL/Real/float_syntax.ML => src/HOL/Tools/float_syntax.ML rename : src/HOL/hologic.ML => src/HOL/Tools/hologic.ML rename : src/HOL/int_arith1.ML => src/HOL/Tools/int_arith.ML rename : src/HOL/int_factor_simprocs.ML => src/HOL/Tools/int_factor_simprocs.ML rename : src/HOL/nat_simprocs.ML => src/HOL/Tools/nat_simprocs.ML rename : src/HOL/Real/rat_arith.ML => src/HOL/Tools/rat_arith.ML rename : src/HOL/Real/real_arith.ML => src/HOL/Tools/real_arith.ML rename : src/HOL/simpdata.ML => src/HOL/Tools/simpdata.ML rename : src/HOL/Hyperreal/Transcendental.thy => src/HOL/Transcendental.thy rename : src/HOL/Library/RType.thy => src/HOL/Typerep.thy rename : src/HOL/Library/Univ_Poly.thy => src/HOL/Univ_Poly.thy rename : src/HOL/Complex/ex/Arithmetic_Series_Complex.thy => src/HOL/ex/Arithmetic_Series_Complex.thy rename : src/HOL/Complex/ex/BigO_Complex.thy => src/HOL/ex/BigO_Complex.thy rename : src/HOL/Complex/ex/HarmonicSeries.thy => src/HOL/ex/HarmonicSeries.thy rename : src/HOL/Complex/ex/MIR.thy => src/HOL/ex/MIR.thy rename : src/HOL/Complex/ex/ReflectedFerrack.thy => src/HOL/ex/ReflectedFerrack.thy rename : src/HOL/Complex/ex/Sqrt.thy => src/HOL/ex/Sqrt.thy rename : src/HOL/Complex/ex/Sqrt_Script.thy => src/HOL/ex/Sqrt_Script.thy rename : src/HOL/Complex/ex/linrtac.ML => src/HOL/ex/linrtac.ML rename : src/HOL/Complex/ex/mirtac.ML => src/HOL/ex/mirtac.ML rename : src/Pure/Tools/quickcheck.ML => src/Tools/quickcheck.ML rename : src/Pure/Tools/value.ML => src/Tools/value.ML
|
#
8e16c387 |
|
29-Sep-2008 |
wenzelm <none@none> |
added context_position.ML;
|
#
7ab10044 |
|
22-Sep-2008 |
wenzelm <none@none> |
removed deriv.ML which is now incorporated into thm.ML;
|
#
a269eae7 |
|
18-Sep-2008 |
wenzelm <none@none> |
added deriv.ML: Abstract derivations based on raw proof terms.
|
#
40d00608 |
|
11-Sep-2008 |
wenzelm <none@none> |
separate Concurrent/ROOT.ML;
|
#
9d507e0c |
|
08-Sep-2008 |
wenzelm <none@none> |
added Concurrent/task_queue.ML;
|
#
a36f6ba4 |
|
07-Sep-2008 |
wenzelm <none@none> |
added Concurrent/future.ML;
|
#
aae33f87 |
|
04-Sep-2008 |
wenzelm <none@none> |
added Concurrent/mailbox.ML;
|
#
d978e399 |
|
04-Sep-2008 |
wenzelm <none@none> |
added Concurrent/schedule.ML;
|
#
97c1e76b |
|
17-Jul-2008 |
wenzelm <none@none> |
structure Distribution: swapped default for is_official;
|
#
57126332 |
|
11-Jul-2008 |
haftmann <none@none> |
tuned order
|
#
316f24ea |
|
18-Jun-2008 |
wenzelm <none@none> |
load type_infer.ML after Syntax module;
|
#
88f2efa1 |
|
18-Jun-2008 |
wenzelm <none@none> |
load proof term operations later;
|
#
77ac43c6 |
|
12-Apr-2008 |
wenzelm <none@none> |
removed obsolete compress.ML
|
#
e2ff9e86 |
|
15-Mar-2008 |
wenzelm <none@none> |
removed obsolete fact_index.ML; added facts.ML;
|
#
e2bcc450 |
|
25-Feb-2008 |
wenzelm <none@none> |
tuned structure Distribution;
|
#
3ff73c5f |
|
21-Feb-2008 |
wenzelm <none@none> |
more elaborate structure Distribution (filled-in by makedist);
|
#
5797a932 |
|
24-Jan-2008 |
wenzelm <none@none> |
removed obsolete context_position.ML (superseded by Position.thread_data);
|
#
439ba449 |
|
31-Dec-2007 |
wenzelm <none@none> |
removed obsolete banner;
|
#
7124ec6c |
|
28-Nov-2007 |
wenzelm <none@none> |
removed typedecl.ML (cf. object_logic.ML);
|
#
daec5a07 |
|
23-Nov-2007 |
haftmann <none@none> |
separated typedecl module, providing typedecl command with interpretation
|
#
7552cb77 |
|
11-Oct-2007 |
wenzelm <none@none> |
load axclass.ML before Isar;
|
#
d6fa1861 |
|
04-Oct-2007 |
wenzelm <none@none> |
load variable.ML before conv.ML;
|
#
1cac996b |
|
20-Sep-2007 |
wenzelm <none@none> |
added interpretation.ML;
|
#
30b145ef |
|
14-Sep-2007 |
wenzelm <none@none> |
moved ML_XXX.ML files to Pure/ML;
|
#
789da2dd |
|
28-Aug-2007 |
berghofe <none@none> |
codegen.ML is now loaded in Pure again.
|
#
556be6ff |
|
14-Aug-2007 |
wenzelm <none@none> |
tuned order;
|
#
12ee453b |
|
14-Aug-2007 |
wenzelm <none@none> |
use logic.ML earlier; added primitive_defs.ML;
|
#
c1a38439 |
|
12-Aug-2007 |
wenzelm <none@none> |
added Syntax/simple_syntax.ML;
|
#
c710e368 |
|
01-Aug-2007 |
wenzelm <none@none> |
renamed config_option.ML to config.ML;
|
#
f23bfbd2 |
|
28-Jul-2007 |
wenzelm <none@none> |
use config_option.ML after sign.ML;
|
#
2a226891 |
|
27-Jul-2007 |
wenzelm <none@none> |
renamed config.ML to config_option.ML;
|
#
c8e5c285 |
|
25-Jul-2007 |
wenzelm <none@none> |
added config.ML;
|
#
a3fae8fc |
|
17-Jul-2007 |
wenzelm <none@none> |
simplified loading of ML files -- no static forward references;
|
#
7b68eb6e |
|
10-Jul-2007 |
wenzelm <none@none> |
use position.ML earlier;
|
#
828a997f |
|
09-Jul-2007 |
wenzelm <none@none> |
use position.ML after pretty.ML;
|
#
c40d0f94 |
|
12-Jun-2007 |
wenzelm <none@none> |
added context_position.ML;
|
#
3be492ee |
|
09-May-2007 |
wenzelm <none@none> |
added conv.ML;
|
#
dda7c2a4 |
|
25-Apr-2007 |
wenzelm <none@none> |
renamed some old names Theory.xxx to Sign.xxx;
|
#
2ab2aee9 |
|
15-Apr-2007 |
wenzelm <none@none> |
load type_infer.ML early;
|
#
7e02a9cd |
|
14-Apr-2007 |
wenzelm <none@none> |
removed Pure/Syntax/ROOT.ML;
|
#
3e1a5c63 |
|
03-Apr-2007 |
wenzelm <none@none> |
added print_mode (generic non-sense);
|
#
10708316 |
|
26-Feb-2007 |
wenzelm <none@none> |
added more_thm.ML;
|
#
ab5f130c |
|
04-Feb-2007 |
wenzelm <none@none> |
load morphism.ML later;
|
#
edbd4a04 |
|
19-Jan-2007 |
wenzelm <none@none> |
tuned order;
|
#
36fa6962 |
|
29-Dec-2006 |
wenzelm <none@none> |
removed obsolete proof_general.ML;
|
#
6ee0d0a0 |
|
29-Dec-2006 |
aspinall <none@none> |
Enable new Proof General code again after SML/NJ compatibility fixes by Florian.
|
#
0aa48e5b |
|
21-Dec-2006 |
aspinall <none@none> |
Disable new Proof General code until SML/NJ compile fixed.
|
#
eda48142 |
|
20-Dec-2006 |
aspinall <none@none> |
Use new Proof General code by default [see comment for reverting]
|
#
1e807976 |
|
14-Dec-2006 |
wenzelm <none@none> |
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
|
#
7b9d7f5f |
|
07-Dec-2006 |
wenzelm <none@none> |
reorganized structure Tactic vs. MetaSimplifier;
|
#
9989d06d |
|
06-Dec-2006 |
wenzelm <none@none> |
reorganized structure Goal vs. Tactic;
|
#
366de3ed |
|
04-Dec-2006 |
aspinall <none@none> |
Build instructions for new Proof General module [not yet activated]
|
#
c2d36a7c |
|
22-Nov-2006 |
wenzelm <none@none> |
added morphism.ML, General/ml_syntax.ML;
|
#
bae03da8 |
|
15-Nov-2006 |
wenzelm <none@none> |
added General/basics.ML;
|
#
a3874a91 |
|
11-Sep-2006 |
wenzelm <none@none> |
added Pure/term_subst.ML;
|
#
a7bac44a |
|
27-Jul-2006 |
wenzelm <none@none> |
added Pure/assumption.ML;
|
#
f7a35fd5 |
|
25-Jul-2006 |
wenzelm <none@none> |
added Pure/subgoal.ML;
|
#
c3d626c1 |
|
10-Jul-2006 |
wenzelm <none@none> |
added name.ML;
|
#
eca83d2a |
|
15-Jun-2006 |
wenzelm <none@none> |
added variable.ML;
|
#
d39a4568 |
|
10-Jun-2006 |
dixon <none@none> |
removed IsaPlannner things from Pure. Moved to Provers.
|
#
3945efca |
|
08-May-2006 |
wenzelm <none@none> |
tuned;
|
#
b5574c12 |
|
12-Apr-2006 |
wenzelm <none@none> |
added conjunction.ML;
|
#
b267069a |
|
09-Apr-2006 |
wenzelm <none@none> |
moved theory presentation to Isar/ROOT.ML;
|
#
7bd1a752 |
|
11-Mar-2006 |
wenzelm <none@none> |
use axclass.ML earlier (in Isar/ROOT.ML);
|
#
38b475b7 |
|
09-Feb-2006 |
wenzelm <none@none> |
use proof_general.ML: setmp quick_and_dirty captures default value;
|
#
eb5d0a8b |
|
06-Feb-2006 |
wenzelm <none@none> |
load envir.ML and logic.ML early;
|
#
17dec8dd |
|
31-Jan-2006 |
wenzelm <none@none> |
tuned comments;
|
#
8b2a4afa |
|
29-Jan-2006 |
wenzelm <none@none> |
CPure: Context.add_setup;
|
#
450fc36c |
|
14-Nov-2005 |
haftmann <none@none> |
added modules for code generator generation two, not operational yet
|
#
8e012ba6 |
|
02-Nov-2005 |
wenzelm <none@none> |
added consts.ML;
|
#
8500c2a9 |
|
21-Oct-2005 |
wenzelm <none@none> |
added goal.ML; moved use of goals.ML;
|
#
ef476777 |
|
19-Oct-2005 |
wenzelm <none@none> |
removed obsolete Thy/thy_parse.ML, Thy/thy_scan.ML, Thy/thy_syn.ML;
|
#
3742174b |
|
17-Sep-2005 |
wenzelm <none@none> |
added quick_and_dirty (from Isar/skip_proofs.ML);
|
#
e49506d8 |
|
17-Sep-2005 |
wenzelm <none@none> |
removed obsolete BasisLibrary; proof_general.ML: setmp proofs 1 to capture sane default preferences;
|
#
6adb1b75 |
|
01-Aug-2005 |
wenzelm <none@none> |
added compress.ML;
|
#
1dbd51e6 |
|
14-Jul-2005 |
wenzelm <none@none> |
tuned;
|
#
c720bbe9 |
|
12-Jul-2005 |
obua <none@none> |
- introduce Pure/Tools directory - add compute oracle to Pure/Tools
|
#
afddbaf5 |
|
17-Jun-2005 |
wenzelm <none@none> |
removed Pure/theory_data.ML;
|
#
696999ac |
|
28-May-2005 |
obua <none@none> |
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
|
#
1e517f3c |
|
23-Apr-2005 |
wenzelm <none@none> |
added content of Pure/Thy/ROOT.ML, Pure/Proof/ROOT.ML;
|
#
9f1ea5d9 |
|
21-Apr-2005 |
wenzelm <none@none> |
superceded by Pure.thy and CPure.thy;
|
#
b0ae8ea7 |
|
10-Mar-2005 |
ballarin <none@none> |
Debugging code (error_depth) removed.
|
#
f527ae4a |
|
09-Mar-2005 |
ballarin <none@none> |
First version of global registration command.
|
#
883f343f |
|
01-Feb-2005 |
paulson <none@none> |
the new subst tactic, by Lucas Dixon
|
#
d16d95fd |
|
25-Jun-2004 |
skalberg <none@none> |
Merging the meta-simplifier with the Provers-simplifier. Next step: make the simplification procedure simpset-aware.
|
#
571bb326 |
|
29-May-2004 |
wenzelm <none@none> |
moved print_mode to General/output.ML; load General/pretty.ML early;
|
#
35d34683 |
|
21-May-2004 |
wenzelm <none@none> |
type.ML now before Syntax module;
|
#
9c546104 |
|
21-Jul-2002 |
berghofe <none@none> |
Added program extraction module.
|
#
303740af |
|
02-Jul-2002 |
wenzelm <none@none> |
added fact_index.ML;
|
#
ad7f6f0c |
|
16-Jan-2002 |
wenzelm <none@none> |
Interface/proof_general.ML move to proof_general.ML;
|
#
ea706941 |
|
20-Nov-2001 |
wenzelm <none@none> |
print_depth 10;
|
#
521826c6 |
|
27-Oct-2001 |
wenzelm <none@none> |
tuned;
|
#
b444759f |
|
24-Oct-2001 |
wenzelm <none@none> |
print_depth 8 from the very beginning;
|
#
ede310e3 |
|
22-Oct-2001 |
wenzelm <none@none> |
reorganize sources to accomodate locales;
|
#
c3f6dcfa |
|
18-Oct-2001 |
wenzelm <none@none> |
revert to proper version (!);
|
#
8f03a002 |
|
14-Oct-2001 |
wenzelm <none@none> |
added object_logic.ML;
|
#
82cc3be4 |
|
31-Aug-2001 |
wenzelm <none@none> |
final proofs := 0;
|
#
b7e75f55 |
|
31-Aug-2001 |
berghofe <none@none> |
Added new files for proof terms.
|
#
f15717f7 |
|
05-Feb-2001 |
wenzelm <none@none> |
fixed version string;
|
#
a1cc734c |
|
15-Jan-2001 |
wenzelm <none@none> |
removed Session.finish ();
|
#
7405a161 |
|
07-Nov-2000 |
berghofe <none@none> |
Added new file meta_simplifier.ML
|
#
0d9b2b35 |
|
14-Sep-2000 |
wenzelm <none@none> |
"Isabelle repository version";
|
#
98e4b162 |
|
20-Mar-2000 |
wenzelm <none@none> |
quick_and_dirty moved to Isar/skip_proof.ML;
|
#
8a7a6067 |
|
26-Oct-1999 |
wenzelm <none@none> |
activate ml_prompts;
|
#
ed6d3586 |
|
05-Jun-1999 |
wenzelm <none@none> |
renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
|
#
d8d6ddee |
|
21-May-1999 |
wenzelm <none@none> |
added Interface/ROOT.ML Interface/isamode.ML Interface/proof_general.ML;
|
#
0cc368a5 |
|
17-Mar-1999 |
wenzelm <none@none> |
axclass.ML loaded after Isar;
|
#
f4dcf949 |
|
05-Feb-1999 |
wenzelm <none@none> |
Session.finish (); use;
|
#
33f1f4d8 |
|
04-Feb-1999 |
wenzelm <none@none> |
use, cd;
|
#
9cd86c49 |
|
03-Feb-1999 |
wenzelm <none@none> |
tuned;
|
#
9e4bbb05 |
|
29-Jan-1999 |
oheimb <none@none> |
moved print_mode to ROOT.ML
|
#
3f0c4240 |
|
11-Jan-1999 |
wenzelm <none@none> |
removed attribute.ML;
|
#
b87be476 |
|
28-Dec-1998 |
paulson <none@none> |
String added to BasisLibrary
|
#
1ca27929 |
|
09-Nov-1998 |
wenzelm <none@none> |
added Isar;
|
#
91d09873 |
|
20-Oct-1998 |
wenzelm <none@none> |
structure Hidden = struct end;
|
#
f45636dc |
|
02-Oct-1998 |
paulson <none@none> |
added Real to BasisLibrary
|
#
d4c14c27 |
|
25-Sep-1998 |
paulson <none@none> |
added Int to BasisLibrary
|
#
e8c12fc3 |
|
04-Aug-1998 |
wenzelm <none@none> |
added locale.ML;
|
#
54bdb8a3 |
|
29-Jul-1998 |
wenzelm <none@none> |
late setup of Pure and CPure;
|
#
e5f112c9 |
|
02-Jul-1998 |
wenzelm <none@none> |
tuned comment;
|
#
2e9430ba |
|
30-Jun-1998 |
wenzelm <none@none> |
added quick_and_dirty flag;
|
#
cebe035f |
|
29-Jun-1998 |
wenzelm <none@none> |
moved actual (C)Pure theories to pure.ML;
|
#
6b792018 |
|
10-Jun-1998 |
wenzelm <none@none> |
moved table.ML, object.ML, seq.ML, name_space.ML to General;
|
#
710c857d |
|
08-Jun-1998 |
wenzelm <none@none> |
added theory_data.ML;
|
#
dd11160f |
|
05-Jun-1998 |
wenzelm <none@none> |
added object.ML;
|
#
463a3a0d |
|
29-May-1998 |
wenzelm <none@none> |
tuned msgs;
|
#
f49b0d67 |
|
27-May-1998 |
wenzelm <none@none> |
version under control of Admin/makedist; ml_prompts;
|
#
14249579 |
|
25-May-1998 |
wenzelm <none@none> |
global_names moved to pure_thy.ML;
|
#
00b5d1a1 |
|
20-May-1998 |
wenzelm <none@none> |
tuned comments;
|
#
b572c874 |
|
03-Apr-1998 |
wenzelm <none@none> |
added attribute.ML;
|
#
21eb690e |
|
09-Mar-1998 |
wenzelm <none@none> |
tuned comment;
|
#
8de0e01f |
|
28-Dec-1997 |
wenzelm <none@none> |
replaced symtab.ML by table.ML;
|
#
93519908 |
|
15-Dec-1997 |
wenzelm <none@none> |
tuned;
|
#
4dd28c07 |
|
13-Dec-1997 |
wenzelm <none@none> |
version = "Isabelle98: Jan 1998";
|
#
a6613fdc |
|
04-Dec-1997 |
wenzelm <none@none> |
moved global_names ref to Pure/ROOT.ML;
|
#
96d41dcd |
|
22-Nov-1997 |
wenzelm <none@none> |
tuned;
|
#
ce14539d |
|
21-Nov-1997 |
wenzelm <none@none> |
changed Sequence interface (now Seq, in seq.ML);
|
#
a654949b |
|
20-Nov-1997 |
wenzelm <none@none> |
removed data.ML (made part of sign.ML);
|
#
87e374ed |
|
12-Nov-1997 |
wenzelm <none@none> |
structure BasisLibrary;
|
#
b5b70f96 |
|
24-Oct-1997 |
wenzelm <none@none> |
added pure_thy.ML;
|
#
d17354e7 |
|
22-Oct-1997 |
wenzelm <none@none> |
tuned;
|
#
65e477f8 |
|
14-Oct-1997 |
wenzelm <none@none> |
added data.ML;
|
#
67302a78 |
|
01-Oct-1997 |
wenzelm <none@none> |
added name_space.ML;
|
#
45107498 |
|
09-Jul-1997 |
wenzelm <none@none> |
removed init_database;
|
#
ced36543 |
|
21-May-1997 |
wenzelm <none@none> |
set version;
|
#
a7b9cd7e |
|
16-Apr-1997 |
wenzelm <none@none> |
added sorts.ML, type_infer.ML;
|
#
b3cff843 |
|
06-Feb-1997 |
wenzelm <none@none> |
cd made readably again;
|
#
e51c3416 |
|
27-Nov-1996 |
paulson <none@none> |
Uses Basis Library equivalent of cd
|
#
7aecb613 |
|
13-Nov-1996 |
paulson <none@none> |
Updated version and date
|
#
33ca5698 |
|
16-Jul-1996 |
paulson <none@none> |
Increased revision number
|
#
5f955682 |
|
21-Mar-1996 |
paulson <none@none> |
Now loads deriv.ML
|
#
389c82c1 |
|
15-Mar-1996 |
paulson <none@none> |
Updated for new file search.ML
|
#
bd582e4c |
|
01-Mar-1996 |
paulson <none@none> |
Theories are now in theory.ML
|
#
27ce7eaf |
|
16-Feb-1996 |
paulson <none@none> |
Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.
|
#
8772958d |
|
18-Jan-1996 |
paulson <none@none> |
New version number
|
#
243edb68 |
|
22-Dec-1995 |
paulson <none@none> |
Now loads symtab.ML before term.ML. Functor > SymtabFun has been changed to the structure Symtab.
|
#
066cdeaa |
|
14-Aug-1995 |
paulson <none@none> |
updated version number to revision 4
|
#
fbd6cc7e |
|
28-Apr-1995 |
nipkow <none@none> |
Added functor f() = struct end to hide functors to save space.
|
#
6fe9dee0 |
|
25-Apr-1995 |
lcp <none@none> |
updated version
|
#
ac89311a |
|
03-Mar-1995 |
clasohm <none@none> |
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
|
#
24bc7d07 |
|
27-Feb-1995 |
lcp <none@none> |
Updated the "version" variable (which was never done for Isabelle-94 revisions 1 and 2!)
|
#
1f5d90b5 |
|
12-Oct-1994 |
wenzelm <none@none> |
AxClass no longer open;
|
#
88887aec |
|
26-Sep-1994 |
wenzelm <none@none> |
added init_database (somewhat experimental);
|
#
ddae0a80 |
|
13-Sep-1994 |
lcp <none@none> |
updated the identifier "version"
|
#
a4619b14 |
|
26-May-1994 |
wenzelm <none@none> |
added "axclass.ML", structure AxClass;
|
#
5ac45b53 |
|
28-Oct-1993 |
lcp <none@none> |
updated version to October 93
|
#
2418a230 |
|
22-Oct-1993 |
clasohm <none@none> |
delete_file now has type string -> unit in both NJ and POLY, use of Pure/Thy/ROOT has been moved to the end of Pure/ROOT again
|
#
6f5acbf3 |
|
04-Oct-1993 |
wenzelm <none@none> |
Pure/ROOT.ML cleaned comments; removed extraneous 'print_depth 1'; replaced Basic_Syntax by BasicSyntax added 'use "install_pp.ML"'; Pure/README fixed comments; Pure/POLY.ML Pure/NJ.ML make_pp: added fbrk; Pure/install_pp.ML replaced "Ast" by "Syntax"; Pure/sign.ML added 'quote' to some error msgs;
|
#
3d89c2df |
|
16-Sep-1993 |
clasohm <none@none> |
moved use of Thy/ROOT.ML to end of file because Thy/read.ML needs Thm
|
#
f253ef6a |
|
15-Sep-1993 |
clasohm <none@none> |
Initial revision
|