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