isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -10000 -3000 -1000 -300 -100 -50 -28 +28 +50 +100 +300 +1000 +3000 +10000 +30000 tip

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

less more | (0) -10000 -3000 -1000 -300 -100 -50 -28 +28 +50 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle