| 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-29 |
wenzelm |
2010-04-29 |
ProofContext.read_const: allow for type constraint (for fixed variable);
added proof command 'write' to introduce concrete syntax within a proof body;
|
file | diff | annotate |
| 2010-04-25 |
wenzelm |
2010-04-25 |
modernized naming conventions of main Isar proof elements;
|
file | diff | annotate |
| 2010-04-23 |
wenzelm |
2010-04-23 |
explicit 'schematic_theorem' etc. for schematic theorem statements;
|
file | diff | annotate |
| 2010-04-11 |
wenzelm |
2010-04-11 |
Thm.add_axiom/add_def: return internal name of foundational axiom;
|
file | diff | annotate |
| 2010-03-22 |
wenzelm |
2010-03-22 |
added Specification.axiom convenience;
|
file | diff | annotate |
| 2010-03-07 |
wenzelm |
2010-03-07 |
modernized structure Object_Logic;
|
file | diff | annotate |
| 2010-03-07 |
wenzelm |
2010-03-07 |
modernized structure Local_Defs;
|
file | diff | annotate |
| 2010-03-01 |
wenzelm |
2010-03-01 |
added type_notation command;
|
file | diff | annotate |
| 2010-02-27 |
wenzelm |
2010-02-27 |
clarified ProofContext.read_const(_proper)/Args.const(_proper) wrt. strict logical consts;
|
file | diff | annotate |
| 2009-11-19 |
wenzelm |
2009-11-19 |
Specification.definition: Thm.definitionK marks exactly the high-level end-user result;
|
file | diff | annotate |
| 2009-11-19 |
bulwahn |
2009-11-19 |
replacing Predicate_Compile_Preproc_Const_Defs by more general Spec_Rules
|
file | diff | annotate |
| 2009-11-15 |
wenzelm |
2009-11-15 |
axiomatization: declare Spec_Rules, direct result;
|
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-12 |
wenzelm |
2009-11-12 |
eliminated slightly odd (unused) "axiom" and "assumption" -- collapsed to unspecific "";
|
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 |
declare Spec_Rules for most basic definitional packages;
|
file | diff | annotate |
| 2009-11-02 |
wenzelm |
2009-11-02 |
modernized structure Proof_Display;
|
file | diff | annotate |
| 2009-11-02 |
wenzelm |
2009-11-02 |
modernized structure AutoBind;
|
file | diff | annotate |
| 2009-11-01 |
wenzelm |
2009-11-01 |
modernized structure Context_Rules;
|
file | diff | annotate |
| 2009-11-01 |
wenzelm |
2009-11-01 |
modernized structure Rule_Cases;
|
file | diff | annotate |
| 2009-10-25 |
wenzelm |
2009-10-25 |
eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
|
file | diff | annotate |
| 2009-10-02 |
wenzelm |
2009-10-02 |
clarified Proof.refine_insert -- always "refine" to apply standard method treatment (of conjunctions);
|
file | diff | annotate |
| 2009-09-30 |
wenzelm |
2009-09-30 |
eliminated dead code;
|
file | diff | annotate |
| 2009-09-23 |
bulwahn |
2009-09-23 |
handling of definitions
|
file | diff | annotate |
| 2009-09-23 |
bulwahn |
2009-09-23 |
experimenting to add some useful interface for definitions
|
file | diff | annotate |
| 2009-03-28 |
wenzelm |
2009-03-28 |
renamed ProofContext.add_fixes_i to ProofContext.add_fixes, eliminated obsolete external version;
|
file | diff | annotate |
| 2009-03-28 |
wenzelm |
2009-03-28 |
renamed ProofContext.note_thmss_i to ProofContext.note_thmss, eliminated obsolete external version;
|
file | diff | annotate |
| 2009-03-19 |
wenzelm |
2009-03-19 |
use Name.of_binding for basic logical entities without name space (fixes, case names etc.);
|
file | diff | annotate |
| 2009-03-12 |
wenzelm |
2009-03-12 |
simplified versions check_spec, read_spec, check_free_spec, read_free_spec: operate on list of singleton statements;
simplified check_specification, read_specification: operate on a single list of simultaneous statements;
tuned;
|
file | diff | annotate |
| 2009-03-12 |
wenzelm |
2009-03-12 |
Assumption.local_prems_of;
|
file | diff | annotate |
| 2009-03-12 |
wenzelm |
2009-03-12 |
axiomatization: more precise treatment of binding;
|
file | diff | annotate |
| 2009-03-11 |
wenzelm |
2009-03-11 |
Thm.def_binding_optional;
|
file | diff | annotate |
| 2009-03-07 |
wenzelm |
2009-03-07 |
more uniform handling of binding in targets and derived elements;
|
file | diff | annotate |
| 2009-03-03 |
wenzelm |
2009-03-03 |
renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
minor tuning;
|
file | diff | annotate |
| 2009-01-21 |
wenzelm |
2009-01-21 |
removed Ids;
|
file | diff | annotate |
| 2009-01-21 |
haftmann |
2009-01-21 |
binding is alias for Binding.T
|
file | diff | annotate |
| 2008-12-19 |
ballarin |
2008-12-19 |
All logics ported to new locales.
|
file | diff | annotate |
| 2008-12-05 |
haftmann |
2008-12-05 |
Name.name_of -> Binding.base_name
|
file | diff | annotate |
| 2008-12-04 |
haftmann |
2008-12-04 |
cleaned up binding module and related code
|
file | diff | annotate |
| 2008-12-01 |
haftmann |
2008-12-01 |
new Binding module
|
file | diff | annotate |
| 2008-11-24 |
ballarin |
2008-11-24 |
Enable switching to new locales during session.
|
file | diff | annotate |
| 2008-11-24 |
ballarin |
2008-11-24 |
More ramifications of removal of 'includes' element.
|
file | diff | annotate |
| 2008-11-20 |
haftmann |
2008-11-20 |
tuned name bindings
|
file | diff | annotate |
| 2008-11-20 |
wenzelm |
2008-11-20 |
removed traces of former 'includes' element;
|
file | diff | annotate |
| 2008-11-17 |
haftmann |
2008-11-17 |
adjusted locale signature to *_cmd convention
|
file | diff | annotate |
| 2008-11-14 |
haftmann |
2008-11-14 |
Name.is_nothing
|
file | diff | annotate |
| 2008-10-30 |
ballarin |
2008-10-30 |
Dropped context element 'includes'.
|
file | diff | annotate |
| 2008-10-28 |
haftmann |
2008-10-28 |
cleanup code default attribute
|
file | diff | annotate |
| 2008-09-26 |
haftmann |
2008-09-26 |
removed obsolete name convention "func"
|
file | diff | annotate |
| 2008-09-03 |
wenzelm |
2008-09-03 |
axiomatization is now global-only;
|
file | diff | annotate |
| 2008-09-02 |
wenzelm |
2008-09-02 |
ProofDisplay.print_results;
|
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;
simplified ProofContext.inferred_param;
|
file | diff | annotate |
| 2008-08-13 |
wenzelm |
2008-08-13 |
ProofDisplay.theory_results;
|
file | diff | annotate |
| 2008-04-09 |
wenzelm |
2008-04-09 |
print_consts only for external specifications;
|
file | diff | annotate |
| 2008-03-20 |
wenzelm |
2008-03-20 |
renamed former get_thms(_silent) to get_fact(_silent);
|
file | diff | annotate |
| 2008-03-19 |
wenzelm |
2008-03-19 |
renamed datatype thmref to Facts.ref, tuned interfaces;
|
file | diff | annotate |
| 2007-11-10 |
wenzelm |
2007-11-10 |
notation: improved ProofContext.read_const does the job;
|
file | diff | annotate |