| 2011-02-08 |
wenzelm |
2011-02-08 |
discontinued support for Poly/ML 5.2, which was the last version without proper multithreading and TimeLimit implementation;
|
file | diff | annotate |
| 2011-02-05 |
wenzelm |
2011-02-05 |
clarified bootstrapping of structure TimeLimit;
|
file | diff | annotate |
| 2010-12-17 |
wenzelm |
2010-12-17 |
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
|
file | diff | annotate |
| 2010-11-27 |
wenzelm |
2010-11-27 |
removed bash from ML system bootstrap, and past the Secure ML barrier;
|
file | diff | annotate |
| 2010-11-27 |
wenzelm |
2010-11-27 |
more explicit Isabelle_System operations;
|
file | diff | annotate |
| 2010-09-20 |
wenzelm |
2010-09-20 |
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
|
file | diff | annotate |
| 2010-09-17 |
wenzelm |
2010-09-17 |
simplified some internal flags using Config.T instead of full-blown Proof_Data;
|
file | diff | annotate |
| 2010-09-12 |
wenzelm |
2010-09-12 |
load type_infer.ML later -- proper context for Type_Infer.infer_types;
renamed Type_Infer.polymorphicT to Type.mark_polymorphic;
|
file | diff | annotate |
| 2010-09-08 |
haftmann |
2010-09-08 |
removed ancient constdefs command
|
file | diff | annotate |
| 2010-09-01 |
wenzelm |
2010-09-01 |
eliminated obsolete old-style goal stack package, which was considered the main Isabelle user interface at some point;
|
file | diff | annotate |
| 2010-08-30 |
wenzelm |
2010-08-30 |
more careful treatment of nested multi-exceptions, collapsing cumulatively empty list to Interrupt;
|
file | diff | annotate |
| 2010-08-23 |
wenzelm |
2010-08-23 |
recognize more "smlnj" variants;
|
file | diff | annotate |
| 2010-08-19 |
wenzelm |
2010-08-19 |
moved Isar_Document to Pure/PIDE;
|
file | diff | annotate |
| 2010-08-17 |
wenzelm |
2010-08-17 |
discontinued support for Poly/ML 5.0 and 5.1 versions;
|
file | diff | annotate |
| 2010-08-17 |
wenzelm |
2010-08-17 |
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;
|
file | diff | annotate |
| 2010-08-15 |
wenzelm |
2010-08-15 |
more explicit / functional ML version of document model;
tuned;
|
file | diff | annotate |
| 2010-08-14 |
wenzelm |
2010-08-14 |
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
|
file | diff | annotate |
| 2010-08-11 |
haftmann |
2010-08-11 |
more convenient split of class modules: class and class_declaration
|
file | diff | annotate |
| 2010-08-11 |
haftmann |
2010-08-11 |
renamed Theory_Target to the more appropriate Named_Target
|
file | diff | annotate |
| 2010-08-11 |
haftmann |
2010-08-11 |
merged
|
file | diff | annotate |
| 2010-08-11 |
haftmann |
2010-08-11 |
moved theory-level target operation fragements to Generic_Target; adjusted bootstrap order
|
file | diff | annotate |
| 2010-08-11 |
wenzelm |
2010-08-11 |
merged, resolving conflict in src/Pure/IsaMakefile concerning General/xml_data.ML;
|
file | diff | annotate |
| 2010-08-10 |
haftmann |
2010-08-10 |
split off structure Generic_Target into separate file
|
file | diff | annotate |
| 2010-08-11 |
wenzelm |
2010-08-11 |
Isar_Document command input via native Isabelle_Process commands, using YXML and XML_Data representation;
|
file | diff | annotate |
| 2010-08-10 |
wenzelm |
2010-08-10 |
type XML.body as basic data representation language;
tuned;
|
file | diff | annotate |
| 2010-08-05 |
wenzelm |
2010-08-05 |
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;
|
file | diff | annotate |
| 2010-07-24 |
wenzelm |
2010-07-24 |
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;
|
file | diff | annotate |
| 2010-07-12 |
wenzelm |
2010-07-12 |
removed legacy aliases;
|
file | diff | annotate |
| 2010-06-01 |
wenzelm |
2010-06-01 |
uniform ML environment setup for Isar and PG;
|
file | diff | annotate |
| 2010-06-01 |
wenzelm |
2010-06-01 |
keep structure ThyLoad for the sake of Proof General;
|
file | diff | annotate |
| 2010-05-31 |
wenzelm |
2010-05-31 |
modernized some structure names, keeping a few legacy aliases;
|
file | diff | annotate |
| 2010-05-27 |
wenzelm |
2010-05-27 |
renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
|
file | diff | annotate |
| 2010-05-27 |
wenzelm |
2010-05-27 |
renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
|
file | diff | annotate |
| 2010-05-18 |
wenzelm |
2010-05-18 |
do not open Legacy by default;
|
file | diff | annotate |
| 2010-05-17 |
wenzelm |
2010-05-17 |
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
eliminated slightly odd alias structure T;
|
file | diff | annotate |
| 2010-05-17 |
wenzelm |
2010-05-17 |
centralized legacy aliases;
|
file | diff | annotate |
| 2010-05-15 |
wenzelm |
2010-05-15 |
renamed structure SpecParse to Parse_Spec, keeping the old name as alias for some time;
|
file | diff | annotate |
| 2010-05-15 |
wenzelm |
2010-05-15 |
renamed structure ValueParse to Parse_Value;
eliminated old-style structure alias V;
|
file | diff | annotate |
| 2010-05-15 |
wenzelm |
2010-05-15 |
renamed structure OuterKeyword to Keyword and OuterParse to Parse, keeping the old names as legacy aliases for some time;
|
file | diff | annotate |
| 2010-03-24 |
wenzelm |
2010-03-24 |
slightly more logical bootstrap order -- also helps to sort out proof terms extension;
|
file | diff | annotate |
| 2010-03-09 |
wenzelm |
2010-03-09 |
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.;
|
file | diff | annotate |
| 2010-03-07 |
wenzelm |
2010-03-07 |
Digesting strings according to SHA-1.
|
file | diff | annotate |
| 2010-03-07 |
wenzelm |
2010-03-07 |
separate structure Typedecl;
|
file | diff | annotate |
| 2010-02-06 |
wenzelm |
2010-02-06 |
explicit representation of single-assignment variables;
|
file | diff | annotate |
| 2009-11-09 |
wenzelm |
2009-11-09 |
setup for official Poly/ML 5.3.0, which is now the default;
|
file | diff | annotate |
| 2009-11-01 |
wenzelm |
2009-11-01 |
Rules that characterize functional/relational specifications.
|
file | diff | annotate |
| 2009-10-01 |
wenzelm |
2009-10-01 |
Concurrently cached values.
|
file | diff | annotate |
| 2009-10-01 |
wenzelm |
2009-10-01 |
more official status of sequential implementations;
tuned;
|
file | diff | annotate |
| 2009-10-01 |
wenzelm |
2009-10-01 |
separate concurrent/sequential versions of lazy evaluation;
lazy based on future avoids wasted evaluations;
|
file | diff | annotate |
| 2009-09-29 |
wenzelm |
2009-09-29 |
explicit indication of Unsynchronized.ref;
|
file | diff | annotate |
| 2009-09-28 |
wenzelm |
2009-09-28 |
Dummy version of state variables -- plain refs for sequential access.
|
file | diff | annotate |
| 2009-08-11 |
wenzelm |
2009-08-11 |
clarified situation about unidentified repository versions -- in a distributed setting there is not "the" repository;
|
file | diff | annotate |
| 2009-07-25 |
wenzelm |
2009-07-25 |
renamed structure Display_Goal to Goal_Display;
|
file | diff | annotate |
| 2009-07-24 |
wenzelm |
2009-07-24 |
renamed Pure/tctical.ML to Pure/tactical.ML;
|
file | diff | annotate |
| 2009-07-20 |
wenzelm |
2009-07-20 |
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
load display.ML after assumption.ML, to accomodate proper contextual theorem display;
|
file | diff | annotate |
| 2009-07-16 |
wenzelm |
2009-07-16 |
Support for copy-avoiding functions on pure values, at the cost of readability.
|
file | diff | annotate |
| 2009-06-06 |
wenzelm |
2009-06-06 |
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
|
file | diff | annotate |
| 2009-06-04 |
wenzelm |
2009-06-04 |
just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources;
|
file | diff | annotate |
| 2009-06-02 |
wenzelm |
2009-06-02 |
early setup of secure operations (again, cf. deddd77112b7) -- NB: fix_ints is required for bootstrap;
late setup of ML_Env and ML_Compiler;
|
file | diff | annotate |
| 2009-06-01 |
wenzelm |
2009-06-01 |
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
|
file | diff | annotate |