isabelle: Graph

'obtains' element;
2006-02-02, by wenzelm
'obtain': optional case name;
2006-02-02, by wenzelm
index elements;
2006-02-02, by wenzelm
* Isar: 'obtains' element;
2006-02-02, by wenzelm
tuned msg;
2006-02-02, by wenzelm
theorem(_in_locale): Element.statement, Obtain.statement;
2006-02-02, by wenzelm
added parname;
2006-02-02, by wenzelm
obtain(_i): optional name for 'that';
2006-02-02, by wenzelm
tuned comments;
2006-02-02, by wenzelm
moved (general_)statement to outer_parse.ML;
2006-02-02, by wenzelm
added concluding statements: Shows/Obtains;
2006-02-02, by wenzelm
moved specific map_typ/term to sign.ML;
2006-02-02, by wenzelm
added specific map_typ/term (from term.ML);
2006-02-02, by wenzelm
Exporting recdef's hints for use by new recdef package
2006-02-02, by krauss
*_asms_of fixed.
2006-02-02, by ballarin
add 64bit atbroy98 platform
2006-02-02, by kleing
updated;
2006-02-01, by wenzelm
Added "evaluation" method and oracle.
2006-02-01, by berghofe
new and updated protocol proofs by Giamp Bella
2006-02-01, by paulson
substantial cleanup and simplifications
2006-02-01, by haftmann
name clarifications
2006-02-01, by haftmann
added map_entry_yield
2006-02-01, by haftmann
- renamed some lemmas (some had names coming from ancient
2006-02-01, by urbanc
added all constructors from PhD
2006-02-01, by urbanc
axiomatization: retrict parameters to occurrences in specs;
2006-01-31, by wenzelm
improved comments;
2006-01-31, by wenzelm
tuned LocalDefs.unfold;
2006-01-31, by wenzelm
(un)fold: removed '(raw)' option;
2006-01-31, by wenzelm
added consts_retricted;
2006-01-31, by wenzelm
(un)fold: no raw flag;
2006-01-31, by wenzelm
tuned;
2006-01-31, by wenzelm
tuned LocalTheory.pretty_consts;
2006-01-31, by wenzelm
(un)folded: removed '(raw)' option;
2006-01-31, by wenzelm
lambda: abstract over TYPE argument, too;
2006-01-31, by wenzelm
tuned comments;
2006-01-31, by wenzelm
removal of ResClause.num_of_clauses and other simplifications
2006-01-31, by paulson
working SPASS support; much tidying
2006-01-31, by paulson
added serialization for arbitrary
2006-01-31, by haftmann
minor change to CodegenPackage interface
2006-01-31, by haftmann
minor cleanups
2006-01-31, by haftmann
more coherent lookup extraction functions
2006-01-31, by haftmann
reorganization of code to support DFG otuput
2006-01-31, by paulson
* Pure: 'advanced' translation functions use Context.generic instead of just theory;
2006-01-31, by wenzelm
declare defn rules;
2006-01-31, by wenzelm
all styles now reset to defaults first, i.e. the document may switch styles back and forth;
2006-01-31, by wenzelm
export meta_rewrite_rule;
2006-01-31, by wenzelm
advanced translations: Context.generic;
2006-01-31, by wenzelm
advanced translations: Context.generic;
2006-01-31, by wenzelm
tidy-up of res_clause.ML, removing the "predicates" field
2006-01-30, by paulson
'setup': no list type, support implicit setup;
2006-01-30, by wenzelm
'fixes': support plain vars;
2006-01-30, by wenzelm
fixed a syntax error!
2006-01-30, by paulson
replaced gen_list by enum
2006-01-30, by haftmann
adaptions to codegen_package
2006-01-30, by haftmann
various improvements
2006-01-30, by haftmann
added three times overloaded Isar instance command
2006-01-30, by haftmann
moved instance Isar command to class_package.ML
2006-01-30, by haftmann
added map_atype, map_aterms
2006-01-30, by haftmann
tuned proof;
2006-01-29, by wenzelm
declare atomize/defn for Ball;
2006-01-29, by wenzelm
invent_fixes: merely enter body temporarily;
2006-01-29, by wenzelm
'unfolding': LocalDefs.unfold;
2006-01-29, by wenzelm
moved treatment of object-logic equalities to local_defs.ML;
2006-01-29, by wenzelm
method (un)folded: option '(raw)';
2006-01-29, by wenzelm
added attributes defn_add/del;
2006-01-29, by wenzelm
added 'defn' attribute;
2006-01-29, by wenzelm
proper order of trfuns;
2006-01-29, by wenzelm
CPure: Context.add_setup;
2006-01-29, by wenzelm
tuned proofs;
2006-01-29, by wenzelm
implicit setup;
2006-01-29, by wenzelm
default rule step: norm_hhf_tac;
2006-01-29, by wenzelm
tuned comment;
2006-01-29, by wenzelm
declare 'defn' rules;
2006-01-29, by wenzelm
LocalDefs;
2006-01-28, by wenzelm
Basic operations on local definitions.
2006-01-28, by wenzelm
removed unnecessary Syntax.fix_mixfix;
2006-01-28, by wenzelm
added axiomatization_loc, definition_loc;
2006-01-28, by wenzelm
moved local defs to local_defs.ML;
2006-01-28, by wenzelm
LocalDefs;
2006-01-28, by wenzelm
removed unatomize;
2006-01-28, by wenzelm
(un)fold: support object-level rewrites;
2006-01-28, by wenzelm
added print_consts;
2006-01-28, by wenzelm
removed obsolete keyword 'files';
2006-01-28, by wenzelm
(un)folded: support object-level rewrites;
2006-01-28, by wenzelm
added equals_cong;
2006-01-28, by wenzelm
added Isar/local_defs.ML;
2006-01-28, by wenzelm
LocalDefs.add_def;
2006-01-28, by wenzelm
LocalDefs.def_export;
2006-01-28, by wenzelm
tuned proofs;
2006-01-28, by wenzelm
Pure/Isar: (un)folded, (un)fold, unfolding support
2006-01-28, by wenzelm
interrupt_timeout for Poly replaced by stub
2006-01-27, by webertj
added atomize_iff;
2006-01-27, by wenzelm
renamed Pretty.gen_list to Pretty.enum;
2006-01-27, by wenzelm
swapped theory_context;
2006-01-27, by wenzelm
swapped Toplevel.theory_context;
2006-01-27, by wenzelm
added invent_fixes;
2006-01-27, by wenzelm
swapped Toplevel.theory_context;
2006-01-27, by wenzelm
renamed reverse_atomize to unatomize;
2006-01-27, by wenzelm
init: include view;
2006-01-27, by wenzelm
improved 'notes', including proper treatment of locale results;
2006-01-27, by wenzelm
swapped Toplevel.theory_context;
2006-01-27, by wenzelm
Locale.init;
2006-01-27, by wenzelm
renamed gen_list to enum;
2006-01-27, by wenzelm
moved theorem tags from Drule to PureThy;
2006-01-27, by wenzelm
added ProofContext.pprint_context (depends on ProofContext.debug);
2006-01-27, by wenzelm
moved theorem tags from Drule to PureThy;
2006-01-27, by wenzelm
tidying up SPASS output
2006-01-27, by paulson
tidying
2006-01-27, by paulson
better reporting
2006-01-27, by paulson
Interface to access the specification of a named locale.
2006-01-27, by ballarin
Added new file Tools/ATP/reduce_axiomsN.ML
2006-01-27, by mengj
Added in new file Tools/ATP/reduce_axiomsN.ML
2006-01-27, by mengj
Changed codes that call relevance filter.
2006-01-27, by mengj
Relevance filtering. Has replaced the previous version.
2006-01-27, by mengj
interrupt_timeout now raises Interrupt instead of SML90.Interrupt
2006-01-26, by webertj
smaller example to prevent timeout
2006-01-26, by webertj
Fixed bug in code generator for primitive definitions that
2006-01-26, by berghofe
Inductive sets with no introduction rules are now allowed as well.
2006-01-26, by berghofe
added definition(_i);
2006-01-25, by wenzelm
renamed export to export_standard (again!), because it includes Drule.local_standard';
2006-01-25, by wenzelm
ProofContext.export_standard;
2006-01-25, by wenzelm
tuned atomize_cterm;
2006-01-25, by wenzelm
turned abstract_term into ProofContext.abs_def;
2006-01-25, by wenzelm
added constant definition;
2006-01-25, by wenzelm
added 'definition';
2006-01-25, by wenzelm
tuned comment;
2006-01-25, by wenzelm
export name_multi;
2006-01-25, by wenzelm
abs_def: improved error;
2006-01-25, by wenzelm
ObjectLogic.atomize_cterm;
2006-01-25, by wenzelm
updated;
2006-01-25, by wenzelm
works with DPLL solver now
2006-01-24, by webertj
the additional freshness-condition in the one-induction
2006-01-24, by urbanc
fixed code_generate syntax;
2006-01-24, by wenzelm
renamed axiomatize(_i) to axiomatization(_i);
2006-01-24, by wenzelm
renamed inferred_type to inferred_param;
2006-01-24, by wenzelm
ProofContext.inferred_param;
2006-01-24, by wenzelm
removed the_params;
2006-01-24, by wenzelm
added actual operations;
2006-01-24, by wenzelm
axiomatization: optional vars;
2006-01-24, by wenzelm
LocalTheory.pretty_consts;
2006-01-24, by wenzelm
tuned;
2006-01-24, by wenzelm
add_finals: prep_consts, i.e. varify type;
2006-01-24, by wenzelm
added dest_all;
2006-01-24, by wenzelm
TimeLimit replaced by interrupt_timeout
2006-01-23, by webertj
TimeLimit replaced by interrupt_timeout
2006-01-23, by webertj
Updated to Isabelle 2006-01-23
2006-01-23, by krauss
made change for ex1
2006-01-23, by urbanc
removed problematic keyword 'atom'
2006-01-23, by haftmann
more general serializer
2006-01-23, by haftmann
slight steps forward
2006-01-23, by haftmann
exported after_qed for axclass instance
2006-01-23, by haftmann
ResClasimp.get_clasimp_lemmas now takes all subgoals rather than only the first
2006-01-23, by paulson
Clausification now handles some IFs in rewrite rules (if-split did not work)
2006-01-23, by paulson
bugfix: induct_tac no longer raises THM "dest_state"
2006-01-23, by paulson
fixed the <<= notation
2006-01-23, by paulson
replacement of bool by a datatype (making problems first-order). More lemma names
2006-01-23, by paulson
Fixed a bug.
2006-01-23, by mengj
no essential changes
2006-01-22, by urbanc
made the change for setup-functions not returning functions
2006-01-22, by urbanc
a fixme comments about abs_fun_if, which should be called perm_if
2006-01-22, by urbanc
Local theory operations, with optional target locale.
2006-01-22, by wenzelm
added restore_body;
2006-01-22, by wenzelm
added the_params;
2006-01-22, by wenzelm
tuned order;
2006-01-22, by wenzelm
added Isar/local_theory.ML;
2006-01-22, by wenzelm
Ensure dereference is delayed.
2006-01-21, by mengj
tuned;
2006-01-21, by wenzelm
* ML: simplified type attribute;
2006-01-21, by wenzelm
simplified type attribute;
2006-01-21, by wenzelm
removed duplicate type_solver (cf. Tools/typechk.ML);
2006-01-21, by wenzelm
simplified type attribute;
2006-01-21, by wenzelm
simplified type attribute;
2006-01-21, by wenzelm
simplified type attribute;
2006-01-21, by wenzelm
rename map_theory/proof to theory/proof_map;
2006-01-21, by wenzelm
tuned proofs;
2006-01-21, by wenzelm
simplified type attribute;
2006-01-21, by wenzelm
simplified type attribute;
2006-01-21, by wenzelm
type information is now also printed.
2006-01-20, by mengj
added some debugging code.
2006-01-20, by mengj
fixed a bug
2006-01-20, by mengj
quote "atom";
2006-01-19, by wenzelm
updated;
2006-01-19, by wenzelm
* ML/Isar: theory setup has type (theory -> theory);
2006-01-19, by wenzelm
use/use_thy: Output.toplevel_errors;
2006-01-19, by wenzelm
added basic syntax;
2006-01-19, by wenzelm
moved pure syntax to Syntax/syntax.ML and pure_thy.ML;
2006-01-19, by wenzelm
keep: disable Output.toplevel_errors;
2006-01-19, by wenzelm
run_thy: removed Output.toplevel_errors;
2006-01-19, by wenzelm
added ML_errors;
2006-01-19, by wenzelm
use: Output.ML_errors;
2006-01-19, by wenzelm
Syntax.basic_syn;
2006-01-19, by wenzelm
setup: theory -> theory;
2006-01-19, by wenzelm
tuned setmp;
2006-01-19, by wenzelm
setup: theory -> theory;
2006-01-19, by wenzelm
tuned comments;
2006-01-19, by wenzelm
setup: theory -> theory;
2006-01-19, by wenzelm
setup: theory -> theory;
2006-01-19, by wenzelm
Use generic Simplifier.simp_add attribute instead
2006-01-19, by berghofe
Re-inserted consts_code declaration accidentally deleted
2006-01-19, by berghofe
strengthened some lemmas; simplified some proofs
2006-01-19, by paulson
substantial improvement in serialization handling
2006-01-18, by haftmann
fixed one proof that broke because of the changes
2006-01-18, by urbanc
substantial improvements in code generator
2006-01-17, by haftmann
these hacks are no longer needed
2006-01-17, by paulson
improved SPASS support
2006-01-17, by paulson
case_result: drop_schematic, i.e. be permissive about illegal binds;
2006-01-16, by wenzelm
put_facts: do not pretend local thms were named;
2006-01-16, by wenzelm
declare the1_equality [elim?];
2006-01-16, by wenzelm
tuned;
2006-01-15, by wenzelm
tuned;
2006-01-15, by wenzelm
* Classical: optional weight for attributes;
2006-01-15, by wenzelm
guess: used fixed inferred_type of vars;
2006-01-15, by wenzelm
export add_args;
2006-01-15, by wenzelm
attributes: optional weight;
2006-01-15, by wenzelm
classical attributes: optional weight;
2006-01-15, by wenzelm
prefer ex1I over ex_ex1I in single-step reasoning;
2006-01-15, by wenzelm
generic attributes;
2006-01-14, by wenzelm
tuned;
2006-01-14, by wenzelm
* ML/Isar: simplified treatment of user-level errors;
2006-01-14, by wenzelm
sane ERROR vs. TOPLEVEL_ERROR handling;
2006-01-14, by wenzelm
added Isar.toplevel;
2006-01-14, by wenzelm
Output.error_msg;
2006-01-14, by wenzelm
removed special ERROR handling stuff (transform_error etc.);
2006-01-14, by wenzelm
added exception ERROR, error, cat_error, sys_error, assert, deny, assert_all;
2006-01-14, by wenzelm
Output.debug;
2006-01-14, by wenzelm
generated code: raise Match instead of ERROR;
2006-01-14, by wenzelm
sane ERROR handling;
2006-01-14, by wenzelm
blacklist experiments
2006-01-13, by paulson
more readable divide ops
2006-01-13, by paulson
more practical time limit
2006-01-13, by paulson
*** empty log message ***
2006-01-13, by nipkow
mixfix: added Structure;
2006-01-13, by wenzelm
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
2006-01-13, by wenzelm
uniform handling of fixes;
2006-01-13, by wenzelm
uniform handling of fixes;
2006-01-13, by wenzelm
uniform handling of fixes;
2006-01-13, by wenzelm
uniform handling of fixes;
2006-01-13, by wenzelm
tuned;
2006-01-13, by wenzelm
generic_setup: optional argument, defaults to Context.setup();
2006-01-13, by wenzelm
added map_theory, map_proof;
2006-01-13, by wenzelm
removed obsolete sign_of;
2006-01-13, by wenzelm
implicit setup, which admits exception_trace;
2006-01-13, by wenzelm
ProofContext.def_export;
2006-01-13, by wenzelm
updated to new induction principle
2006-01-11, by urbanc
cahges to use the new induction-principle (now proved in
2006-01-11, by urbanc
changes to make use of the new induction principle proved by
2006-01-11, by urbanc
Implemented proof of (strong) induction rule.
2006-01-11, by berghofe
Added theorem at_finite_select.
2006-01-11, by berghofe
added lemmas perm_empty, perm_insert to do with
2006-01-11, by urbanc
merged the silly lemmas into the eqvt proof of subtype
2006-01-11, by urbanc
tuned proofs
2006-01-11, by urbanc
tuned the eqvt-proof
2006-01-11, by urbanc
rolled back the last addition since these lemmas were already
2006-01-11, by urbanc
added the thms-collection "pt_id" (collection of all pt_<ak>1 lemmas)
2006-01-11, by urbanc
tuned
2006-01-11, by urbanc
tidied, and added missing thm divide_less_eq_1_neg
2006-01-11, by paulson
tidied, and giving theorems names
2006-01-11, by paulson
add transitivity rules
2006-01-11, by huffman
tuned;
2006-01-11, by wenzelm
updated;
2006-01-11, by wenzelm
tuned;
2006-01-10, by wenzelm
generic attributes;
2006-01-10, by wenzelm
* ML: generic context, data, attributes;
2006-01-10, by wenzelm
added context_of -- generic context;
2006-01-10, by wenzelm
generic attributes;
2006-01-10, by wenzelm
print rules: generic context;
2006-01-10, by wenzelm
Specification.pretty_consts ctxt;
2006-01-10, by wenzelm
generic data and attributes;
2006-01-10, by wenzelm
added rule, declaration;
2006-01-10, by wenzelm
added generic syntax;
2006-01-10, by wenzelm
tuned dependencies;
2006-01-10, by wenzelm
added declaration_attribute;
2006-01-10, by wenzelm
support for generic contexts with data;
2006-01-10, by wenzelm
fix_tac: no warning;
2006-01-10, by wenzelm
generic attributes;
2006-01-10, by wenzelm
Attrib.rule;
2006-01-10, by wenzelm
tuned
2006-01-10, by urbanc
added the lemmas supp_char and supp_string
2006-01-10, by urbanc
added some lemmas to the collection "abs_fresh"
2006-01-09, by urbanc
_E suffix for compatibility with AddIffs
2006-01-09, by paulson
tidied
2006-01-09, by paulson
simplified the special-case simprules
2006-01-09, by paulson
theorems need names
2006-01-09, by paulson
commented the transitivity and narrowing proof
2006-01-09, by urbanc
Theory specifications --- with type-inference, but no internal polymorphism.
2006-01-07, by wenzelm
added infer_type, declared_type;
2006-01-07, by wenzelm
added param, spec, named_spec;
2006-01-07, by wenzelm
added init;
2006-01-07, by wenzelm
added 'axiomatization';
2006-01-07, by wenzelm
Specification.pretty_consts;
2006-01-07, by wenzelm
gen_names: preserve empty names;
2006-01-07, by wenzelm
added Isar/specification.ML;
2006-01-07, by wenzelm
updated;
2006-01-07, by wenzelm
another change for the new induct-method
2006-01-07, by urbanc
RuleCases.make_nested;
2006-01-07, by wenzelm
support nested cases;
2006-01-07, by wenzelm
support nested cases;
2006-01-07, by wenzelm
RuleCases.make_common;
2006-01-07, by wenzelm
pretty_locale: backquote notes;
2006-01-07, by wenzelm
RuleCases.make_simple;
2006-01-07, by wenzelm
tuned order;
2006-01-07, by wenzelm
added backquote;
2006-01-07, by wenzelm
RuleCases.make_common/nested;
2006-01-07, by wenzelm
* Provers/induct: improved simultaneous goals -- nested cases;
2006-01-07, by wenzelm
added private datatype nprod (copy of prod) to be
2006-01-07, by urbanc
changed PRO_RED proof to conform with the new induction rules
2006-01-07, by urbanc
prep_meta_eq: reuse mk_rews of local simpset;
2006-01-06, by wenzelm
removed obsolete eqrule_HOL_data.ML;
2006-01-06, by wenzelm
removed obsolete eqrule_FOL_data.ML;
2006-01-06, by wenzelm
simplified EqSubst setup;
2006-01-06, by wenzelm
obsolete, reuse mk_rews of local simpset;
2006-01-06, by wenzelm
Toplevel.theory_to_proof;
2006-01-06, by wenzelm
transactions now always see quasi-functional intermediate checkpoint;
2006-01-06, by wenzelm
tuned EqSubst setup;
2006-01-06, by wenzelm
Pure/Isar: Toplevel.theory_to_proof admits transactions that modify the theory;
2006-01-06, by wenzelm
hide type datatype node;
2006-01-05, by wenzelm
tuned print_theorems_theory;
2006-01-05, by wenzelm
Toplevel.proof_position_of;
2006-01-05, by wenzelm
store_thm: transfer to current context, i.e. the target theory;
2006-01-05, by wenzelm
replaced swap by contrapos_np;
2006-01-05, by wenzelm
added setminus;
2006-01-05, by wenzelm
proper handling of simultaneous goals and mutual rules;
2006-01-05, by wenzelm
provide projections of induct_weak, induct_unsafe;
2006-01-05, by wenzelm
added strict_mutual_rule;
2006-01-05, by wenzelm
RuleCases.strict_mutual_rule;
2006-01-05, by wenzelm
changed the name of the type "nOption" to "noption".
2006-01-05, by urbanc
added "fresh_singleton" lemma
2006-01-04, by urbanc
added more documentation; will now try out a modification
2006-01-04, by urbanc
Reversed Larry's option/iff change.
2006-01-04, by nipkow
substantial additions using locales
2006-01-04, by haftmann
exported read|cert_arity interfaces
2006-01-04, by haftmann
trace_simp_depth_limit is 1 by default
2006-01-04, by nipkow
removed pointless trace msg.
2006-01-04, by nipkow
preservation of names
2006-01-04, by paulson
a few more named lemmas
2006-01-04, by paulson
fix: reintroduced pred_ctxt in gen_add_locale
2006-01-04, by haftmann
tuned;
2006-01-04, by wenzelm
* Pure/Isar: Toplevel.theory_theory_to_proof;
2006-01-04, by wenzelm
added unlocalize_mfix;
2006-01-04, by wenzelm
added unlocalize_mixfix;
2006-01-04, by wenzelm
added theory_to_theory_to_proof, which may change theory before entering the proof;
2006-01-04, by wenzelm
tuned;
2006-01-04, by wenzelm
moved forget_proof to toplevel.ML;
2006-01-04, by wenzelm
Toplevel.forget_proof;
2006-01-04, by wenzelm
adapted Toplevel.Proof;
2006-01-04, by wenzelm
removed dead code;
2006-01-04, by wenzelm
more stuff;
2006-01-04, by wenzelm
Provers/classical: stricter checks to ensure that supplied intro, dest and
2006-01-03, by paulson
added explicit paths to required theories
2006-01-03, by paulson
added implementation manual;
2006-01-03, by wenzelm
more stuff;
2006-01-03, by wenzelm
fixed LaTeX source;
2006-01-03, by wenzelm
class now a keyword
2006-01-03, by haftmann
class now an keyword, quoted where necessary
2006-01-03, by haftmann
add_local_context now yields imported and body elements seperatly; additional slight clenup in code
2006-01-03, by haftmann
rearranged burrow_split to fold_burrow to allow composition with fold_map
2006-01-03, by haftmann
added unfolding(_i);
2006-01-03, by wenzelm
unparse String/AltString: escape quotes;
2006-01-03, by wenzelm
tuned;
2006-01-03, by wenzelm
avoid hardwired Trueprop;
2006-01-03, by wenzelm
added 'using' command;
2006-01-03, by wenzelm
updated;
2006-01-03, by wenzelm
added IsarImplementation;
2006-01-03, by wenzelm
updated -- lost update!?
2006-01-03, by wenzelm
* Pure/Isar: new command 'unfolding';
2006-01-03, by wenzelm
ISABELLE_USER for remote cvs access;
2006-01-02, by wenzelm
outline;
2006-01-02, by wenzelm
"The Isabelle/Isar Implementation" manual;
2006-01-02, by wenzelm
* Provers/classical: removed obsolete classical version of elim_format;
2005-12-31, by wenzelm
tuned forall_intr_vars;
2005-12-31, by wenzelm
added classical_rule, which replaces Data.make_elim;
2005-12-31, by wenzelm
explicitly reject consts *Goal*, *False*;
2005-12-31, by wenzelm
elim rules: Classical.classical_rule;
2005-12-31, by wenzelm
removed obsolete cla_dist_concl;
2005-12-31, by wenzelm
removed classical elim_format;
2005-12-31, by wenzelm
removed obsolete Provers/make_elim.ML;
2005-12-31, by wenzelm
obsolete, see classical_rule in Provers/classical.ML;
2005-12-31, by wenzelm
more robust phantomsection;
2005-12-31, by wenzelm
require cla_dist_concl, avoid assumptions about concrete syntax;
2005-12-30, by wenzelm
avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
2005-12-30, by wenzelm
provide equality_name, not_name;
2005-12-30, by wenzelm
fixed final_consts;
2005-12-30, by wenzelm
provide cla_dist_concl;
2005-12-30, by wenzelm
non-PDF: phantomsection;
2005-12-30, by wenzelm
added atom keyword
2005-12-29, by haftmann
changes in code generator keywords
2005-12-29, by haftmann
adaptions to changes in code generator
2005-12-29, by haftmann
slight improvements
2005-12-29, by haftmann
slightly improved serialization
2005-12-28, by haftmann
substantial improvements in code generating
2005-12-27, by haftmann
added map_index
2005-12-27, by haftmann
tuned proofs;
2005-12-23, by wenzelm
removed obsolete atomize_old;
2005-12-23, by wenzelm
removed obsolete induct_atomize_old;
2005-12-23, by wenzelm
the "skolem" attribute and better initialization of the clause database
2005-12-23, by paulson
blacklist of prolific theorems (must be replaced by an attribute later
2005-12-23, by paulson
tidied
2005-12-23, by paulson
tuned;
2005-12-23, by wenzelm
* Provers/induct: support simultaneous goals with mutual rules;
2005-12-23, by wenzelm
induct etc.: admit multiple rules;
2005-12-23, by wenzelm
backpatching of Substring.full;
2005-12-23, by wenzelm
goal/qed: proper treatment of two levels of conjunctions;
2005-12-23, by wenzelm
Logic.mk_conjunction_list;
2005-12-23, by wenzelm
turned bicompose_no_flatten into compose_no_flatten, without elimination;
2005-12-23, by wenzelm
CONJUNCTS: full nesting (again), PRECISE_CONJUNCTS: outer level of nesting;
2005-12-23, by wenzelm
added mk_conjunction_list2;
2005-12-23, by wenzelm
conj_elim_precise: proper treatment of nested conjunctions;
2005-12-23, by wenzelm
Thm.compose_no_flatten;
2005-12-23, by wenzelm
proper treatment of nested conjunctions, i.e. simultaneous goals and mutual rules;
2005-12-23, by wenzelm
is_prefix
2005-12-23, by haftmann
slight improvements
2005-12-22, by haftmann
more lemmas
2005-12-22, by nipkow
shorter proof
2005-12-22, by paulson
Tuned syntax for perm.
2005-12-22, by berghofe
new lemmas
2005-12-22, by nipkow
Fixed a use of an outdated Substring function
2005-12-22, by paulson
tuned;
2005-12-22, by wenzelm
exh_casedist2: norm_hhf_eq;
2005-12-22, by wenzelm
added bicompose_no_flatten, which refrains from
2005-12-22, by wenzelm
bicompose_proof: no_flatten;
2005-12-22, by wenzelm
conclude/SELECT: Thm.bicompose_no_flatten avoids unsolicited modification of result;
2005-12-22, by wenzelm
Transform mutual rule into projection.
2005-12-22, by wenzelm
added Provers/project_rule.ML
2005-12-22, by wenzelm
structure ProjectRule;
2005-12-22, by wenzelm
* induct: improved treatment of mutual goals and mutual rules;
2005-12-22, by wenzelm
updated auxiliary facts for induct method;
2005-12-22, by wenzelm
prop_tr': proper handling of aprop marked as bound;
2005-12-22, by wenzelm
consume: expand defs in prems of concls;
2005-12-22, by wenzelm
cases: main is_proper flag;
2005-12-22, by wenzelm
auto cases: marked improper;
2005-12-22, by wenzelm
conjunction_tac: single goal;
2005-12-22, by wenzelm
CONJUNCTS2;
2005-12-22, by wenzelm
rule_context: numbered cases;
2005-12-22, by wenzelm
conjunction_tac: single goal;
2005-12-22, by wenzelm
renamed imp_cong' to imp_cong_rule;
2005-12-22, by wenzelm
mk_conjunction: proper treatment of bounds;
2005-12-22, by wenzelm
fixed has_internal;
2005-12-22, by wenzelm
Tactic.precise_conjunction_tac;
2005-12-22, by wenzelm
added locale meta_conjunction_syntax and various conjunction rules;
2005-12-22, by wenzelm
simplified setup: removed dest_concls, local_impI, conjI;
2005-12-22, by wenzelm
induct_rulify;
2005-12-22, by wenzelm
actually produce projected rules;
2005-12-22, by wenzelm
*.inducts holds all projected rules;
2005-12-22, by wenzelm
tuned;
2005-12-22, by wenzelm
tuned induct proofs;
2005-12-22, by wenzelm
mutual induct with *.inducts;
2005-12-22, by wenzelm
wf_induct_rule: consumes 1;
2005-12-22, by wenzelm
structure ProjectRule;
2005-12-22, by wenzelm
updated auxiliary facts for induct method;
2005-12-22, by wenzelm
slight improvements
2005-12-21, by haftmann
slight improvements in name handling
2005-12-21, by haftmann
slight refinements
2005-12-21, by haftmann
added eq_ord
2005-12-21, by haftmann
slight clean ups
2005-12-21, by haftmann
discontinued unflat in favour of burrow and burrow_split
2005-12-21, by haftmann
new hash table module in HOL/Too/s
2005-12-21, by paulson
modified suffix for [iff] attribute
2005-12-21, by paulson
removed or modified some instances of [iff]
2005-12-21, by paulson
tuned;
2005-12-20, by wenzelm
added .cvsignore
2005-12-20, by haftmann
removed improper .cvsignore
2005-12-20, by haftmann
removed superfluos is_prefix functions
2005-12-20, by haftmann
resolved shadowing of Library.find_first
2005-12-20, by haftmann
removed infix prefix, introduces burrow
2005-12-20, by haftmann
Literals in clauses are sorted now. Added functions for clause equivalence tests and hashing clauses to words.
2005-12-20, by mengj
Added functions for fol_type; also put some functions to the signature, used by ResHolClause.
2005-12-20, by mengj
made the changes according to Florian's re-arranging of
2005-12-19, by urbanc
added proofs to show that every atom-kind combination
2005-12-19, by urbanc
added thms to perm_compose (so far only composition
2005-12-19, by urbanc
tuned one comment
2005-12-19, by urbanc
fixed a bug that occured when more than one atom-type
2005-12-19, by urbanc
fixed proof
2005-12-19, by nipkow
more cleaning up - this time of the cp-instance
2005-12-18, by urbanc
improved the finite-support proof
2005-12-18, by urbanc
improved the code for showing that a type is
2005-12-18, by urbanc
simp del: empty_Collect_eq;
2005-12-17, by wenzelm
sort_distinct;
2005-12-17, by wenzelm
added sort_distinct;
2005-12-17, by wenzelm
added container-lemma fresh_eqvt
2005-12-16, by urbanc
I think the earlier version was completely broken
2005-12-16, by urbanc
tuned more proofs
2005-12-16, by urbanc
new lemmas
2005-12-16, by nipkow
re-arranged tuples (theory * 'a) to ('a * theory) in Pure
2005-12-16, by haftmann
re-arranged tuples (theory * 'a) to ('a * theory) in Pure
2005-12-16, by haftmann
hashing to eliminate the output of duplicate clauses
2005-12-16, by paulson
hash tables from SML/NJ
2005-12-16, by paulson
re-arranged tuples (theory * 'a) to ('a * theory) in Pure
2005-12-16, by haftmann
there was a small error in the last commit - fixed now
2005-12-15, by urbanc
tuned more proof and added in-file documentation
2005-12-15, by urbanc
improved proofs;
2005-12-15, by wenzelm
acc_induct: proper tags;
2005-12-15, by wenzelm
removed obsolete/unused setup_induction;
2005-12-15, by wenzelm
tuned the proof of transitivity/narrowing
2005-12-15, by urbanc
No axiom, arity or classrel clauses contain HOL.type. Negative occurrences are
2005-12-15, by paulson
made further tunings
2005-12-15, by urbanc
Added functions to test equivalence between clauses.
2005-12-15, by mengj
ex/Sudoku.thy
2005-12-14, by webertj
deleted redundant (looping!) simprule
2005-12-14, by paulson
modified example for new clauses
2005-12-14, by paulson
removal of some redundancies (e.g. one-point-rules) in clause production
2005-12-14, by paulson
removed unused function repeat_RS
2005-12-14, by paulson
Changed literals' ordering and the functions for sorting literals.
2005-12-14, by mengj
1. changed fol_type, it's not a string type anymore.
2005-12-14, by mengj
changed ATP input files' names and location.
2005-12-14, by mengj
Potentially infinite lists as greatest fixed-point.
2005-12-13, by wenzelm
Provers/induct: coinduct;
2005-12-13, by wenzelm
tuned proofs;
2005-12-13, by wenzelm
added HOL/Library/Coinductive_List.thy;
2005-12-13, by wenzelm
added a fresh_left lemma that contains all instantiation
2005-12-13, by urbanc
initial commit (not to be seen by the public)
2005-12-13, by urbanc
simpset for computation in raw_arith_tac added just as comment, nothing changed!
2005-12-13, by chaieb
deals with Suc in mod expressions
2005-12-13, by chaieb
Poplog/pml provides a proper print function already!
2005-12-13, by wenzelm
meson no longer does these examples
2005-12-13, by paulson
now generates the name "append"
2005-12-13, by paulson
removal of functional reflexivity axioms
2005-12-13, by paulson
list_of_indset now also generates code for set type.
2005-12-13, by berghofe
added generic name mangler
2005-12-12, by haftmann
improvement in eq handling
2005-12-12, by haftmann
improvements in class and eq handling
2005-12-12, by haftmann
added dummy 'print' to non-polyml systems
2005-12-12, by haftmann
ISAR-fied some proofs
2005-12-11, by urbanc
completed the sn proof and changed the manual
2005-12-11, by urbanc
changed the types in accordance with Florian's changes
2005-12-10, by urbanc
substantial improvements for class code generation
2005-12-09, by haftmann
improved extraction interface
2005-12-09, by haftmann
tuned
2005-12-09, by urbanc
oriented result pairs in PureThy
2005-12-09, by haftmann
tuned;
2005-12-08, by wenzelm
removed Syntax.deskolem;
2005-12-08, by wenzelm
swap: no longer pervasive;
2005-12-08, by wenzelm
replaced swap by contrapos_np;
2005-12-08, by wenzelm
tuned proofs;
2005-12-08, by wenzelm
Cla.swap;
2005-12-08, by wenzelm
removed hint for Classical.swap, which is not really user-level anyway;
2005-12-08, by wenzelm
tuned sources and proofs
2005-12-08, by wenzelm
Classical.swap;
2005-12-08, by wenzelm
* HOL: Theorem 'swap' is no longer bound at the ML top-level.
2005-12-08, by wenzelm
Adapted to new type of PureThy.add_defs_i.
2005-12-08, by berghofe
replaced swap by Classical.swap;
2005-12-07, by wenzelm
avoid unportable tail;
2005-12-07, by wenzelm
tuned
2005-12-07, by urbanc
removed thms 'swap' and 'nth_map' from ML toplevel
2005-12-06, by haftmann
improved serialization of classes to haskell
2005-12-06, by haftmann
improved class handling
2005-12-06, by haftmann
added 'dig' combinator
2005-12-06, by haftmann
re-oriented some result tuples in PureThy
2005-12-06, by haftmann
Added more functions for new type embedding of HOL clauses.
2005-12-06, by mengj
Added new type embedding methods for translating HOL clauses.
2005-12-06, by mengj
added code to say that discrete types (nat, bool, char)
2005-12-05, by urbanc
tuned
2005-12-05, by urbanc
transitivity should be now in a reasonable state. But
2005-12-05, by urbanc
tuned
2005-12-05, by urbanc
ISAR-fied two proofs
2005-12-05, by urbanc
Adapted to new type of store_thmss(_atts).
2005-12-05, by berghofe
Added store_thmss_atts to signature again.
2005-12-05, by berghofe
tuned
2005-12-04, by urbanc
tuned
2005-12-04, by urbanc
tuned
2005-12-04, by urbanc
added an Isar-proof for the abs_ALL lemma
2005-12-04, by urbanc
tuning
2005-12-04, by urbanc
defines: beta/eta contract lhs;
2005-12-02, by wenzelm
asts_to_terms: builtin free_fixed translation makes local binders work properly;
2005-12-02, by wenzelm
mixfix_args: 1 for binders;
2005-12-02, by wenzelm
removed fixed_tr: now handled in syntax module;
2005-12-02, by wenzelm
added mixfixT;
2005-12-02, by wenzelm
defs: beta/eta contract lhs;
2005-12-02, by wenzelm
abs_def: beta/eta contract lhs;
2005-12-02, by wenzelm
Added recdef congruence rules for bounded quantifiers and commonly used
2005-12-02, by krauss
various improvements
2005-12-02, by haftmann
adjusted to improved code generator interface
2005-12-02, by haftmann
added perhaps option combinator
2005-12-02, by haftmann
adopted keyword for code generator
2005-12-02, by haftmann
Factored out proof for normalization of applications (norm_list).
2005-12-02, by berghofe
introduced new map2, fold
2005-12-02, by haftmann
typo
2005-12-01, by kleing
simprocs: static evaluation of simpset;
2005-12-01, by wenzelm
tuned;
2005-12-01, by wenzelm
tuned msg;
2005-12-01, by wenzelm
ProofContext.lthms_containing: suppress obvious duplicates;
2005-12-01, by wenzelm
unfold_tac: static evaluation of simpset;
2005-12-01, by wenzelm
superceded by timestart|stop.bash;
2005-12-01, by wenzelm
cpu time = user + system;
2005-12-01, by wenzelm
replaced lib/scripts/showtime by more advanced lib/scripts/timestart|stop.bash;
2005-12-01, by wenzelm
assoc_consts and assoc_types now check number of arguments in template.
2005-12-01, by berghofe
Added new component "sorts" to record datatype_info.
2005-12-01, by berghofe
timestop - report timing based on environment (cf. timestart.bash);
2005-12-01, by wenzelm
timestart - setup bash environment for timing;
2005-12-01, by wenzelm
Improved norm_proof to handle proofs containing term (type) variables
2005-12-01, by berghofe
restoring the old status of subset_refl
2005-12-01, by paulson
oriented pairs theory * 'a to 'a * theory
2005-12-01, by haftmann
initial cleanup to use the new induction method
2005-12-01, by urbanc
cleaned up further the proofs (diamond still needs work);
2005-12-01, by urbanc
changed "fresh:" to "avoiding:" and cleaned up the weakening example
2005-12-01, by urbanc
match_bind(_i): return terms;
2005-11-30, by wenzelm
method 'fact': SIMPLE_METHOD, i.e. insert facts;
2005-11-30, by wenzelm
simulaneous 'def';
2005-11-30, by wenzelm
added facilities to prove the pt and fs instances
2005-11-30, by urbanc
started to change the transitivity/narrowing case:
2005-11-30, by urbanc
changed everything until the interesting transitivity_narrowing
2005-11-30, by urbanc
minor improvements
2005-11-30, by haftmann
modified almost everything for the new nominal_induct
2005-11-30, by urbanc
Changed order of predicate arguments and quantifiers in strong induction rule.
2005-11-30, by berghofe
fixed the lemma where the new names generated by nominal_induct
2005-11-30, by urbanc
added one clause for substitution in the lambda-case and
2005-11-30, by urbanc
added rename_params_rule: recover orginal fresh names in subgoals/cases;
2005-11-30, by wenzelm
changed induction principle and everything to conform with the
2005-11-30, by urbanc
fresh: frees instead of terms, rename corresponding params in rule;
2005-11-30, by wenzelm
adapted to the new nominal_induction
2005-11-30, by urbanc
changed \<sim> of permutation equality to \<triangleq>
2005-11-30, by urbanc
fresh_unit_elim and fresh_prod_elim -- for nominal_induct;
2005-11-30, by wenzelm
reimplement Case expression pattern matching to support lazy patterns
2005-11-30, by huffman
add definitions as defs, not axioms
2005-11-30, by huffman
changed section names
2005-11-30, by huffman
add xsymbol syntax for u type constructor
2005-11-30, by huffman
add constant unit_when
2005-11-30, by huffman
proper treatment of tuple/tuple_fun -- nest to the left!
2005-11-30, by wenzelm
moved nth_list to Pure/library.ML;
2005-11-29, by wenzelm
added nth_list;
2005-11-29, by wenzelm
added mk_split;
2005-11-29, by wenzelm
changed the order of the induction variable and the context
2005-11-29, by urbanc
reworked version with proper support for defs, fixes, fresh specification;
2005-11-29, by wenzelm
added haskell serializer
2005-11-29, by haftmann
exported customized syntax interface
2005-11-29, by haftmann
Corrected atom class constraints in strong induction rule.
2005-11-29, by berghofe
made some of the theorem look-ups static (by using
2005-11-29, by urbanc
added (curried) fold2
2005-11-28, by haftmann
added proof of measure_induct_rule;
2005-11-28, by wenzelm
Added flags for setting and detecting whether a problem needs combinators.
2005-11-28, by mengj
Only output types if !keep_types is true.
2005-11-28, by mengj
Added two functions for CNF translation, used by other files.
2005-11-28, by mengj
Added in four control flags for HOL and FOL translations.
2005-11-28, by mengj
Slight modification to trace information.
2005-11-28, by mengj
Added two methods "vampire" and "eprover" that handle both HOL and FOL proofs.
2005-11-28, by mengj
Only output arities and class relations if !ResClause.keep_types is true.
2005-11-28, by mengj
some small tuning
2005-11-28, by urbanc
ISAR-fied two proofs about equality for abstraction functions.
2005-11-28, by urbanc
* Provers/induct: obtain pattern;
2005-11-27, by wenzelm
added an authors section (please let me know if somebody is left out or unhappy)
2005-11-27, by urbanc
some minor tunings
2005-11-27, by urbanc
added the version of nominal.thy that contains
2005-11-27, by urbanc
cleaned up all examples so that they work with the
2005-11-27, by urbanc
finished cleaning up the parts that collect
2005-11-27, by urbanc
Corrected treatment of non-recursive abstraction types.
2005-11-26, by berghofe
tuned induct proofs;
2005-11-25, by wenzelm
induct: insert defs in object-logic form;
2005-11-25, by wenzelm
tuned induct proofs;
2005-11-25, by wenzelm
tuned induct proofs;
2005-11-25, by wenzelm
consume: unfold defs in all major prems;
2005-11-25, by wenzelm
revert_skolem: fall back on Syntax.deskolem;
2005-11-25, by wenzelm
forall_conv ~1;
2005-11-25, by wenzelm
added dummy_pattern;
2005-11-25, by wenzelm
tuned names;
2005-11-25, by wenzelm
forall_conv: limit prefix;
2005-11-25, by wenzelm
fix_tac: proper treatment of major premises in goal;
2005-11-25, by wenzelm
removed obsolete dummy paragraphs;
2005-11-25, by wenzelm
tuned;
2005-11-25, by wenzelm
code generator: case expressions, improved name resolving
2005-11-25, by haftmann
added fsub.thy (poplmark challenge) to the examples
2005-11-25, by urbanc
Fixed problem with strong induction theorem for datatypes containing
2005-11-25, by berghofe
send more information with test-takes-too-long message
2005-11-25, by kleing
fixed spelling of 'case_conclusion';
2005-11-24, by wenzelm
tuned induct proofs;
2005-11-24, by wenzelm
tuned induction proofs;
2005-11-23, by wenzelm
more robust revert_skolem;
2005-11-23, by wenzelm
tuned;
2005-11-23, by wenzelm
Provers/induct: definitional insts and fixing;
2005-11-23, by wenzelm
consume: proper treatment of defs;
2005-11-23, by wenzelm
added case_conclusion attribute;
2005-11-23, by wenzelm
(co)induct: taking;
2005-11-23, by wenzelm
RuleCases.case_conclusion;
2005-11-23, by wenzelm
tuned;
2005-11-23, by wenzelm
added case_conclusion attribute;
2005-11-23, by wenzelm
improved failure tracking
2005-11-23, by haftmann
Datatype_Universe: hide base names only;
2005-11-22, by wenzelm
added type cases/cases_tactic, and CASES, SUBGOAL_CASES;
2005-11-22, by wenzelm
cases_tactic;
2005-11-22, by wenzelm
moved multi_resolve(s) to drule.ML;
2005-11-22, by wenzelm
find_xxxS: term instead of thm;
2005-11-22, by wenzelm
export map_tags;
2005-11-22, by wenzelm
make coinduct actually work;
2005-11-22, by wenzelm
Drule.multi_resolves;
2005-11-22, by wenzelm
declare coinduct rule;
2005-11-22, by wenzelm
added code generator syntax
2005-11-22, by haftmann
added codegenerator
2005-11-22, by haftmann
added code generator syntax
2005-11-22, by haftmann
new treatment of polymorphic types, using Sign.const_typargs
2005-11-22, by paulson
added codegen package
2005-11-21, by haftmann
added serializer
2005-11-21, by haftmann
tweak
2005-11-21, by paulson
fixed some inconveniencies in website
2005-11-21, by haftmann
CONJUNCTS;
2005-11-19, by wenzelm
tuned;
2005-11-19, by wenzelm
Goal.norm_hhf_protected;
2005-11-19, by wenzelm
added coinduct attribute;
2005-11-19, by wenzelm
added CONJUNCTS: treat conjunction as separate sub-goals;
2005-11-19, by wenzelm
simpset: added reorient field, set_reorient;
2005-11-19, by wenzelm
tuned norm_hhf_protected;
2005-11-19, by wenzelm
removed conj_mono;
2005-11-19, by wenzelm
induct: CONJUNCTS for multiple goals;
2005-11-19, by wenzelm
tuned induct syntax;
2005-11-19, by wenzelm
FOL: -p 2;
2005-11-19, by wenzelm
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
2005-11-18, by chaieb
-- changed the interface of functions vampire_oracle and eprover_oracle.
2005-11-18, by mengj
-- terms are fully typed.
2005-11-18, by mengj
-- before converting axiom and conjecture clauses into ResClause.clause format, perform "check_is_fol_term" first.
2005-11-18, by mengj
-- combined common CNF functions used by HOL and FOL axioms, the difference between conversion of HOL and FOL theorems only comes in when theorems are converted to ResClause.clause or ResHolClause.clause format.
2005-11-18, by mengj
-- added combinator reduction axioms (typed and untyped) for HOL goals.
2005-11-18, by mengj
-- split up inputs to ATPs into two groups: temporary files (axioms and goals) and permanent helper files (e.g. combinator reduction axioms).
2005-11-18, by mengj
-- combined "make_nnf" functions for both FOL and HOL vampire/eprover methods.
2005-11-18, by mengj
-- removed "check_is_fol" from "make_nnf" so that the NNF procedure doesn't check whether a thm is FOL.
2005-11-18, by mengj
tuned document;
2005-11-16, by wenzelm
tuned;
2005-11-16, by wenzelm
improved induction proof: local defs/fixes;
2005-11-16, by wenzelm
tuned Pattern.match/unify;
2005-11-16, by wenzelm
added deskolem;
2005-11-16, by wenzelm
added THEN_ALL_NEW_CASES;
2005-11-16, by wenzelm
added revert_skolem, mk_def, add_def;
2005-11-16, by wenzelm
ProofContext.mk_def;
2005-11-16, by wenzelm
Term.betapplys;
2005-11-16, by wenzelm
tuned Pattern.match/unify;
2005-11-16, by wenzelm
added betapplys;
2005-11-16, by wenzelm
tuned interfaces to support incremental match/unify (cf. versions in type.ML);
2005-11-16, by wenzelm
tuned;
2005-11-16, by wenzelm
norm_hhf: no normalization of protected props;
2005-11-16, by wenzelm
added protect_cong, cong_mono_thm;
2005-11-16, by wenzelm
induct: support local definitions to be passed through the induction;
2005-11-16, by wenzelm
Trueprop: use ObjectLogic.judgment etc.;
2005-11-16, by wenzelm
Term.betapply;
2005-11-16, by wenzelm
new version of "tryres" allowing multiple unifiers (apparently needed for
2005-11-16, by paulson
pgmlsymbolson: append Symbol.xsymbolsN at end!
2005-11-16, by wenzelm
better no -d option;
2005-11-15, by wenzelm
added generic transformators
2005-11-15, by haftmann
removal of is_hol
2005-11-14, by paulson
added module system
2005-11-14, by haftmann
added modules for code generator generation two, not operational yet
2005-11-14, by haftmann
class_package - operational view on type classes
2005-11-14, by haftmann
string_of_alist - convenient q'n'd printout function
2005-11-14, by haftmann
support for polyml-4.2.0;
2005-11-14, by wenzelm
new syntax for class_package
2005-11-14, by haftmann
added const_instance;
2005-11-14, by wenzelm
added instance;
2005-11-14, by wenzelm
added ML-Systems/polyml-4.1.4-patch.ML, ML-Systems/polyml-4.2.0.ML;
2005-11-14, by wenzelm
Compatibility wrapper for Poly/ML 4.2.0.
2005-11-14, by wenzelm
tuned;
2005-11-14, by wenzelm
added a few equivariance lemmas (they need to be automated
2005-11-14, by urbanc
changed the HOL_basic_ss back and selectively added
2005-11-13, by urbanc
exchanged HOL_ss for HOL_basic_ss in the simplification
2005-11-13, by urbanc
a proof step corrected due to the changement in the presburger method.
2005-11-11, by chaieb
old argument "abs" is replaced by "no_abs". Abstraction is turned on by default.
2005-11-11, by chaieb
add header
2005-11-11, by huffman
tuned proofs;
2005-11-10, by wenzelm
moved find_free to term.ML;
2005-11-10, by wenzelm
guess: Seq.hd;
2005-11-10, by wenzelm
guess: Toplevel.proof;
2005-11-10, by wenzelm
added find_free (from Isar/proof_context.ML);
2005-11-10, by wenzelm
curried multiply;
2005-11-10, by wenzelm
induct method: fixes;
2005-11-10, by wenzelm
uncurried Consts.typargs;
2005-11-10, by wenzelm
renamed Thm.cgoal_of to Thm.cprem_of;
2005-11-10, by wenzelm
duplicate axioms in ATP linkup, and general fixes
2005-11-10, by paulson
tidying
2005-11-10, by paulson
called the induction principle "unsafe" instead of "test".
2005-11-10, by urbanc
Skolemization by inference, but not quite finished
2005-11-09, by paulson
Explicit data structures for some Isar language elements.
2005-11-09, by wenzelm
tuned;
2005-11-09, by wenzelm
tvars_intr_list: natural argument order;
2005-11-09, by wenzelm
moved datatype elem to element.ML;
2005-11-09, by wenzelm
P.context_element, P.locale_element;
2005-11-09, by wenzelm
Element.context;
2005-11-09, by wenzelm
use existing exeption Empty;
2005-11-09, by wenzelm
avoid code redundancy;
2005-11-09, by wenzelm
tuned comments;
2005-11-09, by wenzelm
removed obsolete term set operations;
2005-11-09, by wenzelm
P.locale_element;
2005-11-09, by wenzelm
added fold_terms;
2005-11-09, by wenzelm
added Isar/element.ML;
2005-11-09, by wenzelm
Thm.varifyT': natural argument order;
2005-11-09, by wenzelm
added join function
2005-11-09, by haftmann
allowing indentation of 'theory' keyword
2005-11-08, by haftmann
simplified after_qed;
2005-11-08, by wenzelm
avoid prove_plain, export_plain, simplified after_qed;
2005-11-08, by wenzelm
removed export_plain;
2005-11-08, by wenzelm
renamed assert_prop to ensure_prop;
2005-11-08, by wenzelm
renamed goals.ML to old_goals.ML;
2005-11-08, by wenzelm
export compose_hhf;
2005-11-08, by wenzelm
removed impose_hyps, satisfy_hyps;
2005-11-08, by wenzelm
const args: do not store variable names (unused);
2005-11-08, by wenzelm
renamed goals.ML to old_goals.ML;
2005-11-08, by wenzelm
(fix for accidental commit)
2005-11-08, by haftmann
(codegen)
2005-11-08, by haftmann
generate pattern combinators for new datatypes
2005-11-08, by huffman
reimplemented Case syntax using print/parse translations; moved as-patterns to separate section
2005-11-07, by huffman
add case syntax for type one
2005-11-07, by huffman
remove syntax for as-patterns
2005-11-07, by huffman
avoid 'as' as identifier;
2005-11-07, by wenzelm
avoid 'as' as identifier;
2005-11-07, by wenzelm
Added strong induction theorem (currently only axiomatized!).
2005-11-07, by berghofe
Initial commit.
2005-11-07, by urbanc
Initial commit of the theory "Weakening".
2005-11-07, by urbanc
added thms perm, distinct and fresh to the simplifier.
2005-11-07, by urbanc
added proper fillin_mixfix
2005-11-07, by haftmann
added fillin_mixfix, replace_quote
2005-11-07, by haftmann
New function store_thmss_atts.
2005-11-07, by berghofe
used the function Library.product for the cprod from Stefan
2005-11-07, by urbanc
fixed bug with nominal induct
2005-11-07, by urbanc
added fillin_mixfix' needed by serializer
2005-11-07, by haftmann
add case syntax stuff
2005-11-06, by huffman
use consts for infix syntax
2005-11-06, by huffman
add proof of Bekic's theorem: fix_cprod
2005-11-06, by huffman
simplify definitions
2005-11-05, by huffman
put iterate and fix in separate sections; added Letrec
2005-11-05, by huffman
renamed and added ch2ch, cont2cont, mono2mono theorems ending in _fun, _lambda, _LAM
2005-11-05, by huffman
add line breaks to Rep_CFun syntax
2005-11-05, by huffman
moved adm_chfindom from Fix.thy to Cfun.thy; moved admw-related stuff to its own section
2005-11-04, by huffman
moved adm_chfindom from Fix.thy to Cfun.thy
2005-11-04, by huffman
cleaned up
2005-11-04, by huffman
add print translation: Abs_CFun f => LAM x. f x
2005-11-04, by huffman
Changed the way additional lemmas are passed to ATP methods for proof of a goal: now only list them after the methods' names.
2005-11-03, by mengj
improve support for mutual recursion: now generates correct copy constant and induction theorem for mutually-recursive types; initial support for indirect recursion
2005-11-03, by huffman
reimplement copy_def to use data constructor constants
2005-11-03, by huffman
cleaned up; renamed library function mk_cRep_CFun to list_ccomb; replaced rep_TFree with dest_TFree; added functions spair, mk_stuple
2005-11-03, by huffman
generate lambda pattern syntax for new data constructors
2005-11-03, by huffman
changed order of arguments for constant behind If-then-else-fi syntax; added LAM patterns for TT, FF
2005-11-03, by huffman
add constant one_when; LAM pattern for ONE
2005-11-03, by huffman
add translation for wildcard pattern
2005-11-03, by huffman
change syntax for LAM to use expressions as patterns; define LAM pattern syntax for cpair, spair, sinl, sinr, up
2005-11-03, by huffman
make cpair_less, cpair_defined_iff into iff rules; add lemma csplit1
2005-11-03, by huffman
cleaned up; ch2ch_Rep_CFun is a simp rule
2005-11-03, by huffman
changed iterate to a continuous type
2005-11-03, by huffman
reorganized; removed intermediate constant Ifix; changed iterate to a continuous type; added theorem fix_least_less
2005-11-03, by huffman
removed ex/loeckx.ML
2005-11-03, by huffman
removed proof about Ifix, which no longer exists
2005-11-03, by huffman
cleaned up; chain_const and thelub_const are simp rules
2005-11-03, by huffman
cleaned up; removed adm_tricks in favor of compactness theorems
2005-11-03, by huffman
fix spelling
2005-11-02, by huffman
Moved atom stuff to new file nominal_atoms.ML
2005-11-02, by berghofe
- completed the list of thms for supp_atm
2005-11-02, by urbanc
Added code for proving that new datatype has finite support.
2005-11-02, by berghofe
removed unused modify_typargs, map_typargs, fold_typargs;
2005-11-02, by wenzelm
added Isar.state/exn;
2005-11-02, by wenzelm
Isar.loop;
2005-11-02, by wenzelm
moved consts declarations to consts.ML;
2005-11-02, by wenzelm
Consts.dest;
2005-11-02, by wenzelm
Polymorphic constants.
2005-11-02, by wenzelm
added consts.ML;
2005-11-02, by wenzelm
fromConst: use Sign.const_typargs for efficient representation of type instances of constant declarations;
2005-11-02, by wenzelm
dist_eqI: the_context();
2005-11-02, by wenzelm
Sign.const_monomorphic;
2005-11-02, by wenzelm
Logic.nth_prem;
2005-11-02, by wenzelm
added the collection of lemmas "supp_at"
2005-11-02, by urbanc
some minor tweaks in some proofs (nothing extraordinary)
2005-11-01, by urbanc
tunings of some comments (nothing serious)
2005-11-01, by urbanc
nth_*, fold_index refined
2005-10-31, by haftmann
fold_index replacing foldln
2005-10-31, by haftmann
A few new lemmas
2005-10-31, by nipkow
tuned my last commit
2005-10-30, by urbanc
simplified the abs_supp_approx proof and tuned some comments in
2005-10-30, by urbanc
Changed Simplifier.simp_modifiers to Simplifier.simp_modifiers'.
2005-10-29, by urbanc
1) have adjusted the swapping of the result type
2005-10-29, by urbanc
tuned;
2005-10-28, by wenzelm
lthms_containing: not o valid_thms;
2005-10-28, by wenzelm
added fact_tac, some_fact_tac;
2005-10-28, by wenzelm
renamed Goal constant to prop, more general protect/unprotect interfaces;
2005-10-28, by wenzelm
renamed Goal constant to prop, more general protect/unprotect interfaces;
2005-10-28, by wenzelm
added fact method;
2005-10-28, by wenzelm
tuned ProofContext.export interfaces;
2005-10-28, by wenzelm
syntax for literal facts;
2005-10-28, by wenzelm
removed try_dest_Goal, use Logic.unprotect;
2005-10-28, by wenzelm
added cgoal_of;
2005-10-28, by wenzelm
accomodate simplified Thm.lift_rule;
2005-10-28, by wenzelm
export cong_modifiers, simp_modifiers';
2005-10-28, by wenzelm
certify_term: tuned monomorphic consts;
2005-10-28, by wenzelm
datatype thmref: added Fact;
2005-10-28, by wenzelm
Logic.lift_all;
2005-10-28, by wenzelm
renamed Goal constant to prop, more general protect/unprotect interfaces;
2005-10-28, by wenzelm
renamed Goal.norm_hhf_rule to Goal.norm_hhf;
2005-10-28, by wenzelm
renamed Goal constant to prop, more general protect/unprotect interfaces;
2005-10-28, by wenzelm
added add_local/add_global;
2005-10-28, by wenzelm
added incr_indexes;
2005-10-28, by wenzelm
renamed Goal constant to prop;
2005-10-28, by wenzelm
accomodate simplified Thm.lift_rule;
2005-10-28, by wenzelm
Logic.unprotect;
2005-10-28, by wenzelm
literal facts;
2005-10-28, by wenzelm
* Pure/Isar: literal facts;
2005-10-28, by wenzelm
tuned;
2005-10-28, by wenzelm
unnecessary imports removed
2005-10-28, by webertj
fixed case names in the weak induction principle and
2005-10-28, by urbanc
Implemented proof of weak induction theorem.
2005-10-28, by berghofe
Added "deepen" method.
2005-10-28, by berghofe
circumvented smlnj value restriction
2005-10-28, by haftmann
added extraction interface for code generator
2005-10-28, by haftmann
Added (optional) arguments to the tactics
2005-10-28, by urbanc
cleaned up nth, nth_update, nth_map and nth_string functions
2005-10-28, by haftmann
Removed legacy prove_goalw_cterm command.
2005-10-28, by berghofe
got rid of obsolete prove_goalw_cterm
2005-10-28, by paulson
swapped add_datatype result
2005-10-28, by haftmann
removed obfuscating PStrStrTab
2005-10-28, by haftmann
reachable - abandoned foldl_map in favor of fold_map
2005-10-28, by haftmann
Added Tools/res_hol_clause.ML
2005-10-28, by mengj
Added a new file res_hol_clause.ML to Reconstruction.thy. This file is used to translate HOL formulae into FOL clauses.
2005-10-28, by mengj
Added "writeln_strs" to the signature
2005-10-28, by mengj
Added several new functions that are used to prove HOL goals. Added new methods "vampireH" and "eproverH" that can prove both FOL and HOL goals. The old "vampire" and "eprover" methods are renamed to "vampireF" and "eproverF"; they can only prove FOL goals.
2005-10-28, by mengj
Added new functions to handle HOL goals and lemmas.
2005-10-28, by mengj
Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names.
2005-10-28, by mengj
Added several functions to the signature.
2005-10-28, by mengj
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
2005-10-28, by mengj
sorted lemma lists
2005-10-27, by paulson
* HOL: alternative iff syntax;
2005-10-27, by wenzelm
consts: monomorphic;
2005-10-27, by wenzelm
removed inappropriate monomorphic test;
2005-10-27, by wenzelm
replaced Defs.monomorphic by Sign.monomorphic;
2005-10-27, by wenzelm
alternative iff syntax for equality on booleans, with print_mode 'iff';
2005-10-27, by wenzelm
added module Pure/General/rat.ML
2005-10-27, by haftmann
tidied away duplicate thm
2005-10-26, by paulson
EVERY;
2005-10-25, by wenzelm
traceIt: plain term;
2005-10-25, by wenzelm
val legacy = ref false;
2005-10-25, by wenzelm
prove_raw: cterms, explicit asms;
2005-10-25, by wenzelm
avoid legacy goals;
2005-10-25, by wenzelm
legacy = ref true for the time being -- avoid volumious warnings;
2005-10-22, by wenzelm
tuned;
2005-10-21, by wenzelm
avoid OldGoals shortcuts;
2005-10-21, by wenzelm
* Legacy goal package: reduced interface to the bare minimum required to keep existing proof scripts running.
2005-10-21, by wenzelm
Internal goals.
2005-10-21, by wenzelm
renamed triv_goal to goalI, rev_triv_goal to goalD;
2005-10-21, by wenzelm
tuned header;
2005-10-21, by wenzelm
Goal.norm_hhf_rule;
2005-10-21, by wenzelm
export add_binds_i;
2005-10-21, by wenzelm
load_file: setmp OldGoals.legacy true;
2005-10-21, by wenzelm
improved check_result;
2005-10-21, by wenzelm
Goal.prove_plain;
2005-10-21, by wenzelm
do not export find_thms;
2005-10-21, by wenzelm
use obsolete goals.ML here;
2005-10-21, by wenzelm
Goal.conclude;
2005-10-21, by wenzelm
moved SELECT_GOAL to goal.ML;
2005-10-21, by wenzelm
moved norm_hhf_rule, prove etc. to goal.ML;
2005-10-21, by wenzelm
added simplification tactics and rules (from meta_simplifier.ML);
2005-10-21, by wenzelm
moved various simplification tactics and rules to simplifier.ML;
2005-10-21, by wenzelm
warn_obsolete for goal commands -- danger of disrupting a local proof context;
2005-10-21, by wenzelm
renamed triv_goal to goalI, rev_triv_goal to goalD;
2005-10-21, by wenzelm
added goal.ML;
2005-10-21, by wenzelm
added goal.ML;
2005-10-21, by wenzelm
Goal.norm_hhf_rule, Goal.init;
2005-10-21, by wenzelm
avoid triv_goal and home-grown meta_allE;
2005-10-21, by wenzelm
OldGoals;
2005-10-21, by wenzelm
proper header;
2005-10-21, by wenzelm
avoid home-grown meta_allE;
2005-10-21, by wenzelm
Goal.prove;
2005-10-21, by wenzelm
avoid shortcuts from OldGoals;
2005-10-21, by wenzelm
added simplified settings for Poly/ML 4.x (commented out);
2005-10-21, by wenzelm
reverted (accidental?) change of 1.148;
2005-10-21, by wenzelm
abandoned rational number functions in favor of General/rat.ML
2005-10-21, by haftmann
introduced functions from Pure/General/rat.ML
2005-10-21, by haftmann
slight corrections
2005-10-21, by haftmann
substantially improved integration of website into distribution framework
2005-10-21, by haftmann
substantially improved integration of website into distribution framework
2005-10-21, by haftmann
substantially improved integration of website into distribution framework
2005-10-21, by haftmann
substantially improved integration of website into distribution framework
2005-10-21, by haftmann
towards an improved website/makedist integration
2005-10-21, by haftmann
towards an improved website/makedist integration
2005-10-21, by haftmann
added default distinfo.mak
2005-10-21, by haftmann
towards an improved website/makedist integration
2005-10-21, by haftmann
towards an improved website/makedist integration
2005-10-21, by haftmann
added rounding functions
2005-10-21, by haftmann
Merged theory ResAtpOracle.thy into ResAtpMethods.thy
2005-10-21, by mengj
obsolete;
2005-10-19, by wenzelm
removed add_inductive_x;
2005-10-19, by wenzelm
removed obsolete add_datatype_x;
2005-10-19, by wenzelm
removed obsolete thy_syntax.ML;
2005-10-19, by wenzelm
removed obsolete old_symbol_source;
2005-10-19, by wenzelm
removed obsolete non-Isar theory format and old Isar theory headers;
2005-10-19, by wenzelm
removed old-style theory format;
2005-10-19, by wenzelm
avoid lagacy read function;
2005-10-19, by wenzelm
added thm(s) retrieval functions (from goals.ML);
2005-10-19, by wenzelm
removed obsolete old-locales;
2005-10-19, by wenzelm
removed obsolete axclass_tac, add_inst_subclass_x, add_inst_arity_x;
2005-10-19, by wenzelm
removed obsolete Thy/thy_parse.ML, Thy/thy_scan.ML, Thy/thy_syn.ML;
2005-10-19, by wenzelm
removed obsolete old-style syntax;
2005-10-19, by wenzelm
removed obsolete IOA/meta_theory/ioa_package.ML;
2005-10-19, by wenzelm
removed obsolete domain/interface.ML, IOA/meta_theory/ioa_package.ML;
2005-10-19, by wenzelm
removed obsolete domain/interface.ML;
2005-10-19, by wenzelm
removed obsolete add_typedef_x;
2005-10-19, by wenzelm
removed print_exn (better let the toplevel do this);
2005-10-19, by wenzelm
removed obsolete add_recdef_old;
2005-10-19, by wenzelm
removed obsolete HOL/thy_syntax.ML;
2005-10-19, by wenzelm
* Theory syntax: discontinued non-Isar format and old Isar headers;
2005-10-19, by wenzelm
replaced commafy by existing commas;
2005-10-19, by wenzelm
updated;
2005-10-19, by wenzelm
isatool fixheaders;
2005-10-19, by wenzelm
fix headers;
2005-10-19, by wenzelm
added table functor instance for pairs of strings
2005-10-19, by haftmann
added subgraph
2005-10-19, by haftmann
added join
2005-10-19, by haftmann
slight improvements for website
2005-10-19, by haftmann
moved VAMPIRE_HOME, E_HOME to section "External reasoning tools" -- commented out by default!
2005-10-19, by wenzelm
More functions are added to the signature of ResClause
2005-10-19, by mengj
*** empty log message ***
2005-10-19, by mengj
added 2 lemmas
2005-10-19, by nipkow
Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
2005-10-19, by mengj
simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
2005-10-18, by wenzelm
tuned error msg;
2005-10-18, by wenzelm
renamed atomize_rule to atomize_cterm;
2005-10-18, by wenzelm
ObjectLogic.atomize_cterm;
2005-10-18, by wenzelm
use simplified Toplevel.proof etc.;
2005-10-18, by wenzelm
back: Toplevel.actual/skip_proof;
2005-10-18, by wenzelm
renamed set_context to context;
2005-10-18, by wenzelm
renamed set_context to context;
2005-10-18, by wenzelm
functor: no Simplifier argument;
2005-10-18, by wenzelm
moved helper lemma to HilbertChoice.thy;
2005-10-18, by wenzelm
Simplifier.theory_context;
2005-10-18, by wenzelm
added lemma exE_some (from specification_package.ML);
2005-10-18, by wenzelm
Simplifier.theory_context;
2005-10-18, by wenzelm
tuned error msg;
2005-10-18, by wenzelm
Simplifier.context/theory_context;
2005-10-18, by wenzelm
updated;
2005-10-18, by wenzelm
new interface to make_conjecture_clauses
2005-10-18, by paulson
* Simplifier: simpset of a running simplification process contains a proof context;
2005-10-17, by wenzelm
added type_solver (uses Simplifier.the_context);
2005-10-17, by wenzelm
added pos/negDivAlg_induct declarations (from Main.thy);
2005-10-17, by wenzelm
moved pos/negDivAlg_induct declarations to Integ/IntDiv.thy;
2005-10-17, by wenzelm
removed obsolete/experimental context components (superceded by Simplifier.the_context);
2005-10-17, by wenzelm
added set/addloop' for simpset dependent loopers;
2005-10-17, by wenzelm
functor: no Simplifier argument;
2005-10-17, by wenzelm
change_claset(_of): more abtract interface;
2005-10-17, by wenzelm
functor: no Simplifier argument;
2005-10-17, by wenzelm
tuned;
2005-10-17, by wenzelm
Simplifier.inherit_context instead of Simplifier.inherit_bounds;
2005-10-17, by wenzelm
change_claset/simpset;
2005-10-17, by wenzelm
change_claset/simpset;
2005-10-17, by wenzelm
Improved proof of injectivity theorems to make it work on
2005-10-17, by berghofe
Fixed bug in proof of support theorem (it failed on constructors with no arguments).
2005-10-17, by berghofe
Implemented proofs for support and freshness theorems.
2005-10-17, by berghofe
deleted leading space in the definition of fresh
2005-10-17, by urbanc
Initial revision.
2005-10-17, by berghofe
tuned;
2005-10-15, by wenzelm
tuned comment;
2005-10-15, by wenzelm
added ML_type, ML_struct;
2005-10-15, by wenzelm
more;
2005-10-15, by wenzelm
* antiquotations ML_type, ML_struct;
2005-10-15, by wenzelm
added guess;
2005-10-15, by wenzelm
added antiquotations ML_type, ML_struct;
2005-10-15, by wenzelm
use perl for test/stat;
2005-10-15, by wenzelm
export strip_params;
2005-10-15, by wenzelm
note_thmss, read/cert_vars etc.: natural argument order;
2005-10-15, by wenzelm
goal statements: before_qed argument;
2005-10-15, by wenzelm
added 'guess', which derives the obtained context from the course of reasoning;
2005-10-15, by wenzelm
added primitive_text, succeed_text;
2005-10-15, by wenzelm
goal statements: accomodate before_qed argument;
2005-10-15, by wenzelm
goal statements: accomodate before_qed argument;
2005-10-15, by wenzelm
added 'guess';
2005-10-15, by wenzelm
tuned;
2005-10-15, by wenzelm
added no_facts;
2005-10-15, by wenzelm
tuned comments;
2005-10-15, by wenzelm
updated;
2005-10-15, by wenzelm
signature changes
2005-10-14, by paulson
added module rat.ML for rational numbers
2005-10-14, by haftmann
longer time out for test (kleing)
2005-10-14, by isatest
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
2005-10-14, by paulson
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
2005-10-14, by paulson
obsolete;
2005-10-13, by wenzelm
counter added to SAT signature
2005-10-12, by webertj
no proof reconstruction when quick_and_dirty is set
2005-10-12, by webertj
tidying
2005-10-12, by paulson
domain package generates compactness lemmas for new constructors
2005-10-12, by huffman
add ML bindings for compactness lemmas
2005-10-12, by huffman
added compactness theorems
2005-10-12, by huffman
added compactness lemmas; cleaned up
2005-10-12, by huffman
added compactness theorems in locale iso
2005-10-11, by huffman
added several theorems in locale iso
2005-10-11, by huffman
added xsymbols syntax for pairs; cleaned up
2005-10-11, by huffman
added theorem typedef_compact
2005-10-11, by huffman
rearranged subsections; added theorems expand_cfun_eq, expand_cfun_less
2005-10-11, by huffman
cleaned up; renamed less_fun to expand_fun_less
2005-10-11, by huffman
added hd lemma
2005-10-11, by nipkow
simplifying the treatment of clausification
2005-10-11, by paulson
simplifying the treatment of nameless theorems
2005-10-11, by paulson
expand: error on undefined/empty env variable;
2005-10-11, by wenzelm
added assert;
2005-10-11, by wenzelm
tuned;
2005-10-11, by wenzelm
added string_of_pid;
2005-10-11, by wenzelm
raw symbols: allow non-ASCII chars (e.g. UTF-8);
2005-10-11, by wenzelm
moved string_of_pid to ML-Systems;
2005-10-11, by wenzelm
ML_SUFFIX in targets (experimental);
2005-10-11, by wenzelm
cleanup backup images;
2005-10-11, by wenzelm
small tidy-up of utility functions
2005-10-10, by paulson
updated print_tac;
2005-10-10, by wenzelm
add names to infix declarations
2005-10-10, by huffman
new syntax translations for continuous lambda abstraction
2005-10-10, by huffman
removed Istrictify; simplified some proofs
2005-10-10, by huffman
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
2005-10-10, by huffman
cleaned up
2005-10-10, by huffman
added theorem typedef_chfin
2005-10-10, by huffman
replaced foldr' with foldr1
2005-10-10, by huffman
cleaned up; renamed "Porder.op <<" to "Porder.<<"
2005-10-10, by huffman
Tactics sat and satx reimplemented, several improvements
2005-10-09, by webertj
tuned Memory.hilim;
2005-10-08, by wenzelm
get rid of feeder -- at the cost of batch-only commit-at-exit;
2005-10-08, by wenzelm
*** empty log message ***
2005-10-08, by nipkow
-nort option;
2005-10-08, by wenzelm
added could_unify;
2005-10-08, by wenzelm
more efficient check_specified, much less invocations;
2005-10-08, by wenzelm
moved susp.ML, lazy_seq.ML, lazy_scan.ML to HOL/Import;
2005-10-08, by wenzelm
uses susp.ML, lazy_seq.ML, lazy_scan.ML;
2005-10-08, by wenzelm
added Import/susp.ML, Import/lazy_seq.ML, Import/lasy_scan.ML;
2005-10-08, by wenzelm
minor tweaks for Poplog/PML;
2005-10-08, by wenzelm
tuned memory limits;
2005-10-08, by wenzelm
Int.max;
2005-10-08, by wenzelm
minor tweaks for Poplog/PML;
2005-10-08, by wenzelm
minor tweaks for Poplog/PML;
2005-10-08, by wenzelm
initial pop11 code for ML use/use_string;
2005-10-08, by wenzelm
Poplog/PML: ML_SUFFIX=.psv;
2005-10-08, by wenzelm
support ML_SUFFIX;
2005-10-08, by wenzelm
obsolete;
2005-10-08, by wenzelm
fix due to new neq_simproc
2005-10-08, by nipkow
removed obsolete comment;
2005-10-07, by wenzelm
added idtypdummy_ast_tr;
2005-10-07, by wenzelm
added syntax for _idtdummy, _idtypdummy;
2005-10-07, by wenzelm
added absdummy;
2005-10-07, by wenzelm
removed obsolete dummy_pat_tr;
2005-10-07, by wenzelm
Term.absdummy;
2005-10-07, by wenzelm
removed obsolete ex/Tuple.thy;
2005-10-07, by wenzelm
replaced _K by dummy abstraction;
2005-10-07, by wenzelm
print_translation: does not handle _idtdummy;
2005-10-07, by wenzelm
tuned;
2005-10-07, by wenzelm
added dummy variable binding;
2005-10-07, by wenzelm
changes due to new neq_simproc in simpdata.ML
2005-10-07, by nipkow
added str_of_term (from HOL/Tools/ATP/recon_translate_proof.ML);
2005-10-07, by wenzelm
Term.str_of_term;
2005-10-07, by wenzelm
minor code tidyig
2005-10-07, by paulson
code restructuring
2005-10-07, by paulson
more tidying. Fixed process management bugs and race condition
2005-10-07, by paulson
major simplification: removal of the goalstring argument
2005-10-06, by paulson
Optimized getPreds and getSuccs.
2005-10-06, by berghofe
adjusted sydney to new website
2005-10-06, by haftmann
changed sydney share
2005-10-06, by haftmann
added Poplog/PML version 15.6/2.1 (experimental!);
2005-10-05, by wenzelm
added fold_nodes, map_node_yield
2005-10-05, by haftmann
added merge, tuned
2005-10-05, by haftmann
added last in set lemma
2005-10-05, by nipkow
improved process handling. tidied
2005-10-05, by paulson
more signals
2005-10-05, by paulson
new hd/rev/last lemmas
2005-10-04, by nipkow
new lemmas
2005-10-04, by nipkow
added compiler and runtime options;
2005-10-04, by wenzelm
Poplog/PML startup script.
2005-10-04, by wenzelm
Compatibility file for Poplog/PML (version 15.6/2.1).
2005-10-04, by wenzelm
Substring.all = Substring.full;
2005-10-04, by wenzelm
minor tweaks for Poplog/ML;
2005-10-04, by wenzelm
find_theorems: support * wildcard in name: criterion;
2005-10-04, by wenzelm
* Command 'find_theorems': support * wildcard in name: criterion.
2005-10-04, by wenzelm
Patch for PolyML 4.1.4 to make it work with Isabelle2005. We commit this into ML_dbase!
2005-10-04, by wenzelm
added redirect.html
2005-10-04, by haftmann
better error handling
2005-10-04, by haftmann
improved linktest
2005-10-04, by haftmann
removed removed IntFloor
2005-10-04, by haftmann
fixed broken link
2005-10-04, by haftmann
fixed broken mailto: link
2005-10-04, by haftmann
fixed the ascii-armouring of goalstring
2005-10-04, by paulson
reset clause counter
2005-10-04, by paulson
theorems need names
2005-10-04, by paulson
support for setting local permissions
2005-10-04, by haftmann
improved dependency build
2005-10-04, by haftmann
added conf/ to .cvsignore
2005-10-04, by haftmann
Add icon for interface. Isabelle2005
2005-09-30, by aspinall
Move welcomemsg and helpdoc to pgip_isar.xml
2005-09-30, by aspinall
Add helpdocs and welcomemsg here instead of hard wiring in proof_general.ML.
2005-09-30, by aspinall
Explanatory text
2005-09-30, by aspinall
Schema files (for information, and validating pgip_isar.xml)
2005-09-30, by aspinall
Schema for PGIP
2005-09-30, by aspinall
pruned notes about Poly/ML;
2005-09-30, by wenzelm
converted to Isar theory format;
2005-09-30, by wenzelm
Initialise pgip id also for Emacs mode. Allow dynamic config file location for PGIP.
2005-09-30, by aspinall
tuned;
2005-09-30, by wenzelm
Fix for guiconfig -> displayconfig element rename
2005-09-30, by aspinall
theorems need names
2005-09-30, by paulson
refer to $PRG instead of (old) rsync-isabelle;
2005-09-29, by wenzelm
updated;
2005-09-29, by wenzelm
updated;
2005-09-29, by wenzelm
pdfsetup.sty: better not rely on ifpdf.sty;
2005-09-29, by wenzelm
simprules need names
2005-09-29, by paulson
export debug_bounds;
2005-09-29, by wenzelm
explicit dependencies of SAT vs. Refute;
2005-09-29, by wenzelm
explicit dependencies of SAT vs. Refute;
2005-09-29, by wenzelm
Isabelle2005 (October 2005);
2005-09-29, by wenzelm
Added a few lemmas
2005-09-29, by nipkow
reduction in tracing files
2005-09-29, by paulson
improvements for problem generation
2005-09-29, by paulson
moved concat_with_and to watcher.ML
2005-09-29, by paulson
a name for empty_not_insert
2005-09-29, by paulson
Simplifier now removes flex-flex constraints from theorem returned by prover.
2005-09-29, by berghofe
Optimized and exported flexflex_unique.
2005-09-29, by berghofe
make signature constraint actually work;
2005-09-29, by wenzelm
activate signature constraints;
2005-09-29, by wenzelm
HOL4 image is back;
2005-09-29, by wenzelm
tuned default operation: use internal modify;
2005-09-29, by wenzelm
abstract_rule: tuned exception msgs;
2005-09-29, by wenzelm
back to simple 'defs' (cf. revision 1.79 of theory.ML);
2005-09-29, by wenzelm
back to simple 'defs' (cf. revision 1.79);
2005-09-29, by wenzelm
removed revert_bound;
2005-09-29, by wenzelm
print_theory: discontinued final consts;
2005-09-29, by wenzelm
Theory.add_finals_i;
2005-09-29, by wenzelm
more finalconsts;
2005-09-29, by wenzelm
tuned;
2005-09-29, by wenzelm
pointer to HOL/ex/SAT_Examples.thy added
2005-09-28, by webertj
updated;
2005-09-28, by wenzelm
more reliable check for PDF output using ifpdf.sty;
2005-09-28, by wenzelm
pre_sat_tac moved towards end of file
2005-09-28, by webertj
adjusted www links
2005-09-28, by haftmann
comment fixed
2005-09-28, by webertj
mapped "-->" to "hol4-->"
2005-09-28, by obua
avoid naming existing tags in explanations;
2005-09-28, by wenzelm
revert 'defs' advertisement;
2005-09-28, by wenzelm
revert 'defs' advertisement;
2005-09-28, by wenzelm
time limit option; fixed bug concerning first line of ATP output
2005-09-28, by paulson
streamlined theory; conformance to recent publication
2005-09-28, by paulson
new lemma
2005-09-28, by paulson
better appearance in lynx and netscape4
2005-09-28, by haftmann
MB instead of KB
2005-09-28, by haftmann
renamed packages to download;
2005-09-27, by wenzelm
more details about incomplete 'defs';
2005-09-27, by wenzelm
renamed "Packages" to "Download";
2005-09-27, by wenzelm
build bed
2005-09-27, by haftmann
build bed
2005-09-27, by haftmann
build bed
2005-09-27, by haftmann
slight corrections
2005-09-27, by haftmann
tuned;
2005-09-27, by wenzelm
renamed "Packages" to "Download";
2005-09-27, by wenzelm
fixed dead link
2005-09-27, by haftmann
fixed dead link
2005-09-27, by haftmann
improved linkcheck
2005-09-27, by haftmann
added simple linktester for isabelle website
2005-09-27, by haftmann
warn about Poly/ML segfault problem;
2005-09-27, by wenzelm
website preparation for Isabelle2005
2005-09-27, by haftmann
corrected spelling bug
2005-09-27, by obua
added defs disclaimer
2005-09-27, by obua
nat_number_of is no longer declared as code lemma, since this turned
2005-09-27, by berghofe
Inserted clause for nat in number_of_codegen again ("code unfold" turned
2005-09-27, by berghofe
Optimized unfold_attr.
2005-09-27, by berghofe
removed link to HOL4, which is not in the library right now;
2005-09-27, by wenzelm
tuned;
2005-09-27, by wenzelm
Added entries for code_module, code_library, and value.
2005-09-27, by berghofe
Tuned.
2005-09-27, by berghofe
updates for Isabelle2005;
2005-09-26, by wenzelm
tuned;
2005-09-26, by wenzelm
Updated description of code generator.
2005-09-26, by berghofe
updated;
2005-09-26, by wenzelm
moved disambiguate_frees to ProofKernel;
2005-09-26, by wenzelm
quote 'value';
2005-09-26, by wenzelm
yet another atempt to get doc/Contents right;
2005-09-26, by wenzelm
Renamed wf_rec to wfrec in consts_code declaration.
2005-09-26, by berghofe
really copy doc/Contents;
2005-09-26, by wenzelm
Release HOL4 and HOLLight Importer.
2005-09-26, by obua
copy doc/Contents;
2005-09-26, by wenzelm
Made sure all lemmas now have names (especially so that certain of them
2005-09-26, by skalberg
echo HOL_USERDIR_OPTIONS;
2005-09-26, by wenzelm
tuned
2005-09-26, by obua
added ROOT.ML
2005-09-26, by obua
adjusted web link
2005-09-26, by haftmann
added entry for running HOLLight
2005-09-26, by obua
fixed disambiguation problem
2005-09-26, by obua
added Drule.disambiguate_frees : thm -> thm
2005-09-26, by obua
zero_var_inst: replace loose bounds :000 etc.;
2005-09-25, by wenzelm
* Hyperreal: A theory of Taylor series.
2005-09-25, by wenzelm
more;
2005-09-25, by wenzelm
eq_codegen now ensures that code for bool type is generated.
2005-09-25, by berghofe
Fixed print mode problem in test_term.
2005-09-25, by berghofe
Added ExecutableSet and Taylor.
2005-09-25, by berghofe
Now uses set implementation from ExecutableSet.
2005-09-25, by berghofe
Added Taylor.
2005-09-25, by berghofe
Formalization of Taylor series by Lukas Bulwahn and
2005-09-25, by berghofe
Added ExecutableSet.
2005-09-25, by berghofe
New theory for implementing finite sets by lists.
2005-09-25, by berghofe
sat_solver.ML not loaded anymore (already loaded by Refute.thy)
2005-09-25, by webertj
set show_types and show_sorts during import
2005-09-24, by obua
a few new filter lemmas
2005-09-24, by nipkow
HOL4-Import: map ONTO to Fun.surj
2005-09-24, by obua
cnf_struct renamed to cnf
2005-09-24, by webertj
remove debug clutter
2005-09-24, by obua
preliminary fix of HOL build problem
2005-09-24, by obua
bug fix
2005-09-24, by obua
replay_proof optimized: now performs backwards proof search
2005-09-24, by webertj
code reformatted and restructured, many minor modifications
2005-09-24, by webertj
bugfix in "zchaff_with_proofs"
2005-09-24, by webertj
parse_std_result_file renamed to read_std_result_file
2005-09-24, by webertj
new sat tactic
2005-09-23, by webertj
new sat tactic imports resolution proofs from zChaff
2005-09-23, by webertj
fix
2005-09-23, by obua
simprocs: pattern now "x" (the proc is supposed to discriminate faster than Pattern.match);
2005-09-23, by wenzelm
tuned msg;
2005-09-23, by wenzelm
added mk_solver';
2005-09-23, by wenzelm
Simplifier.inherit_bounds;
2005-09-23, by wenzelm
adm_tac/cont_tacRs: proper simpset;
2005-09-23, by wenzelm
Provers/Arith/fast_lin_arith.ML: Simplifier.inherit_bounds;
2005-09-23, by wenzelm
tuned order of targets;
2005-09-23, by wenzelm
Provers/cancel_sums.ML: Simplifier.inherit_bounds;
2005-09-23, by wenzelm
some typos in comments fixed
2005-09-23, by webertj
1) fixed bug in type_introduction: first stage uses different namespace than second stage
2005-09-23, by obua
removed doc/index.html from distribution (now produced by website);
2005-09-23, by wenzelm
mkdir -p for symlinks
2005-09-23, by haftmann
rules -> iprover
2005-09-23, by nipkow
spaces inserted in header
2005-09-23, by webertj
header (title/ID) added
2005-09-23, by webertj
typo fixed: rufute -> refute
2005-09-23, by webertj
bugfix in record_tr'
2005-09-23, by schirmer
method 'rules' renamed to 'iprover', which does *not* retrieve theorems from the Internet;
2005-09-23, by wenzelm
Id;
2005-09-23, by wenzelm
tuned;
2005-09-23, by wenzelm
changed defaults
2005-09-23, by paulson
ATP linkup
2005-09-23, by paulson
replay type_introduction fix
2005-09-23, by obua
temporarily re-introduced overwrite_warn
2005-09-23, by haftmann
add debug messages
2005-09-23, by obua
renamed rules to iprover
2005-09-23, by nipkow
*** empty log message ***
2005-09-23, by nipkow
renamed rules to iprover
2005-09-22, by nipkow
fix because of list lemmas
2005-09-22, by nipkow
renamed "rules" to "iprover"
2005-09-22, by nipkow
added theorem adm_ball
2005-09-22, by huffman
cleaned up
2005-09-22, by huffman
HOLCF theorem naming conventions
2005-09-22, by huffman
removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
2005-09-22, by paulson
Fix because of new lemma in List
2005-09-22, by nipkow
solver "auto" does not reverse the list of solvers anymore
2005-09-22, by webertj
added fold_map_graph
2005-09-22, by haftmann
added fold_map_table
2005-09-22, by haftmann
only show trunk in Changelog (kleing)
2005-09-22, by isatest
zchaff_with_proofs does not delete zChaff\s resolve_trace file anymore
2005-09-21, by webertj
echo HOL_USEDIR_OPTIONS;
2005-09-21, by wenzelm
tuned;
2005-09-21, by wenzelm
PROOFGENERAL_OPTIONS: smart fall-back on plain emacs (back again);
2005-09-21, by wenzelm
updated for Isabelle2005;
2005-09-21, by wenzelm
tuned;
2005-09-21, by wenzelm
updated for Isabelle2005;
2005-09-21, by wenzelm
obsolete;
2005-09-21, by wenzelm
improved proof parsing
2005-09-21, by paulson
trying to limit the looping
2005-09-21, by paulson
updated for Isabelle2005;
2005-09-21, by wenzelm
new header syntax;
2005-09-21, by wenzelm
introduces update_warn instead of overwrite_warn
2005-09-21, by haftmann
added AList.make, eq_fst, apr ...
2005-09-21, by haftmann
unify dist and main
2005-09-21, by haftmann
tuned;
2005-09-21, by wenzelm
fixed cvs export;
2005-09-21, by wenzelm
tuned;
2005-09-21, by wenzelm
obsolete;
2005-09-21, by wenzelm
tuned;
2005-09-21, by wenzelm
the_default, the_list;
2005-09-21, by wenzelm
updated;
2005-09-21, by wenzelm
quote "value";
2005-09-21, by wenzelm
removed "--" argument;
2005-09-21, by wenzelm
isatool fixheaders;
2005-09-21, by wenzelm
Added new "value" command.
2005-09-21, by berghofe
Simplified code generator for numerals.
2005-09-21, by berghofe
Declared nat_number_of as code lemma.
2005-09-21, by berghofe
- Added eval_term function and value command
2005-09-21, by berghofe
tunes;
2005-09-21, by wenzelm
updated for Isabelle2005;
2005-09-21, by wenzelm
HOL-Complex-Matrix: fixed deps;
2005-09-21, by wenzelm
tuned;
2005-09-21, by wenzelm
updated for Isabelle2005;
2005-09-21, by wenzelm
tuned;
2005-09-21, by wenzelm
(name mess cleanup)
2005-09-21, by haftmann
introduced AList module
2005-09-21, by haftmann
removed assoc, overwrite
2005-09-21, by haftmann
added update_warn
2005-09-21, by haftmann
tuned;
2005-09-21, by wenzelm
fixed proof script of lemma merges_same_conv (Why did it stop working?);
2005-09-20, by wenzelm
updated;
2005-09-20, by wenzelm
tuned;
2005-09-20, by wenzelm
HOL/ex/Chinese.thy;
2005-09-20, by wenzelm
tuned;
2005-09-20, by wenzelm
more contributions;
2005-09-20, by wenzelm
tuned headers;
2005-09-20, by wenzelm
tuned header;
2005-09-20, by wenzelm
use "ML-Systems/smlnj-basis-compat.ML" *after* Interrupt;
2005-09-20, by wenzelm
fixed proof script of lemma Cond_sound (Why did it stop working anyway?);
2005-09-20, by wenzelm
bugfix in "zchaff_with_proofs"
2005-09-20, by webertj
fixed recursive-looking declaration
2005-09-20, by paulson
tidying, and support for axclass/classrel clauses
2005-09-20, by paulson
fixed syntax for sml/nj
2005-09-20, by paulson
undone the previous change: show_hyps not supported anymore
2005-09-20, by webertj
pointers to src/HOL/Tools/sat_solver.ML added in comments
2005-09-20, by webertj
introduced AList module in favor of assoc etc.
2005-09-20, by haftmann
new menu item show-sort-hypotheses to toggle show_hyps
2005-09-20, by webertj
HOL/ex/Chinese.thy;
2005-09-20, by wenzelm
HOL-ex: Library/Commutative_Ring.thy;
2005-09-20, by wenzelm
moved Tools/comm_ring.ML to Library;
2005-09-20, by wenzelm
added Commutative_Ring (from Main HOL);
2005-09-20, by wenzelm
Simplifier.inherit_bounds;
2005-09-20, by wenzelm
TextIO.inputLine: handle IO.Io, assuming it stems from a signal;
2005-09-20, by wenzelm
get_interrupt: special handling of IO.io now in ML-Systems/smlnj-basis-compat.ML;
2005-09-20, by wenzelm
removed obsolete thms_containing;
2005-09-20, by wenzelm
tuned;
2005-09-20, by wenzelm
tuned simprocs;
2005-09-20, by wenzelm
removed Commutative_Ring hacks;
2005-09-20, by wenzelm
tuned theory dependencies;
2005-09-20, by wenzelm
removed Commutative_Ring.thy, added HOL/ex/Chinese.thy;
2005-09-20, by wenzelm
tuned;
2005-09-20, by wenzelm
Chinese Unicode example;
2005-09-20, by wenzelm
tuned proofs;
2005-09-20, by wenzelm
The simpset of the actual theory is take, in order to handle rings defined after the method
2005-09-20, by chaieb
further tidying; killing of old Watcher loops
2005-09-20, by paulson
added a number of lemmas
2005-09-20, by nipkow
uniform handling of interrupts
2005-09-20, by paulson
algebra method added.
2005-09-20, by chaieb
improved eq_fst and eq_snd, removed some deprecated stuff
2005-09-20, by haftmann
added make and find
2005-09-20, by haftmann
slight adaptions to library changes
2005-09-20, by haftmann
infix operator precedence
2005-09-20, by haftmann
using curried Inttab.update_new function now
2005-09-20, by webertj
SAT solver interface modified to support proofs of unsatisfiability
2005-09-19, by webertj
shrink: compress terms and types;
2005-09-19, by wenzelm
added String.isSuffix;
2005-09-19, by wenzelm
maybe the last bug fix (sigh)?
2005-09-19, by obua
Removed superfluous HOL/Matrix/cplex/ROOT.ML.
2005-09-19, by obua
further simplification of the Isabelle-ATP linkup
2005-09-19, by paulson
added make function
2005-09-19, by haftmann
removed some deprecated assocation list functions
2005-09-19, by haftmann
introduced AList module
2005-09-19, by haftmann
simplification of the Isabelle-ATP code; hooks for batch generation of problems
2005-09-19, by paulson
update usage message
2005-09-19, by kleing
obsolete;
2005-09-19, by wenzelm
converted to Isar theory format;
2005-09-18, by wenzelm
converted to Isar theory format;
2005-09-18, by wenzelm
converted to Isar theory format;
2005-09-17, by wenzelm
tuned;
2005-09-17, by wenzelm
converted to Isar theory format;
2005-09-17, by wenzelm
moved quick_and_dirty to Pure/ROOT.ML;
2005-09-17, by wenzelm
pretty_thm_aux: ora masked by quick_and_dirty;
2005-09-17, by wenzelm
added quick_and_dirty (from Isar/skip_proofs.ML);
2005-09-17, by wenzelm
manually generated from Isabelle/HOLCF/IOA/Complex/Import;
2005-09-17, by wenzelm
tuned document;
2005-09-17, by wenzelm
tuned;
2005-09-17, by wenzelm
added with_charset: string -> ('a -> 'b) -> 'a -> 'b;
2005-09-17, by wenzelm
tuned comments;
2005-09-17, by wenzelm
pretty_thm_aux: aconv hyps;
2005-09-17, by wenzelm
removed obsolete BasisLibrary;
2005-09-17, by wenzelm
Hebrew: HTML.with_charset;
2005-09-17, by wenzelm
removed obsolete BasisLibrary;
2005-09-17, by wenzelm
added quickcheck_params (from Main.thy);
2005-09-17, by wenzelm
removed spurious PolyML.exception_trace;
2005-09-17, by wenzelm
moved setup ResAxioms.clause_setup to Main.thy (it refers to all previous theories);
2005-09-17, by wenzelm
minor cleanup, moved stuff in its proper place;
2005-09-17, by wenzelm
generate: added HOL-Complex-Generate-HOLLight;
2005-09-17, by wenzelm
added code generator setup (from Main.thy);
2005-09-17, by wenzelm
lemmas [code] = imp_conv_disj (from Main.thy) -- Why does it need Datatype?
2005-09-17, by wenzelm
HTML.with_charset;
2005-09-17, by wenzelm
converted to Isar theory format;
2005-09-17, by wenzelm
tuned document;
2005-09-17, by wenzelm
obsolete;
2005-09-17, by wenzelm
plain test session, includes example;
2005-09-17, by wenzelm
theory_to_proof: check theory of initial proof state, which must not be changed;
2005-09-17, by wenzelm
added auto_fix (from proof.ML);
2005-09-17, by wenzelm
export put_facts;
2005-09-17, by wenzelm
interpretation: use goal commands without target -- no storing of results;
2005-09-17, by wenzelm
theorem(_i): empty target;
2005-09-17, by wenzelm
pretty_thm_aux: observe asms context;
2005-09-17, by wenzelm
tuned;
2005-09-17, by wenzelm
Cube: converted to Isar, use locales;
2005-09-17, by wenzelm
1) mapped .. and == constants
2005-09-17, by obua
use interpretation command
2005-09-17, by huffman
add HOLCF entries for pcpodef, cont_proc, fixrec;
2005-09-16, by huffman
converted to Isar theory format;
2005-09-16, by wenzelm
fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions
2005-09-16, by obua
add header
2005-09-16, by huffman
tuned
2005-09-16, by ballarin
interpretation uses primitive goal interface
2005-09-16, by ballarin
tuned
2005-09-16, by ballarin
PARTIAL conversion to Vampire8
2005-09-16, by paulson
catching exception Io
2005-09-16, by paulson
rearranged
2005-09-16, by huffman
use mem operator
2005-09-16, by huffman
fix names in hypreal_arith.ML
2005-09-16, by huffman
merge Hyperreal/Transfer.thy and Hyperreal/StarType.thy into Hyperreal/StarDef.thy
2005-09-15, by huffman
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
2005-09-15, by huffman
add header
2005-09-15, by huffman
The SMLNJ Problem fixed...
2005-09-15, by chaieb
getting it work for SMLNJ
2005-09-15, by chaieb
* Improved efficiency of the Simplifier etc.;
2005-09-15, by wenzelm
incorporated into NEWS;
2005-09-15, by wenzelm
incorporated HOL/Hyperreal/CHANGES;
2005-09-15, by wenzelm
massive tidy-up and simplification
2005-09-15, by paulson
moving Commutative_Ring to the correct theory
2005-09-15, by paulson
comment
2005-09-15, by paulson
poly -doDisplay;
2005-09-15, by wenzelm
TableFun/Symtab: curried lookup and update;
2005-09-15, by wenzelm
TableFun/Symtab: curried lookup and update;
2005-09-15, by wenzelm
fixed type;
2005-09-15, by wenzelm
fixed ML;
2005-09-15, by wenzelm
The Hebrew Alef-Bet -- Unicode example;
2005-09-15, by wenzelm
added Hebrew.thy;
2005-09-15, by wenzelm
TableFun/Symtab: curried lookup and update;
2005-09-15, by wenzelm
fixed document;
2005-09-15, by wenzelm
added HOL/ex/Hebrew.thy;
2005-09-15, by wenzelm
obsolete;
2005-09-15, by wenzelm
command 'thms_containing' has been discontinued in favour of 'find_theorems';
2005-09-15, by wenzelm
Revert previous attribute name change, problem can be avoided in JAXB.
2005-09-15, by aspinall
forget_proof: Sign.local_path o Sign.restore_naming ProtoPure.thy -- workaround to omission in locale goals;
2005-09-15, by wenzelm
extend: NameSpace.default_naming;
2005-09-15, by wenzelm
the experimental tagging system, and the usual tidying
2005-09-15, by paulson
Change PGIP attribute name class->messageclass to avoid Java keyword clash.
2005-09-15, by aspinall
AList, the_*
2005-09-15, by haftmann
fixed type annotation
2005-09-15, by haftmann
added gen_list to Pretty module
2005-09-15, by haftmann
@{term [source] ...} in subsections probably more robust;
2005-09-14, by wenzelm
tuned;
2005-09-14, by wenzelm
hide: added option '(open)';
2005-09-14, by wenzelm
imports Commutative_Ring instead of Main, since the latter hides our names;
2005-09-14, by wenzelm
hide the rather generic names used in theory Commutative_Ring;
2005-09-14, by wenzelm
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
2005-09-14, by wenzelm
... prem19
2005-09-14, by schirmer
added prem10 - prem19
2005-09-14, by schirmer
removed syntax fun_map_comp;
2005-09-14, by schirmer
Unfortunately patched to use IntInf.int instead of just int (SML compatibility)
2005-09-14, by chaieb
Method comm_ring for proving equalities in commutative rings.
2005-09-14, by wenzelm
tuned headers etc.;
2005-09-14, by wenzelm
fixed some ML names;
2005-09-14, by wenzelm
imports Commutative_Ring;
2005-09-14, by wenzelm
HOL: method comm_ring;
2005-09-14, by wenzelm
tuned;
2005-09-14, by wenzelm
no longer prefer xemacs, which fails more often than GNU emacs;
2005-09-14, by wenzelm
Bernhard Haeupler: comm_ring;
2005-09-14, by wenzelm
tactic and the rest eliminated, just the theory....
2005-09-14, by chaieb
use was wrong...
2005-09-14, by chaieb
Fixed Importer bug in type_introduction: instantiate type variables in rep-abs theorems exactly as it is done in HOL-light.
2005-09-14, by obua
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
2005-09-14, by chaieb
introduced AList.lookup
2005-09-14, by haftmann
correct E brackets
2005-09-14, by paulson
nice names for more infix operators
2005-09-14, by paulson
introduces AList.lookup
2005-09-14, by haftmann
removed duplicated lemmas; convert more proofs to transfer principle
2005-09-14, by huffman
add theorem chain_const
2005-09-13, by huffman
tuned;
2005-09-13, by wenzelm
global quick_and_dirty;
2005-09-13, by wenzelm
Printing of Isar proof elements etc.
2005-09-13, by wenzelm
Non-empty stacks.
2005-09-13, by wenzelm
IsarThy.begin_theory;
2005-09-13, by wenzelm
export ml_exts;
2005-09-13, by wenzelm
begin_theory: tuned interface, check uses;
2005-09-13, by wenzelm
replaced TRANSLATION_FAIL by EXCEPTION;
2005-09-13, by wenzelm
added three_buffersN, print3;
2005-09-13, by wenzelm
load before proof.ML;
2005-09-13, by wenzelm
added simple;
2005-09-13, by wenzelm
added add_view, export_view (supercedes adhoc view arguments);
2005-09-13, by wenzelm
major cleanup of interfaces and implementation;
2005-09-13, by wenzelm
added name_facts;
2005-09-13, by wenzelm
tuned Isar proof elements;
2005-09-13, by wenzelm
added cheating, sorry_text (from skip_proofs.ML);
2005-09-13, by wenzelm
load late, after proof.ML;
2005-09-13, by wenzelm
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
2005-09-13, by wenzelm
cleanup parsers and interfaces;
2005-09-13, by wenzelm
Proof.get_thmss;
2005-09-13, by wenzelm
tuned;
2005-09-13, by wenzelm
more self-contained proof elements (material from isar_thy.ML);
2005-09-13, by wenzelm
added cases, rule_contextN;
2005-09-13, by wenzelm
load locale.ML late (after proof.ML);
2005-09-13, by wenzelm
added maps, map_list, lift, lifts;
2005-09-13, by wenzelm
added stack.ML;
2005-09-13, by wenzelm
added simple_fact;
2005-09-13, by wenzelm
Seq.maps;
2005-09-13, by wenzelm
added hide_names(_i) (from isar_thy.ML);
2005-09-13, by wenzelm
added generic_setup, add_oracle (from isar_thy.ML);
2005-09-13, by wenzelm
added exception EXCEPTION of exn * string;
2005-09-13, by wenzelm
replaced DATA_FAIL by EXCEPTION;
2005-09-13, by wenzelm
tuned Isar interfaces;
2005-09-13, by wenzelm
added General/stack.ML, Isar/proof_display.ML;
2005-09-13, by wenzelm
the_list (cf. Pure/library.ML);
2005-09-13, by wenzelm
tuned IsarThy.theorem_i;
2005-09-13, by wenzelm
fixed INST: has same semantic now as INST_TYPE for repetitions
2005-09-13, by obua
list of constants and theorems whose names have been changed or merged
2005-09-12, by huffman
add header
2005-09-12, by huffman
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
2005-09-12, by huffman
updated to work with latest HOL-Complex
2005-09-12, by huffman
add file Hyperreal/transfer.ML
2005-09-12, by huffman
new implementation of transfer principle
2005-09-12, by huffman
removed clutter
2005-09-12, by obua
name conflict with global itrev resolved
2005-09-12, by nipkow
dealt with name clash with List.itrev
2005-09-12, by nipkow
introduced new-style AList operations
2005-09-12, by haftmann
introduced internal function hthm2thm
2005-09-12, by obua
1) Added target HOL-Complex-Generate-HOLLight
2005-09-12, by obua
Added HOLLight support to importer.
2005-09-12, by obua
added interact flag to control mode of excursions;
2005-09-12, by wenzelm
excursion: interactive if debug;
2005-09-11, by wenzelm
updated to work with new HOL-Complex version
2005-09-09, by huffman
starfun, starset, and other functions on NS types are now polymorphic;
2005-09-09, by huffman
Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
2005-09-09, by paulson
fixed printing of locales
2005-09-09, by ballarin
consolidation of duplicate code in Isabelle-ATP linkup
2005-09-08, by paulson
introduces some modern-style AList operations
2005-09-08, by haftmann
added the_list, the_default
2005-09-08, by haftmann
yet more tidying of Isabelle-ATP link
2005-09-08, by paulson
converted to Isar theory format;
2005-09-07, by wenzelm
converted to Isar theory format;
2005-09-07, by wenzelm
converted to Isar theory format;
2005-09-07, by wenzelm
removed TLA/Inc/Pcount.thy;
2005-09-07, by wenzelm
elimination of watcher.sig
2005-09-07, by paulson
Progress on eprover linkup, also massive tidying
2005-09-07, by paulson
axioms now included in tptp files, no /bin/cat and various tidying
2005-09-07, by paulson
consolidation of watcher.ML and watcher.sig
2005-09-07, by paulson
generalized types more
2005-09-07, by huffman
generalized types
2005-09-07, by huffman
added theorem hypreal_inverse2
2005-09-07, by huffman
replace type hcomplex with complex star
2005-09-07, by huffman
replace type hypnat with nat star
2005-09-07, by huffman
replace type hypreal with real star
2005-09-06, by huffman
add Hyperreal dependencies
2005-09-06, by huffman
class instances for nonstandard types
2005-09-06, by huffman
transfer principle tactic
2005-09-06, by huffman
generic nonstandard type constructor
2005-09-06, by huffman
converted to Isar theory format;
2005-09-06, by wenzelm
fix proof
2005-09-06, by huffman
converted to Isar theory format;
2005-09-06, by wenzelm
reimplement Filter.thy with locales
2005-09-06, by huffman
converted to Isar theory format;
2005-09-06, by wenzelm
converted to Isar theory format;
2005-09-06, by wenzelm
removed some ML files in Modelcheck/;
2005-09-06, by wenzelm
updated;
2005-09-06, by wenzelm
axclass: no longer bind "cI";
2005-09-06, by wenzelm
deprecated old-style infix declarations, which mix name and syntax;
2005-09-06, by wenzelm
tuned msg;
2005-09-06, by wenzelm
AList.defined;
2005-09-06, by wenzelm
name space prefix is now "c_class" instead of just "c";
2005-09-06, by wenzelm
proper treatment of polymorphic sets;
2005-09-06, by wenzelm
tuned comments;
2005-09-06, by wenzelm
converted to Isar theory format;
2005-09-06, by wenzelm
make LocalesTest last, because it sets funny flags;
2005-09-06, by wenzelm
avoid old-style infixes;
2005-09-06, by wenzelm
axclass: name space prefix is now "c_class" instead of just "c";
2005-09-06, by wenzelm
axclass: name space prefix is now "c_class" instead of just "c";
2005-09-06, by wenzelm
unnecessary parentheses removed
2005-09-06, by webertj
converted to Isar theory format;
2005-09-06, by wenzelm
introduced some new-style AList operations
2005-09-06, by haftmann
eliminated 1 call to polyEq
2005-09-06, by haftmann
tuned;
2005-09-05, by wenzelm
updated;
2005-09-05, by wenzelm
obsolete;
2005-09-05, by wenzelm
added assert, command;
2005-09-05, by wenzelm
tuned check_text;
2005-09-05, by wenzelm
chapter/section/subsection/subsubsection/text: optional locale specification;
2005-09-05, by wenzelm
markup commands: optional locale specification;
2005-09-05, by wenzelm
add_chapter/section/subsection/subsubsection/text: optional locale specification;
2005-09-05, by wenzelm
curried_lookup/update;
2005-09-05, by wenzelm
tuned;
2005-09-05, by wenzelm
Markup commands 'chapter' .. 'text' support optional locale specification;
2005-09-05, by wenzelm
removed duplicate theorems;
2005-09-05, by wenzelm
introduced binding priority 1 for linear combinators etc.
2005-09-05, by haftmann
converted to Isar theory format;
2005-09-03, by wenzelm
tuned method;
2005-09-03, by wenzelm
tuned;
2005-09-03, by wenzelm
obsolete;
2005-09-03, by wenzelm
converted to Isar theory format;
2005-09-03, by wenzelm
obsolete (see Cube.thy);
2005-09-03, by wenzelm
tuned msg;
2005-09-03, by wenzelm
uses ("LCF_lemmas.ML");
2005-09-03, by wenzelm
converted to Isar theory format;
2005-09-03, by wenzelm
tuned;
2005-09-03, by wenzelm
removed fix.thy, pair.thy, simpdata.ML;
2005-09-03, by wenzelm
converted to Isar theory format;
2005-09-03, by wenzelm
converted to Isar theory format;
2005-09-03, by wenzelm
setmp print_mode []; more robust outer syntax; tuned;
2005-09-03, by wenzelm
tuned;
2005-09-03, by wenzelm
simplified oracle;
2005-09-03, by wenzelm
use Check.ML;
2005-09-03, by wenzelm
fixed ML errors;
2005-09-03, by wenzelm
removed IOA/Storage/Impl.ML, IOA/Storage/Action.ML;
2005-09-03, by wenzelm
deprecated non-Isar theory file format;
2005-09-03, by wenzelm
Added ECommunication.ML
2005-09-02, by quigley
Added ECommunication.ML and modified res_atp.ML, Reconstruction.thy, and
2005-09-02, by quigley
further tidying up of Isabelle-ATP link
2005-09-02, by paulson
converted specifications to Isar theories;
2005-09-02, by wenzelm
some 'assoc' etc. refactoring
2005-09-02, by haftmann
tidying up the Isabelle/ATP interface
2005-09-02, by paulson
fixed arities and restored changes that had gone missing
2005-09-02, by paulson
deleted obsolete VampireCommunication.ML
2005-09-02, by paulson
print_locale omits facts by default
2005-09-02, by ballarin
curried_lookup/update;
2005-09-01, by wenzelm
refrain from sorting output;
2005-09-01, by wenzelm
curried_lookup/update;
2005-09-01, by wenzelm
curried_lookup/update;
2005-09-01, by wenzelm
curried_lookup/update;
2005-09-01, by wenzelm
added curried_lookup/update operations -- in preparation of currying plain lookup/update;
2005-09-01, by wenzelm
curried_lookup/update;
2005-09-01, by wenzelm
updated;
2005-09-01, by wenzelm
renamed 'thms_containing' to 'find_theorems' -- keep old version for the time being;
2005-09-01, by wenzelm
removed obsolete 'symbols' mode;
2005-09-01, by wenzelm
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
2005-09-01, by wenzelm
improved formatting
2005-09-01, by paulson
isamarkuptext/txt: \par before changing sizes prevents spacing anomaly;
2005-09-01, by wenzelm
updated;
2005-09-01, by wenzelm
fixed ins_tokentr: AList.default;
2005-08-31, by wenzelm
comp -> compile
2005-08-31, by nipkow
Additional BigO lemmas that require the HOL-Complex logic image;
2005-08-31, by wenzelm
added copy-dump option;
2005-08-31, by wenzelm
added line break for 'uses';
2005-08-31, by wenzelm
added no_body_context;
2005-08-31, by wenzelm
use_dir: added copy-dump option;
2005-08-31, by wenzelm
present_text: Toplevel.no_body_context prevents use of wrong context in interaction;
2005-08-31, by wenzelm
refer to theory instead of low-level tsig;
2005-08-31, by wenzelm
tuned classes_arities_of;
2005-08-31, by wenzelm
refer to theory instead of low-level tsig;
2005-08-31, by wenzelm
added Avigad-Donnelly;
2005-08-31, by wenzelm
reactivate postfix by change of syntax;
2005-08-31, by wenzelm
tuned presentation;
2005-08-31, by wenzelm
moved lemmas that require the HOL-Complex logic image to Complex/ex/BigO_Complex.thy;
2005-08-31, by wenzelm
added Complex/ex/BigO_Complex.thy;
2005-08-31, by wenzelm
simp_implies: proper named infix;
2005-08-31, by wenzelm
tuned;
2005-08-31, by wenzelm
isatool usedir: added option -C;
2005-08-31, by wenzelm
added option -C: copy existing document directory;
2005-08-31, by wenzelm
* Delimiters of outer tokens now produce separate LaTeX macros;
2005-08-31, by wenzelm
introduced AList.*
2005-08-31, by haftmann
better map_entry
2005-08-31, by haftmann
fixed bug in record_type_abbr_tr'
2005-08-30, by schirmer
patterns in setsum and setprod
2005-08-30, by paulson
Updated import.
2005-08-29, by obua
updated;
2005-08-29, by wenzelm
delimiter markup for verbatim tokens;
2005-08-29, by wenzelm
clarify type tok, do not emit markup flag for suppressed tokens;
2005-08-29, by wenzelm
use AList operations;
2005-08-29, by wenzelm
cover tagged command regions;
2005-08-29, by wenzelm
tune spacing where a generated theory text is included directly;
2005-08-29, by wenzelm
updated;
2005-08-29, by wenzelm
recover original definitions of \isactrlsub etc.;
2005-08-29, by wenzelm
canonical interface for 'default'
2005-08-29, by haftmann
output \<^loc> as 'loc' span;
2005-08-28, by wenzelm
isatool latex -o sty;
2005-08-28, by wenzelm
added 'loc';
2005-08-28, by wenzelm
updated;
2005-08-28, by wenzelm
ASCII back-quote no longer sym char;
2005-08-28, by wenzelm
added \isactrlloc;
2005-08-28, by wenzelm
* ML functions legacy_bindings and use_legacy_bindings;
2005-08-28, by wenzelm
avoid symbolic identifier;
2005-08-28, by wenzelm
added (use_)legacy_bindings;
2005-08-28, by wenzelm
output_basic: handle AltString token;
2005-08-28, by wenzelm
removed obsolete type_syn;
2005-08-28, by wenzelm
unskolem local vars;
2005-08-28, by wenzelm
tuned;
2005-08-28, by wenzelm
added alt_string;
2005-08-28, by wenzelm
added AltString token (delimited by ASCII back-quotes);
2005-08-28, by wenzelm
removed unused dest operation;
2005-08-28, by wenzelm
export theorems_of;
2005-08-28, by wenzelm
tuned some proofs;
2005-08-28, by wenzelm
removed obsolete arities;
2005-08-28, by wenzelm
tuned size of included graph;
2005-08-28, by wenzelm
added \isachardoublequoteopen/close, \isacharbackquoteopen/close;
2005-08-28, by wenzelm
(branch cleanup)
2005-08-28, by haftmann
(allocating new branch)
2005-08-28, by haftmann
added superclasses, class_le_path
2005-08-28, by haftmann
added alist.ML
2005-08-28, by haftmann
added 'these', removed assoc2
2005-08-28, by haftmann
added alist module
2005-08-28, by haftmann
Fixed bug.
2005-08-26, by berghofe
DFG output now works for untyped rules (ML "ResClause.untyped();")
2005-08-26, by quigley
Lemmas on dvd, power and finite summation added or strengthened.
2005-08-26, by ballarin
replaced '?' by '??'
2005-08-26, by haftmann
Adapted to new code generator syntax.
2005-08-25, by berghofe
Put quotation marks around some occurrences of "file", since it is now
2005-08-25, by berghofe
Adapted to new code generator syntax.
2005-08-25, by berghofe
Implemented incremental code generation.
2005-08-25, by berghofe
fixed typo
2005-08-25, by haftmann
add_locale_context(_i) now exporting elements (still some refinements to be done)
2005-08-25, by haftmann
added ? combinator for conditional transformations
2005-08-25, by haftmann
added 'default' function
2005-08-25, by haftmann
Printing of interpretations: option to show witness theorems;
2005-08-24, by ballarin
Interpretation in locales: extended back end;
2005-08-24, by ballarin
replaced ? by ??
2005-08-23, by haftmann
fixed deps;
2005-08-19, by wenzelm
tuned arrangement of generated stuff;
2005-08-19, by wenzelm
updated;
2005-08-19, by wenzelm
tuned generated stuff;
2005-08-19, by wenzelm
updated;
2005-08-19, by wenzelm
updated;
2005-08-19, by wenzelm
obsolete;
2005-08-19, by wenzelm
tuned;
2005-08-19, by wenzelm
updated;
2005-08-19, by wenzelm
*** empty log message ***
2005-08-19, by nipkow
updated;
2005-08-19, by wenzelm
updated;
2005-08-19, by wenzelm
-H deleted
2005-08-19, by nipkow
ML_idf -> ML
2005-08-19, by nipkow
nicer list of axioms used
2005-08-18, by paulson
no need for TPTP2X unless SPASS is used
2005-08-18, by paulson
optimization to incr_indexes?
2005-08-18, by paulson
tuned;
2005-08-18, by wenzelm
fixed command prompt (was broken due to P.tags);
2005-08-18, by wenzelm
* The ML antiquotation prints type-checked ML expressions verbatim.
2005-08-18, by wenzelm
replace freeze by 'setmp show_question_marks false';
2005-08-18, by wenzelm
proof_to_theory_context: interaction flag;
2005-08-18, by wenzelm
accomodate interface Proof vs. Method;
2005-08-18, by wenzelm
added NO_CASES;
2005-08-18, by wenzelm
moved after method.ML;
2005-08-18, by wenzelm
prepare attributes here;
2005-08-18, by wenzelm
moved before proof.ML;
2005-08-18, by wenzelm
added add_locale_context(_i), which returns the body context for presentation;
2005-08-18, by wenzelm
moved translation functions to Pure/sign.ML;
2005-08-18, by wenzelm
various Toplevel.theory_context commands: proper presentation in context;
2005-08-18, by wenzelm
use theory instead of obsolete Sign.sg;
2005-08-18, by wenzelm
added map_specs/facts operators (from locale.ML);
2005-08-18, by wenzelm
removed obsolete Theory.sign_of;
2005-08-18, by wenzelm
load method.ML before proof.ML;
2005-08-18, by wenzelm
added interfaces for compile translation functions (from Isar/isar_thy.ML);
2005-08-18, by wenzelm
added tap;
2005-08-18, by wenzelm
updated;
2005-08-18, by wenzelm
usedir: tuned option -V;
2005-08-18, by wenzelm
usedir: removed option -H;
2005-08-18, by wenzelm
* Proper output of proof terms within a proof context;
2005-08-18, by wenzelm
Improved generation of witnesses in interpretation.
2005-08-17, by ballarin
Interpretation in locales.
2005-08-17, by ballarin
Use interpretation in locales.
2005-08-17, by ballarin
new examples
2005-08-17, by paulson
*** empty log message ***
2005-08-17, by nipkow
new command to invoke ATPs
2005-08-17, by paulson
small mods to code lemmas
2005-08-17, by nipkow
made SML/XL happy;
2005-08-17, by wenzelm
list_all_conv -> iff
2005-08-17, by nipkow
name fix
2005-08-16, by nipkow
added quite a few functions for code generation
2005-08-16, by nipkow
more simprules now have names
2005-08-16, by paulson
classical rules must have names for ATP integration
2005-08-16, by paulson
added listT
2005-08-16, by nipkow
support for document versions;
2005-08-16, by wenzelm
eliminated datatype token;
2005-08-16, by wenzelm
begin_index: list of docs;
2005-08-16, by wenzelm
added eq_syntax;
2005-08-16, by wenzelm
export proof_syntax, proof_of;
2005-08-16, by wenzelm
added String.isSuffix;
2005-08-16, by wenzelm
state: body context;
2005-08-16, by wenzelm
P.tags;
2005-08-16, by wenzelm
use_dir: removed hidden, added doc_versions;
2005-08-16, by wenzelm
back: removed ill-defined '!' option;
2005-08-16, by wenzelm
added transfer;
2005-08-16, by wenzelm
moved structure Keyword to OuterKeyword (Isar/outer_keyword.ML);
2005-08-16, by wenzelm
added tags parser;
2005-08-16, by wenzelm
clarify is_newline vs. is_blank;
2005-08-16, by wenzelm
default tags for theory/proof/ML commands;
2005-08-16, by wenzelm
reimplemented theory presentation, with support for tagged command regions;
2005-08-16, by wenzelm
back: removed ill-defined '!' option;
2005-08-16, by wenzelm
replaced sign by thy;
2005-08-16, by wenzelm
added liberal_name;
2005-08-16, by wenzelm
tuned Symbol.spaces;
2005-08-16, by wenzelm
tuned Buffer.add;
2005-08-16, by wenzelm
tuned unsuffix/unprefix;
2005-08-16, by wenzelm
type proof: theory_ref instead of theory (make proof contexts independent entities);
2005-08-16, by wenzelm
Isar command keyword classification (from Isar/outer_syntax.ML);
2005-08-16, by wenzelm
added Isar/outer_keyword.ML;
2005-08-16, by wenzelm
OuterKeyword;
2005-08-16, by wenzelm
updated;
2005-08-16, by wenzelm
removed -H false;
2005-08-16, by wenzelm
isatool usedir: option -V and -f;
2005-08-16, by wenzelm
tuned antiquotations;
2005-08-16, by wenzelm
\isabellestyleit: proper \isacharbackslash;
2005-08-16, by wenzelm
proper ML_DBASE for .../bin/poly;
2005-08-16, by wenzelm
added option -V VERSION;
2005-08-16, by wenzelm
added option -n NAME and -t TAGS;
2005-08-16, by wenzelm
-V outline=/proof,/ML;
2005-08-16, by wenzelm
* Command tags control specific markup of certain regions of text (replaces usedir -H);
2005-08-16, by wenzelm
simp_depth warning now mod 20, not mod 10 (too often)
2005-08-16, by nipkow
lucas - added pretty printing function and cleaned up signature a little.
2005-08-15, by dixon
lucas - fixed bug in changing focus - when moving up and right, if an abs was encountered it would move up an extra time. I also removed the spurious pretty printing function that did nothing.
2005-08-15, by dixon
New command: interpretation in locales.
2005-08-10, by ballarin
moved wf_induct_rule from PreList.thy to Wellfounded_Recursion.thy
2005-08-09, by nipkow
exported after_qed for arity proofs
2005-08-09, by haftmann
added finite(option) to Recdef.thy
2005-08-09, by nipkow
added selectors 'classes_of' and 'classes_arities_of'
2005-08-09, by haftmann
exported dest_def
2005-08-09, by haftmann
added 'the_const_constraint'
2005-08-09, by haftmann
(added to repository)
2005-08-09, by haftmann
(added to repository)
2005-08-09, by haftmann
After_qed takes result argument.
2005-08-08, by ballarin
Release of interpretation in locale.
2005-08-08, by ballarin
fixed typo in ratadd
2005-08-08, by nipkow
added hint for position of aqu options in connection with styles
2005-08-08, by haftmann
clarified ML_idf
2005-08-08, by haftmann
moved some rat functions to library.ML
2005-08-07, by nipkow
added more rat functions
2005-08-07, by nipkow
Tuned comment.
2005-08-06, by berghofe
new lemma
2005-08-06, by nipkow
Added ENTCS 2000 paper by Aleksey Nogin.
2005-08-05, by berghofe
New case study: pigeonhole principle.
2005-08-05, by berghofe
Added Extraction/Pigeonhole.
2005-08-05, by berghofe
added Brian Hufmann's finite instances
2005-08-05, by nipkow
Fixed bug in code generator for let and split leading to ill-formed code.
2005-08-03, by berghofe
Adapted to new argument format of MinProof constructor.
2005-08-03, by berghofe
Adapted to new interface og thms_of_proof / axms_of_proof.
2005-08-03, by berghofe
Adapted to new interface of thms_of_proof.
2005-08-03, by berghofe
- Tuned handling of oracles
2005-08-03, by berghofe
mentioned change to exp_ge_add_one_self, new transitivity rules
2005-08-03, by avigad
changes from renaming of exp_ge_add_one_self
2005-08-03, by avigad
renamed exp_ge_add_one_self to exp_ge_add_one_self_aux
2005-08-03, by avigad
renamed exp_ge_add_one_self2 to exp_ge_add_one_self
2005-08-03, by avigad
added extra transitivity rules
2005-08-03, by avigad
added Hyperreal/Ln, replaced Lfp and Gfp by FixedPoint
2005-08-03, by avigad
changed reference to Lfp.lfp to FixedPint.lfp, ditto for gfp
2005-08-03, by avigad
import FixedPoint instead of Gfp
2005-08-03, by avigad
removed Gfp
2005-08-03, by avigad
removed Lfp
2005-08-03, by avigad
combined Lfp and Gfp to FixedPoint
2005-08-03, by avigad
tuned ML_OPTIONS;
2005-08-02, by wenzelm
export clear_ss;
2005-08-02, by wenzelm
added unfold_tac (Simplifier.inherit_bounds);
2005-08-02, by wenzelm
simprocs: Simplifier.inherit_bounds;
2005-08-02, by wenzelm
tuned;
2005-08-02, by wenzelm
First version of interpretation in locales. Not yet fully functional.
2005-08-02, by ballarin
Turned simp_implies into binary operator.
2005-08-02, by ballarin
Added filter lemma
2005-08-02, by nipkow
* Pure/Simplifier: improved handling of bound variables;
2005-08-01, by wenzelm
determine Poly/ML runtime system version
2005-08-01, by wenzelm
obsolete;
2005-08-01, by wenzelm
determine Poly/ML's idea of current hardware and operating system type;
2005-08-01, by wenzelm
tuned;
2005-08-01, by wenzelm
Thm.full_prop_of;
2005-08-01, by wenzelm
Compress.term;
2005-08-01, by wenzelm
removed atless (use term_ord instead);
2005-08-01, by wenzelm
export MataSimplifier.inherit_bounds;
2005-08-01, by wenzelm
Compress.typ;
2005-08-01, by wenzelm
Compress.init_data;
2005-08-01, by wenzelm
nameless Term.bound;
2005-08-01, by wenzelm
improved bounds: nameless Term.bound, recover names for output;
2005-08-01, by wenzelm