| 2010-05-03 |
wenzelm |
2010-05-03 |
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
|
file | diff | annotate |
| 2010-04-28 |
wenzelm |
2010-04-28 |
localized default sort;
|
file | diff | annotate |
| 2010-03-28 |
wenzelm |
2010-03-28 |
implicit checkpoint in Local_Theory.theory as well -- no longer export Local_Theory.checkpoint;
|
file | diff | annotate |
| 2010-03-15 |
wenzelm |
2010-03-15 |
replaced type_syntax/term_syntax by uniform syntax_declaration;
|
file | diff | annotate |
| 2010-03-13 |
wenzelm |
2010-03-13 |
added Local_Theory.alias operations (independent of target);
|
file | diff | annotate |
| 2010-03-01 |
wenzelm |
2010-03-01 |
more uniform treatment of syntax for types vs. consts;
|
file | diff | annotate |
| 2009-11-19 |
wenzelm |
2009-11-19 |
Local_Theory.define: eliminated slightly odd kind argument -- such low-level definitions should be hardly ever exposed to end-users anyway;
|
file | diff | annotate |
| 2009-11-17 |
wenzelm |
2009-11-17 |
uniform new_group/reset_group;
tuned signature;
|
file | diff | annotate |
| 2009-11-13 |
wenzelm |
2009-11-13 |
modernized structure Local_Theory;
|
file | diff | annotate |
| 2009-11-13 |
wenzelm |
2009-11-13 |
eliminated slightly odd kind argument of LocalTheory.note(s);
added LocalTheory.notes_kind as fall-back for unusual cases;
|
file | diff | annotate |
| 2009-11-08 |
wenzelm |
2009-11-08 |
adapted Generic_Data, Proof_Data;
tuned;
|
file | diff | annotate |
| 2009-11-05 |
wenzelm |
2009-11-05 |
allow "pervasive" local theory declarations, which are applied the background theory;
|
file | diff | annotate |
| 2009-11-02 |
wenzelm |
2009-11-02 |
modernized structure Context_Position;
|
file | diff | annotate |
| 2009-10-28 |
wenzelm |
2009-10-28 |
let naming transform binding beforehand -- covering only the "conceal" flag for now;
export LocalTheory.standard_morphism;
|
file | diff | annotate |
| 2009-10-28 |
wenzelm |
2009-10-28 |
added restore_naming;
|
file | diff | annotate |
| 2009-10-25 |
wenzelm |
2009-10-25 |
maintain proper Name_Space.naming, with conceal and set_group;
maintain group via name space, not tags;
tuned signature;
tuned;
|
file | diff | annotate |
| 2009-10-25 |
wenzelm |
2009-10-25 |
allow name space entries to be "concealed" -- via binding/naming/local_theory;
|
file | diff | annotate |
| 2009-10-24 |
wenzelm |
2009-10-24 |
renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
|
file | diff | annotate |
| 2009-03-19 |
wenzelm |
2009-03-19 |
added map_contexts (cf. Proof.map_contexts);
|
file | diff | annotate |
| 2009-03-12 |
wenzelm |
2009-03-12 |
renamed sticky_prefix to mandatory_path;
|
file | diff | annotate |
| 2009-03-11 |
wenzelm |
2009-03-11 |
eliminated qualified_names naming policy: qualified names are only permitted via explicit Binding.qualify/qualified_name etc. (NB: user-level outer syntax should never do this);
|
file | diff | annotate |
| 2009-01-21 |
haftmann |
2009-01-21 |
binding is alias for Binding.T
|
file | diff | annotate |
| 2008-12-17 |
haftmann |
2008-12-17 |
dropped Ids
|
file | diff | annotate |
| 2008-12-05 |
haftmann |
2008-12-05 |
dropped NameSpace.declare_base
|
file | diff | annotate |
| 2008-12-04 |
haftmann |
2008-12-04 |
cleaned up binding module and related code
|
file | diff | annotate |
| 2008-09-29 |
wenzelm |
2008-09-29 |
target update: invisible context position avoids duplication of reports etc.;
|
file | diff | annotate |
| 2008-09-29 |
wenzelm |
2008-09-29 |
added exit_global, exit_result, exit_result_global;
ProofContext.norm_export_morphism;
|
file | diff | annotate |
| 2008-09-27 |
wenzelm |
2008-09-27 |
Theory.checkpoint for main operations, admits concurrent proofs;
|
file | diff | annotate |
| 2008-09-03 |
wenzelm |
2008-09-03 |
discontinued local axioms -- too difficult to implement, too easy to produce nonsense;
|
file | diff | annotate |
| 2008-09-02 |
wenzelm |
2008-09-02 |
type Attrib.binding abbreviates Name.binding without attributes;
Attrib.no_binding refers to Name.no_binding;
|
file | diff | annotate |
| 2008-09-02 |
wenzelm |
2008-09-02 |
explicit type Name.binding for higher-specification elements;
|
file | diff | annotate |
| 2008-08-27 |
wenzelm |
2008-08-27 |
type Properties.T;
|
file | diff | annotate |
| 2008-02-25 |
wenzelm |
2008-02-25 |
maintain group in lthy data, implicit use in operations;
tuned signature;
added group_position_of;
|
file | diff | annotate |
| 2008-01-26 |
wenzelm |
2008-01-26 |
grouped versions of axioms/define/notes;
|
file | diff | annotate |
| 2007-11-10 |
wenzelm |
2007-11-10 |
removed LocalTheory.target_naming/name;
|
file | diff | annotate |
| 2007-11-05 |
wenzelm |
2007-11-05 |
simplified LocalTheory.reinit;
|
file | diff | annotate |
| 2007-10-20 |
wenzelm |
2007-10-20 |
tuned abbrev interface;
|
file | diff | annotate |
| 2007-10-19 |
wenzelm |
2007-10-19 |
tuned interfaces;
|
file | diff | annotate |
| 2007-10-14 |
wenzelm |
2007-10-14 |
tuned;
|
file | diff | annotate |
| 2007-10-13 |
wenzelm |
2007-10-13 |
renamed def to define;
abbrev: return hypothetical def;
|
file | diff | annotate |
| 2007-10-11 |
wenzelm |
2007-10-11 |
local_theory: incorporated consts into axioms;
|
file | diff | annotate |
| 2007-10-10 |
wenzelm |
2007-10-10 |
generalized notation interface (add or del);
|
file | diff | annotate |
| 2007-10-09 |
wenzelm |
2007-10-09 |
removed LocalTheory.defs/target_morphism operations;
added target_morphism (from theory_target.ML);
|
file | diff | annotate |
| 2007-09-07 |
wenzelm |
2007-09-07 |
fixed type alias in signature;
|
file | diff | annotate |
| 2007-07-28 |
wenzelm |
2007-07-28 |
type Morphism.declaration;
|
file | diff | annotate |
| 2007-07-28 |
wenzelm |
2007-07-28 |
tuned signature;
|
file | diff | annotate |
| 2007-05-07 |
wenzelm |
2007-05-07 |
simplified DataFun interfaces;
|
file | diff | annotate |
| 2007-02-04 |
wenzelm |
2007-02-04 |
added full_naming;
|
file | diff | annotate |
| 2007-01-28 |
wenzelm |
2007-01-28 |
added interface for target_naming;
|
file | diff | annotate |
| 2006-12-15 |
wenzelm |
2006-12-15 |
renamed LocalTheory.assert to affirm;
|
file | diff | annotate |
| 2006-12-12 |
wenzelm |
2006-12-12 |
abbrev: tuned signature;
|
file | diff | annotate |
| 2006-12-10 |
wenzelm |
2006-12-10 |
added notation/abbrev (from term_syntax.ML);
|
file | diff | annotate |
| 2006-12-07 |
wenzelm |
2006-12-07 |
moved notation/abbrevs to TermSyntax;
|
file | diff | annotate |
| 2006-12-06 |
wenzelm |
2006-12-06 |
abbrevs: actually observe target_morphism;
|
file | diff | annotate |
| 2006-12-05 |
wenzelm |
2006-12-05 |
notation/abbreviation: more serious handling of morphisms;
|
file | diff | annotate |
| 2006-11-30 |
wenzelm |
2006-11-30 |
added full_name;
|
file | diff | annotate |
| 2006-11-26 |
wenzelm |
2006-11-26 |
abbrevs: no result;
added target_morphism/name;
simplified theory prefix (no option);
proper morphing of abbrevs/notation;
|
file | diff | annotate |
| 2006-11-23 |
wenzelm |
2006-11-23 |
uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
|
file | diff | annotate |
| 2006-11-21 |
wenzelm |
2006-11-21 |
LocalTheory.axioms/notes/defs: proper kind;
context_notes: ProofContext.set_stmt after import;
|
file | diff | annotate |
| 2006-11-10 |
wenzelm |
2006-11-10 |
simplified exit;
added reinit;
|
file | diff | annotate |