2002-09-26 paulson 2002-09-26 new theory for Pi-sets, restrict, etc.
2002-09-26 paulson 2002-09-26 Converted Fun to Isar style. Moved Pi, funcset, restrict from Fun.thy to Library/FuncSet.thy. Renamed constant "Fun.op o" to "Fun.comp"
2002-09-26 paulson 2002-09-26 new document directory for GroupTheory
2002-09-26 paulson 2002-09-26 converted to Isar and using new "implicit structures" instead of Sigma, etc
2002-09-25 nipkow 2002-09-25 *** empty log message ***
2002-09-25 nipkow 2002-09-25 *** empty log message ***
2002-09-25 nipkow 2002-09-25 *** empty log message ***
2002-09-25 nipkow 2002-09-25 Int.thy -> int.thy
2002-09-25 nipkow 2002-09-25 became int.ML
2002-09-25 nipkow 2002-09-25 conversion to Isar
2002-09-25 nipkow 2002-09-25 converted to Isar
2002-09-25 nipkow 2002-09-25 added nat_split
2002-09-21 paulson 2002-09-21 converted to Isar script
2002-09-20 paulson 2002-09-20 shortened a proof
2002-09-20 paulson 2002-09-20 got rid of deepen_tac
2002-09-20 paulson 2002-09-20 less use of x-symbols
2002-09-19 nipkow 2002-09-19 *** empty log message ***
2002-09-19 nipkow 2002-09-19 drule: added nRS simplifier: trace with names
2002-09-19 nipkow 2002-09-19 preserve names of rewrite rules when transforming them
2002-09-18 kleing 2002-09-18 comments + usage
2002-09-11 paulson 2002-09-11 Streamlined proofs of instances of Separation
2002-09-11 paulson 2002-09-11 Bound variable preservation in Collect_cong
2002-09-10 paulson 2002-09-10 renamed M_triv_axioms to M_trivial and M_axioms to M_basic
2002-09-10 paulson 2002-09-10 tweaks
2002-09-09 nipkow 2002-09-09 *** empty log message ***
2002-09-09 nipkow 2002-09-09 bug in counter example finder
2002-09-07 paulson 2002-09-07 conversion of ZF/Integ/{Int,Bin} to Isar scripts
2002-09-05 paulson 2002-09-05 added checking so that (rename_tac "x y") is rejected, since "x y" is not an identifier
2002-09-03 paulson 2002-09-03 tidied
2002-09-03 paulson 2002-09-03 deleted redundant material (quasiformula, ...) and rationalized
2002-09-03 paulson 2002-09-03 fixed the typesetting
2002-09-03 nipkow 2002-09-03 *** empty log message ***
2002-09-02 paulson 2002-09-02 Added missing rewrite rule and some arith examples
2002-09-02 nipkow 2002-09-02 order_less_irrefl: [simp] -> [iff]
2002-09-01 nipkow 2002-09-01 *** empty log message ***
2002-08-31 paulson 2002-08-31 converted Hyperreal/Zorn to Isar format and moved to Library
2002-08-30 paulson 2002-08-30 removal of blast.overloaded
2002-08-29 wenzelm 2002-08-29 updated;
2002-08-29 wenzelm 2002-08-29 *** empty log message ***
2002-08-29 wenzelm 2002-08-29 tuned;
2002-08-29 paulson 2002-08-29 fixed a name clash
2002-08-28 wenzelm 2002-08-28 improved tell_thm_deps;
2002-08-28 paulson 2002-08-28 various new lemmas for Constructible
2002-08-28 paulson 2002-08-28 completion of the consistency proof for AC
2002-08-27 wenzelm 2002-08-27 thms_containing: allow "_" in specification;
2002-08-27 wenzelm 2002-08-27 *** empty log message ***
2002-08-27 wenzelm 2002-08-27 * Pure: disallow duplicate fact bindings within new-style theory files;
2002-08-27 wenzelm 2002-08-27 disallow duplicate fact bindings for drafts (i.e. within new-style theory files);
2002-08-27 wenzelm 2002-08-27 tuned;
2002-08-27 wenzelm 2002-08-27 avoid duplicate fact bindings;
2002-08-27 wenzelm 2002-08-27 removed IsarTut;
2002-08-27 wenzelm 2002-08-27 *** empty log message ***
2002-08-27 wenzelm 2002-08-27 avoid duplicate fact bindings;
2002-08-27 wenzelm 2002-08-27 check_file: disallow current dir (typically "");
2002-08-27 wenzelm 2002-08-27 simplified results; added hook;
2002-08-27 wenzelm 2002-08-27 simplified results;
2002-08-27 wenzelm 2002-08-27 Thm.proof_of;
2002-08-27 wenzelm 2002-08-27 check_goal: produce error instead of warning;
2002-08-27 wenzelm 2002-08-27 added proof_of;
2002-08-27 wenzelm 2002-08-27 thms/axms_of_proof: proper handling of MinProof;