| 2010-03-13 |
wenzelm |
2010-03-13 |
Local_Defs.contract convenience;
|
file | diff | annotate |
| 2010-03-11 |
wenzelm |
2010-03-11 |
more basic Local_Defs.export_cterm;
|
file | diff | annotate |
| 2010-03-07 |
wenzelm |
2010-03-07 |
modernized structure Local_Defs;
|
file | diff | annotate |
| 2009-11-08 |
wenzelm |
2009-11-08 |
adapted Generic_Data, Proof_Data;
tuned;
|
file | diff | annotate |
| 2009-11-02 |
wenzelm |
2009-11-02 |
modernized structure Primitive_Defs;
|
file | diff | annotate |
| 2009-07-21 |
wenzelm |
2009-07-21 |
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
|
file | diff | annotate |
| 2009-06-24 |
wenzelm |
2009-06-24 |
renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported);
renamed Variable.importT_thms to Variable.importT (again);
|
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-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 |
Assumption.all_prems_of, Assumption.all_assms_of;
|
file | diff | annotate |
| 2009-03-11 |
wenzelm |
2009-03-11 |
Thm.def_binding_optional;
|
file | diff | annotate |
| 2009-03-04 |
blanchet |
2009-03-04 |
Merge.
|
file | diff | annotate |
| 2009-03-04 |
blanchet |
2009-03-04 |
Merge.
|
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-03-03 |
wenzelm |
2009-03-03 |
Thm.binding;
|
file | diff | annotate |
| 2009-01-21 |
haftmann |
2009-01-21 |
binding is alias for Binding.T
|
file | diff | annotate |
| 2009-01-11 |
haftmann |
2009-01-11 |
stripped Id
|
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-09-02 |
wenzelm |
2008-09-02 |
explicit type Name.binding for higher-specification elements;
|
file | diff | annotate |
| 2008-03-27 |
wenzelm |
2008-03-27 |
eliminated theory ProtoPure;
|
file | diff | annotate |
| 2007-10-20 |
wenzelm |
2007-10-20 |
added fixed_abbrev;
|
file | diff | annotate |
| 2007-10-19 |
wenzelm |
2007-10-19 |
tuned interfaces;
|
file | diff | annotate |
| 2007-10-14 |
wenzelm |
2007-10-14 |
added add_def;
|
file | diff | annotate |
| 2007-10-11 |
wenzelm |
2007-10-11 |
added export_cterm;
tuned;
|
file | diff | annotate |
| 2007-10-11 |
wenzelm |
2007-10-11 |
dest/cert_def: replaced Pretty.pp by explicit Proof.context;
|
file | diff | annotate |
| 2007-10-11 |
wenzelm |
2007-10-11 |
moved ProofContext.pp to Syntax.pp;
|
file | diff | annotate |
| 2007-08-14 |
wenzelm |
2007-08-14 |
PrimitiveDefs.dest/abs_def;
|
file | diff | annotate |
| 2007-07-29 |
wenzelm |
2007-07-29 |
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
|
file | diff | annotate |
| 2007-07-03 |
wenzelm |
2007-07-03 |
exported meta_rewrite_conv;
CONVERSION tactical;
|
file | diff | annotate |
| 2007-05-10 |
wenzelm |
2007-05-10 |
moved conversions to structure Conv;
|
file | diff | annotate |
| 2007-05-07 |
wenzelm |
2007-05-07 |
simplified DataFun interfaces;
|
file | diff | annotate |
| 2007-04-15 |
wenzelm |
2007-04-15 |
Thm.fold_terms;
|
file | diff | annotate |
| 2007-04-14 |
wenzelm |
2007-04-14 |
tuned signature;
export: precomputed closure, no reference to contexts;
|
file | diff | annotate |
| 2007-04-03 |
wenzelm |
2007-04-03 |
renamed Variable.import to import_thms (avoid clash with Alice keywords);
|
file | diff | annotate |
| 2006-12-14 |
wenzelm |
2006-12-14 |
added trans_terms/props;
|
file | diff | annotate |
| 2006-12-12 |
wenzelm |
2006-12-12 |
tuned expand_term;
|
file | diff | annotate |
| 2006-12-07 |
wenzelm |
2006-12-07 |
reorganized structure Tactic vs. MetaSimplifier;
|
file | diff | annotate |
| 2006-12-07 |
wenzelm |
2006-12-07 |
expand_term: based on Envir.expand_term;
tuned;
|
file | diff | annotate |
| 2006-12-07 |
wenzelm |
2006-12-07 |
reorganized structure Goal vs. Tactic;
|
file | diff | annotate |
| 2006-12-06 |
wenzelm |
2006-12-06 |
added expand;
export: added explicit term operation;
|
file | diff | annotate |
| 2006-11-29 |
wenzelm |
2006-11-29 |
added export;
removed find_def, expand_defs;
|
file | diff | annotate |
| 2006-11-28 |
wenzelm |
2006-11-28 |
simplified '?' operator;
added expand_defs;
|
file | diff | annotate |
| 2006-11-23 |
wenzelm |
2006-11-23 |
prefer Proof.context over Context.generic;
|
file | diff | annotate |
| 2006-10-11 |
wenzelm |
2006-10-11 |
add_defs: declare terms;
|
file | diff | annotate |
| 2006-10-09 |
wenzelm |
2006-10-09 |
simplified derived_def;
|
file | diff | annotate |
| 2006-10-07 |
wenzelm |
2006-10-07 |
replaced add_def by more elaborate add_defs;
added find_def (based on educated guesses);
|
file | diff | annotate |
| 2006-08-02 |
wenzelm |
2006-08-02 |
normalized Proof.context/method type aliases;
simplified Assumption/ProofContext.export;
|
file | diff | annotate |
| 2006-07-27 |
wenzelm |
2006-07-27 |
moved basic assumption operations from structure ProofContext to Assumption;
|
file | diff | annotate |
| 2006-07-08 |
wenzelm |
2006-07-08 |
Goal.prove: context;
|
file | diff | annotate |
| 2006-07-06 |
wenzelm |
2006-07-06 |
def_export: Drule.generalize;
|
file | diff | annotate |
| 2006-06-15 |
wenzelm |
2006-06-15 |
ProofContext: moved variable operations to struct Variable;
|
file | diff | annotate |
| 2006-05-07 |
wenzelm |
2006-05-07 |
removed 'concl is' patterns;
|
file | diff | annotate |
| 2006-02-06 |
wenzelm |
2006-02-06 |
cert_def: use Logic.dest_def;
moved abs_def to logic.ML;
derived_def: conditional flag;
|
file | diff | annotate |
| 2006-02-02 |
wenzelm |
2006-02-02 |
tuned comments;
|
file | diff | annotate |
| 2006-01-31 |
wenzelm |
2006-01-31 |
(un)fold: no raw flag;
tuned;
|
file | diff | annotate |
| 2006-01-31 |
wenzelm |
2006-01-31 |
export meta_rewrite_rule;
tuned;
|
file | diff | annotate |
| 2006-01-29 |
wenzelm |
2006-01-29 |
added attributes defn_add/del;
added (un)fold operations (from object_logic.ML);
tuned;
|
file | diff | annotate |
| 2006-01-28 |
wenzelm |
2006-01-28 |
Basic operations on local definitions.
|
file | diff | annotate |
| 2001-10-16 |
wenzelm |
2001-10-16 |
simplified exporter interface;
|
file | diff | annotate |