2007-06-13 wenzelm 2007-06-13 tuned proofs: avoid implicit prems; tuned;
2007-06-13 wenzelm 2007-06-13 tuned proofs: avoid implicit prems; major cleanup of proofs/document;
2007-06-13 wenzelm 2007-06-13 tuned comments;
2007-06-13 wenzelm 2007-06-13 tuned proofs: avoid implicit prems;
2007-06-13 huffman 2007-06-13 clean up instance proofs; reorganize section headings
2007-06-13 wenzelm 2007-06-13 reactivated theory Class;
2007-06-13 urbanc 2007-06-13 added the Q_Unit rule (was missing) and adjusted the proof accordingly
2007-06-13 wenzelm 2007-06-13 * Isar: method "assumption" (implicit closing of subproofs) takes non-atomic goal assumptions into account; * Isar: implicit use of prems from the Isar proof context is considered a legacy feature;
2007-06-13 narboux 2007-06-13 generate_fresh works even if there is no free variable in the goal
2007-06-13 wenzelm 2007-06-13 tuned;
2007-06-13 wenzelm 2007-06-13 tuned proofs: avoid implicit prems;
2007-06-13 huffman 2007-06-13 removed constant int :: nat => int; int is now an abbreviation for of_nat :: nat => int
2007-06-13 huffman 2007-06-13 thm antiquotations
2007-06-13 wenzelm 2007-06-13 transaction: context_position (non-destructive only);
2007-06-13 wenzelm 2007-06-13 added map_current; simplified internal type proof;
2007-06-13 wenzelm 2007-06-13 tuned msg;
2007-06-13 wenzelm 2007-06-13 apply_method/end_proof: pass position; Method.Basic: include position;
2007-06-13 wenzelm 2007-06-13 renamed map to map_current;
2007-06-13 wenzelm 2007-06-13 tuned;
2007-06-13 wenzelm 2007-06-13 removed unused is_atomic;
2007-06-13 wenzelm 2007-06-13 renamed prove_raw to prove_internal; tuned;
2007-06-13 wenzelm 2007-06-13 merge/merge_refs: plain error instead of exception TERM;
2007-06-13 wenzelm 2007-06-13 Context positions.
2007-06-13 wenzelm 2007-06-13 added context_position.ML;
2007-06-13 wenzelm 2007-06-13 renamed Goal.prove_raw to Goal.prove_internal;
2007-06-13 wenzelm 2007-06-13 Method.Basic: include position;
2007-06-13 wenzelm 2007-06-13 tuned proofs: avoid implicit prems;
2007-06-13 wenzelm 2007-06-13 Basic text: include position; assumption/close: refer to non-atomic assumptions as well, implicit use of prems now considered legacy feature;
2007-06-12 huffman 2007-06-12 thm antiquotations
2007-06-12 huffman 2007-06-12 add lemma inj_of_nat
2007-06-12 huffman 2007-06-12 thm antiquotations
2007-06-12 chaieb 2007-06-12 Unfortunately needed patch due to incompatibility with SML -- oo is infix and hence can not appear on the left handside of patterns
2007-06-12 chaieb 2007-06-12 changed int stuff into integer for SMLNJ compatibility
2007-06-12 huffman 2007-06-12 more of_rat lemmas
2007-06-12 huffman 2007-06-12 add function of_rat and related lemmas
2007-06-12 chaieb 2007-06-12 turned curry (op opr) into curry op opr --- because of smlnj
2007-06-12 wenzelm 2007-06-12 De-overloaded operations for int and real.
2007-06-12 wenzelm 2007-06-12 SML basis with type int representing proper integers, not machine words.
2007-06-12 chaieb 2007-06-12 Tuned proofs : now use 'algebra ad: ...'
2007-06-12 chaieb 2007-06-12 cooper_tac takes now two lists of theorems to be added/deleted from the simpset dor pre-simplification
2007-06-12 chaieb 2007-06-12 changed val restriction to local due to smlnj
2007-06-12 chaieb 2007-06-12 Changed normalizer Data to contain a simpset besides the list of instances; Before the method starts, it simplifies with this simpset; Added attribute 'algebra' to add and delete theorems from the simpset above;
2007-06-12 chaieb 2007-06-12 Added algebra_tac; tuned;
2007-06-12 chaieb 2007-06-12 Method now takes theorems to be added or deleted from a simpset for simplificatio before the core method starts
2007-06-12 chaieb 2007-06-12 algebra_tac moved to file Tools/Groebner_Basis/groebner.ML; Method now takes theorems to be added or deleted from a simpset for simplificatio *before* the core method starts
2007-06-11 nipkow 2007-06-11 nex example
2007-06-11 chaieb 2007-06-11 Conversion for computation on constants now depends on the context
2007-06-11 chaieb 2007-06-11 tuned setup for the fields instantiation for Groebner Bases;
2007-06-11 chaieb 2007-06-11 Added dependency on file Groebner_Basis.thy
2007-06-11 chaieb 2007-06-11 Added instantiation of algebra method to fields
2007-06-11 nipkow 2007-06-11 hid constant "dom"
2007-06-11 chaieb 2007-06-11 Removed from CVS, since obselete in the new Presburger Method;
2007-06-11 chaieb 2007-06-11 Generated reflected QE procedure for Presburger Arithmetic-- Cooper's Algorithm -- see HOL/ex/Reflected_Presburger.thy
2007-06-11 chaieb 2007-06-11 Added more examples
2007-06-11 chaieb 2007-06-11 Now only contains generic conversion for quantifier elimination in HOL
2007-06-11 chaieb 2007-06-11 A new tactic for Presburger;
2007-06-11 chaieb 2007-06-11 tuned
2007-06-11 chaieb 2007-06-11 Temporarily added theorems for QE that were in old Presburger.thy ; This will diseappear with the new Ferrante and Rackoff shortly;
2007-06-11 chaieb 2007-06-11 tuned tactic
2007-06-11 chaieb 2007-06-11 Temporarily use int instead of IntInf.int but Code generator should map HOL's int to ML's IntInf.int --- To be fixed