Mercurial
testboard
/ shortlog
summary
| shortlog |
changelog
|
graph
|
tags
|
branches
|
files
|
gz
2000-07-27 ago
wenzelm
intro_elim_tac: bimatch_from;
changeset
|
files
2000-07-26 ago
nipkow
While functional for defining tail-recursive functions
changeset
|
files
2000-07-26 ago
nipkow
*** empty log message ***
changeset
|
files
2000-07-25 ago
wenzelm
tuned msg;
changeset
|
files
2000-07-25 ago
berghofe
Corrected example which still used old primrec syntax.
changeset
|
files
2000-07-25 ago
nipkow
Replaced force by fast because force may now take forever to fail
changeset
|
files
2000-07-25 ago
nipkow
new constant same_fst
changeset
|
files
2000-07-25 ago
wenzelm
by (CLASIMPSET auto_tac);
changeset
|
files
2000-07-25 ago
wenzelm
added clarify method;
changeset
|
files
2000-07-25 ago
wenzelm
added clarsimp method;
changeset
|
files
2000-07-25 ago
wenzelm
tuned;
changeset
|
files
2000-07-25 ago
wenzelm
removed slow, slow_best methods;
changeset
|
files
2000-07-25 ago
wenzelm
* Isar/Provers: intro/elim/dest attributes: changed
changeset
|
files
2000-07-25 ago
wenzelm
rearranged setup of arithmetic procedures, avoiding global reference values;
changeset
|
files
2000-07-25 ago
wenzelm
lemmas [arith_split] = abs_split (*belongs to theory RealAbs*);
changeset
|
files
2000-07-25 ago
wenzelm
do nat pass theory value, but sg_ref;
changeset
|
files
2000-07-25 ago
wenzelm
avoid referencing thy value;
changeset
|
files
2000-07-25 ago
wenzelm
avoid referencing thy value;
changeset
|
files
2000-07-25 ago
wenzelm
tuned deps;
changeset
|
files
2000-07-24 ago
wenzelm
tuned;
changeset
|
files
2000-07-24 ago
wenzelm
changed deps;
changeset
|
files
2000-07-24 ago
wenzelm
rename_numerals: use implicit theory context;
changeset
|
files
2000-07-24 ago
wenzelm
avoid referencing thy value;
changeset
|
files
2000-07-24 ago
wenzelm
avoid referencing thy value;
changeset
|
files
2000-07-24 ago
wenzelm
avoid referencing thy value;
changeset
|
files
2000-07-24 ago
wenzelm
simpset_of NatDef.thy (why anyway?);
changeset
|
files
2000-07-24 ago
wenzelm
avoid referencing thy value;
changeset
|
files
2000-07-24 ago
wenzelm
avoid referencing thy value;
changeset
|
files
2000-07-24 ago
wenzelm
tuned comment;
changeset
|
files
2000-07-24 ago
wenzelm
avoid global references;
changeset
|
files
2000-07-24 ago
wenzelm
do not pass theory values, but sg_ref;
changeset
|
files
2000-07-24 ago
wenzelm
Drule.merge_rules;
changeset
|
files
2000-07-23 ago
wenzelm
get_names: topologically sorted;
changeset
|
files
2000-07-23 ago
wenzelm
removed all_sessions.graph;
changeset
|
files
2000-07-23 ago
wenzelm
removed all_sessions;
changeset
|
files
2000-07-23 ago
wenzelm
disallow duplicates in session identifiers;
changeset
|
files
2000-07-23 ago
wenzelm
assimilated;
changeset
|
files
2000-07-23 ago
wenzelm
tuned HeapFun;
changeset
|
files
2000-07-23 ago
wenzelm
tuned ThmHeap;
changeset
|
files
2000-07-23 ago
wenzelm
removed selector syntax -- improper tuples are broken beyond repair :-(
changeset
|
files
2000-07-23 ago
wenzelm
elim?;
changeset
|
files
2000-07-23 ago
wenzelm
classical atts now intro! / intro / intro?;
changeset
|
files
2000-07-23 ago
wenzelm
renamed "Directories" to "Sessions";
changeset
|
files
2000-07-23 ago
wenzelm
tuned;
changeset
|
files
2000-07-22 ago
wenzelm
improved error msg;
changeset
|
files
2000-07-21 ago
nipkow
added ex_someI
changeset
|
files
2000-07-21 ago
paulson
much tidying in connection with the 2nd UNITY paper
changeset
|
files
2000-07-21 ago
oheimb
strengthened force_tac by using new first_best_tac
changeset
|
files
2000-07-21 ago
oheimb
removed safe_asm_full_simp_tac
changeset
|
files
2000-07-21 ago
oheimb
added map_upd_nonempty, also to simpset
changeset
|
files
2000-07-21 ago
oheimb
removed weaker variant of subset_insert_iff
changeset
|
files
2000-07-21 ago
oheimb
removed safe_asm_full_simp_tac, added generic_simp_tac
changeset
|
files
2000-07-21 ago
prensani
Updating of some comments
changeset
|
files
2000-07-21 ago
nipkow
*** empty log message ***
changeset
|
files
2000-07-21 ago
paulson
Univ no longer requires Arith (really it never did)
changeset
|
files
2000-07-20 ago
wenzelm
tuned;
changeset
|
files
2000-07-19 ago
oheimb
corrected header
changeset
|
files
2000-07-19 ago
paulson
changed / to // for quotienting
changeset
|
files
2000-07-19 ago
paulson
changed / to // for quotienting; general tidying
changeset
|
files
2000-07-19 ago
paulson
renamed // to / (which is what we want anyway) to avoid clash with the new
changeset
|
files