| 2006-04-11 |
wenzelm |
2006-04-11 |
added super_classes (from sorts.ML);
removed read/cert_classrel (see axclass.ML);
|
changeset |
files
|
| 2006-04-11 |
wenzelm |
2006-04-11 |
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
tuned;
|
changeset |
files
|
| 2006-04-11 |
wenzelm |
2006-04-11 |
moved abstract syntax operations to logic.ML;
maintain class parameters;
added params_of_sort;
added cert/read_classrel (from sign.ML), check class parameters;
tuned;
|
changeset |
files
|
| 2006-04-10 |
obua |
2006-04-10 |
Moved stuff from Ring_and_Field to Matrix
|
changeset |
files
|
| 2006-04-10 |
berghofe |
2006-04-10 |
Adapted to changed type of add_typedef_i.
|
changeset |
files
|
| 2006-04-10 |
nipkow |
2006-04-10 |
Hoare(Parallel) dependencies on document/*
|
changeset |
files
|
| 2006-04-10 |
nipkow |
2006-04-10 |
added references
|
changeset |
files
|
| 2006-04-10 |
nipkow |
2006-04-10 |
Minimal doc
|
changeset |
files
|
| 2006-04-10 |
nipkow |
2006-04-10 |
Included cyclic list examples
|
changeset |
files
|
| 2006-04-10 |
haftmann |
2006-04-10 |
fixed value restriction
|
changeset |
files
|
| 2006-04-10 |
nipkow |
2006-04-10 |
Added splicing algorithm.
|
changeset |
files
|
| 2006-04-10 |
wenzelm |
2006-04-10 |
hide (open) const;
|
changeset |
files
|
| 2006-04-10 |
wenzelm |
2006-04-10 |
simplified AxClass.add_axclass interface;
|
changeset |
files
|
| 2006-04-10 |
wenzelm |
2006-04-10 |
added aT (from axclass.ML);
non-pervasive itselfT, a_itselfT;
|
changeset |
files
|
| 2006-04-10 |
wenzelm |
2006-04-10 |
removed unused class_le_path, sort_less;
|
changeset |
files
|
| 2006-04-10 |
wenzelm |
2006-04-10 |
add_axclass(_i): return class name only;
subclass/arity statements: require actual TVars, store raw data;
tuned;
|
changeset |
files
|
| 2006-04-10 |
wenzelm |
2006-04-10 |
Term.itselfT;
|
changeset |
files
|
| 2006-04-09 |
nipkow |
2006-04-09 |
Added function "splice"
|
changeset |
files
|
| 2006-04-09 |
wenzelm |
2006-04-09 |
Even/Odd: avoid clash with even/odd of Main HOL;
|
changeset |
files
|
| 2006-04-09 |
wenzelm |
2006-04-09 |
results: smart_pretty_thm uses adhoc proof context if possible;
|
changeset |
files
|
| 2006-04-09 |
wenzelm |
2006-04-09 |
added full_name;
abbrevs: mode does not affect name space;
|
changeset |
files
|
| 2006-04-09 |
wenzelm |
2006-04-09 |
add_syntax: actually observe print mode;
|
changeset |
files
|
| 2006-04-09 |
wenzelm |
2006-04-09 |
print_term etc.: actually observe print mode in final output;
|
changeset |
files
|
| 2006-04-09 |
wenzelm |
2006-04-09 |
abbrevs: mode does not affect name space;
|
changeset |
files
|
| 2006-04-09 |
wenzelm |
2006-04-09 |
added coalesce;
|
changeset |
files
|
| 2006-04-09 |
wenzelm |
2006-04-09 |
moved theory presentation to Isar/ROOT.ML;
|
changeset |
files
|
| 2006-04-09 |
wenzelm |
2006-04-09 |
hide consts in Numeral.thy;
|
changeset |
files
|
| 2006-04-09 |
wenzelm |
2006-04-09 |
tuned syntax/abbreviations;
|
changeset |
files
|
| 2006-04-09 |
wenzelm |
2006-04-09 |
unfold(ed): not necessrily meta equations;
|
changeset |
files
|
| 2006-04-09 |
nipkow |
2006-04-09 |
Made "empty" an abbreviation.
|
changeset |
files
|
| 2006-04-09 |
nipkow |
2006-04-09 |
*** empty log message ***
|
changeset |
files
|
| 2006-04-09 |
nipkow |
2006-04-09 |
Removed old set interval syntax.
|
changeset |
files
|
| 2006-04-08 |
wenzelm |
2006-04-08 |
pretty_term: late externing of consts (support authentic syntax);
|
changeset |
files
|
| 2006-04-08 |
wenzelm |
2006-04-08 |
pretty: late externing of consts (support authentic syntax);
|
changeset |
files
|
| 2006-04-08 |
wenzelm |
2006-04-08 |
removed fix_mixfix;
added const_mixfix, mixfix_const;
|
changeset |
files
|
| 2006-04-08 |
wenzelm |
2006-04-08 |
abbreviation(_i): do not expand abbreviations, do not use derived_def;
|
changeset |
files
|
| 2006-04-08 |
wenzelm |
2006-04-08 |
add_abbrevs(_i): support print mode;
pretty_term': expand abbreviations only for well-typed terms;
added expand_abbrevs;
tuned;
|
changeset |
files
|
| 2006-04-08 |
wenzelm |
2006-04-08 |
abbrevs: support print mode;
|
changeset |
files
|
| 2006-04-08 |
wenzelm |
2006-04-08 |
simplified handling of authentic syntax (cf. early externing in consts.ML);
simplified extern_term;
|
changeset |
files
|
| 2006-04-08 |
wenzelm |
2006-04-08 |
'abbreviation': optional print mode;
|
changeset |
files
|
| 2006-04-08 |
wenzelm |
2006-04-08 |
tuned;
|
changeset |
files
|
| 2006-04-08 |
wenzelm |
2006-04-08 |
pretty_term': early vs. late externing (support authentic syntax);
add_abbrevs(_i): support print mode and authentic syntax;
|
changeset |
files
|
| 2006-04-08 |
wenzelm |
2006-04-08 |
print_theory: print abbreviations nicely;
|
changeset |
files
|
| 2006-04-08 |
wenzelm |
2006-04-08 |
added intern/extern/extern_early;
added expand_abbrevs flag;
strip_abss: demand ocurrences of bounds in body;
const decl: added flag for early externing (disabled for authentic syntax);
abbrevs: support print mode;
major cleanup;
|
changeset |
files
|
| 2006-04-08 |
wenzelm |
2006-04-08 |
refined 'abbreviation';
|
changeset |
files
|
| 2006-04-08 |
haftmann |
2006-04-08 |
made symlink relative
|
changeset |
files
|
| 2006-04-08 |
haftmann |
2006-04-08 |
made symlink relative
|
changeset |
files
|
| 2006-04-08 |
kleing |
2006-04-08 |
converted Müller to Mueller to make smlnj 110.58 work
|
changeset |
files
|
| 2006-04-07 |
berghofe |
2006-04-07 |
Fixed bug that caused proof of induction rule to fail
for inductive sets with trivial introduction rules
such as "x : S ==> x : S".
|
changeset |
files
|
| 2006-04-07 |
kleing |
2006-04-07 |
remame ASeries to Arithmetic_Series
|
changeset |
files
|
| 2006-04-07 |
berghofe |
2006-04-07 |
Added alternative version of thms_of_proof that does not recursively
descend into proofs of (named) theorems.
|
changeset |
files
|
| 2006-04-07 |
mengj |
2006-04-07 |
hash table now stores thm and get_clasimp_atp_lemmas returns thm rather than term.
|
changeset |
files
|
| 2006-04-07 |
mengj |
2006-04-07 |
filter now accepts axioms as thm, instead of term.
|
changeset |
files
|
| 2006-04-07 |
mengj |
2006-04-07 |
tptp_write_file accepts axioms as thm.
|
changeset |
files
|
| 2006-04-07 |
mengj |
2006-04-07 |
added another function for CNF.
|
changeset |
files
|
| 2006-04-07 |
mengj |
2006-04-07 |
lemmas returned from ResClasimp.get_clasimp_atp_lemmas are thm rather than term.
|
changeset |
files
|
| 2006-04-07 |
kleing |
2006-04-07 |
renamed ASeries to Arithmetic_Series, removed the ^M
|
changeset |
files
|
| 2006-04-06 |
urbanc |
2006-04-06 |
modified the perm_compose rule such that it
is applied as simplification rule (as simproc)
in the restricted case where the first
permutation is a swapping coming from a supports
problem
also deleted the perm_compose' rule from the set
of rules that are automatically tried
|
changeset |
files
|
| 2006-04-06 |
haftmann |
2006-04-06 |
cleanup in typedef/datatype package
|
changeset |
files
|
| 2006-04-06 |
haftmann |
2006-04-06 |
added explicit serialization for int equality
|
changeset |
files
|