Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-10000
-3000
-1000
-240
+240
+1000
+3000
+10000
+30000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
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
less
more
|
(0)
-10000
-3000
-1000
-240
+240
+1000
+3000
+10000
+30000
tip