isabelle: Graph

updated for metis method
2007-06-26, by paulson
recoded
2007-06-26, by paulson
simplified
2007-06-26, by paulson
completed some references
2007-06-26, by paulson
changes for type class ring_no_zero_divisors
2007-06-26, by paulson
*** empty log message ***
2007-06-26, by nipkow
added NBE
2007-06-26, by nipkow
removed removed lemmas
2007-06-26, by nipkow
fixed undo: try undos_proof first!
2007-06-26, by wenzelm
tactics: more robust addressing of subgoal using (C)SUBGOAL/THEN_ALL_NEW;
2007-06-25, by wenzelm
removed theorem
2007-06-25, by nipkow
removed redundant lemma
2007-06-25, by nipkow
removed redundant lemmas
2007-06-25, by nipkow
commented changes in HOL/Ring_and_Field.thy, and in HOL/Real/RealPow.thy
2007-06-25, by obua
removed "sum_tools.ML" in favour of BalancedTree
2007-06-25, by krauss
added eta_long_conversion;
2007-06-25, by wenzelm
added eta_long_tac;
2007-06-25, by wenzelm
added reasonably efficient add_cterm_frees;
2007-06-25, by wenzelm
made type conv pervasive;
2007-06-25, by wenzelm
made type conv pervasive;
2007-06-25, by wenzelm
Thm.eta_long_conversion;
2007-06-25, by wenzelm
made type conv pervasive;
2007-06-25, by wenzelm
Thm.add_cterm_frees;
2007-06-25, by wenzelm
made type conv pervasive;
2007-06-25, by wenzelm
made type conv pervasive;
2007-06-25, by wenzelm
tex problem fixed
2007-06-24, by nipkow
tuned and used field_simps
2007-06-24, by nipkow
*** empty log message ***
2007-06-24, by nipkow
*** empty log message ***
2007-06-24, by nipkow
new lemmas
2007-06-24, by nipkow
*** empty log message ***
2007-06-24, by nipkow
tuned and renamed group_eq_simps and ring_eq_simps
2007-06-23, by nipkow
fix looping simp rule
2007-06-22, by huffman
reinstate real_root_less_iff [simp]
2007-06-22, by huffman
merge is now identity
2007-06-22, by chaieb
new method "elim_to_cases" provides ad-hoc conversion of obtain-style
2007-06-22, by krauss
section headings
2007-06-21, by huffman
add thm antiquotations
2007-06-21, by huffman
spelling
2007-06-21, by huffman
add thm antiquotations
2007-06-21, by huffman
changed simp rules for of_nat
2007-06-21, by huffman
tuned proofs -- avoid implicit prems;
2007-06-21, by wenzelm
moved quantifier elimination tools to Tools/Qelim/;
2007-06-21, by wenzelm
moved Presburger setup back to Presburger.thy;
2007-06-21, by wenzelm
tuned proofs -- avoid implicit prems;
2007-06-21, by wenzelm
tuned proofs -- avoid implicit prems;
2007-06-21, by wenzelm
renamed NatSimprocs.thy to Arith_Tools.thy;
2007-06-21, by wenzelm
tuned;
2007-06-21, by wenzelm
adapted tool setup;
2007-06-21, by wenzelm
added Ferrante-Rackoff setup;
2007-06-21, by wenzelm
tuned comments;
2007-06-21, by wenzelm
moved HOL/Tools/Presburger/qelim.ML to HOL/Tools/qelim.ML;
2007-06-21, by wenzelm
Ferrante-Rackoff quantifier elimination.
2007-06-21, by wenzelm
Context data for Ferrante-Rackoff quantifier elimination.
2007-06-21, by wenzelm
replaced Real/Ferrante-Rackoff tool by generic version in Main HOL;
2007-06-21, by wenzelm
Dense linear order witout endpoints
2007-06-21, by wenzelm
renamed metis-env.ML to metis_env.ML;
2007-06-21, by wenzelm
added Id;
2007-06-21, by wenzelm
fine tune automatic generation of inversion lemmas
2007-06-21, by narboux
integration of Metis prover
2007-06-21, by paulson
renamed metis-env to metis-env.ML;
2007-06-21, by wenzelm
tuned comments;
2007-06-20, by wenzelm
obsolete (cf. ATP_Linkup.thy);
2007-06-20, by wenzelm
added Tools/metis_tools.ML;
2007-06-20, by wenzelm
added Metis setup (from Metis.thy);
2007-06-20, by wenzelm
added HOL-Nominal-Examples;
2007-06-20, by wenzelm
The Metis prover (slightly modified version from Larry);
2007-06-20, by wenzelm
avoid using implicit prems in assumption
2007-06-20, by huffman
Added flexflex_first_order and tidied first_order_resolution
2007-06-20, by paulson
A more robust flexflex_unique
2007-06-20, by paulson
remove simp attribute from of_nat_diff, for backward compatibility with zdiff_int
2007-06-20, by huffman
tuned error msg
2007-06-20, by krauss
Remove dedicated flag setting elements in favour of setproverflag.
2007-06-20, by aspinall
Remove dedicated flag setting elements in favour of setproverflag. Restore displayconfig response in askpgip.
2007-06-20, by aspinall
Synchronize schema with current version
2007-06-20, by aspinall
added lemmas
2007-06-20, by nipkow
added meta_impE
2007-06-20, by nipkow
change simp rules for of_nat to work like int did previously (reorient of_nat_Suc, remove of_nat_mult [simp]); preserve original variable names in legacy int theorems
2007-06-20, by huffman
section headings
2007-06-20, by huffman
simplify some proofs
2007-06-20, by huffman
oops -- fixed profiling;
2007-06-19, by wenzelm
Balanced binary trees (material from library.ML);
2007-06-19, by wenzelm
profiling: observe no_timing;
2007-06-19, by wenzelm
added raw_tactic;
2007-06-19, by wenzelm
moved balanced tree operations to General/balanced_tree.ML;
2007-06-19, by wenzelm
added with_subgoal;
2007-06-19, by wenzelm
balanced conjunctions;
2007-06-19, by wenzelm
balanced conjunctions;
2007-06-19, by wenzelm
added General/balanced_tree.ML;
2007-06-19, by wenzelm
BalancedTree;
2007-06-19, by wenzelm
balanced conjunctions;
2007-06-19, by wenzelm
tuned;
2007-06-19, by wenzelm
generalized proofs so that call graphs can have any node type.
2007-06-19, by krauss
macbroy5: trying -j 2;
2007-06-19, by wenzelm
tuned conjunction tactics: slightly smaller proof terms;
2007-06-18, by wenzelm
tuned laws for cancellation in divisions for fields.
2007-06-17, by nipkow
moved nonzero_mult_divide_cancel_right to Ring_and_Field as nonzero_mult_divide_cancel_right'; tuned proofs
2007-06-17, by chaieb
Added eta_conv and eta-expansion conversion: waiting for it to be in thm.ML; exported is_refl
2007-06-17, by chaieb
gen_qelim_conv now reduces the universal quatifier to the existential one; Now also deals with Ex f for eta-contracted f;
2007-06-17, by chaieb
thin_prems_tac first max-scopes universal quantifiers; eta_conv moved to Pure/conv.ML
2007-06-17, by chaieb
Tuned error messages; tuned;
2007-06-17, by chaieb
normalizer conversions depend on the proof context; added functions for conversion and wrapper that sill depend on the variable ordering (_ord)
2007-06-17, by chaieb
added theorems nonzero_mult_divide_cancel_right' nonzero_mult_divide_cancel_left' ordered_field_no_lb ordered_field_no_ub
2007-06-17, by chaieb
moved lemma all_not_ex to HOL.thy ; tuned proofs
2007-06-17, by chaieb
Tuned instantiation of Groebner bases to fields
2007-06-17, by chaieb
added Theorem all_not_ex
2007-06-17, by chaieb
renamed vars in zle_trans for compatibility
2007-06-17, by nipkow
tuned
2007-06-16, by nipkow
The simprocs "divide_cancel_factor" and "ring_eq_cancel_factor" no
2007-06-16, by nipkow
Locally added definition of "int :: nat => int" again to make
2007-06-15, by berghofe
made divide_self a simp rule
2007-06-15, by nipkow
Removed thunk from Fun
2007-06-15, by nipkow
Church numerals added
2007-06-15, by nipkow
method assumption: uniform treatment of prems as legacy feature;
2007-06-14, by wenzelm
tuned proofs;
2007-06-14, by wenzelm
tuned proofs: avoid implicit prems;
2007-06-14, by wenzelm
fixed term_constants (impact on is_relevant); terms in generalize_tac are sorted before we abstract over them (to *try* to avoid the case when a term to be abstracted over already occurs in an other)
2007-06-14, by chaieb
no computation rules in the pre-simplifiaction set
2007-06-14, by chaieb
Added some lemmas to default presburger simpset; tuned proofs
2007-06-14, by chaieb
tuned proofs: avoid implicit prems;
2007-06-14, by wenzelm
tuned proofs: avoid implicit prems;
2007-06-14, by wenzelm
Now ResHolClause also does first-order problems!
2007-06-14, by paulson
Now also handles FO problems
2007-06-14, by paulson
Deleted unused code
2007-06-14, by paulson
tidied
2007-06-14, by paulson
tuned proofs: avoid implicit prems;
2007-06-14, by wenzelm
clarified who we consider to be a contributor
2007-06-14, by kleing
Fixed Problem with ML-bindings for thm names;
2007-06-14, by chaieb
fixed filter syntax
2007-06-14, by nipkow
updated 'find_theorems' -- moved ProofGeneral specifics to ProofGeneral/CHANGES;
2007-06-14, by wenzelm
tuned proofs: avoid implicit prems;
2007-06-14, by wenzelm
int abbreviates of_nat
2007-06-13, by huffman
tuned proofs: avoid implicit prems;
2007-06-13, by wenzelm
tuned proofs: avoid implicit prems;
2007-06-13, by wenzelm
tuned comments;
2007-06-13, by wenzelm
tuned proofs: avoid implicit prems;
2007-06-13, by wenzelm
clean up instance proofs; reorganize section headings
2007-06-13, by huffman
reactivated theory Class;
2007-06-13, by wenzelm
added the Q_Unit rule (was missing) and adjusted the proof accordingly
2007-06-13, by urbanc
* Isar: method "assumption" (implicit closing of subproofs) takes non-atomic goal assumptions into account;
2007-06-13, by wenzelm
generate_fresh works even if there is no free variable in the goal
2007-06-13, by narboux
tuned;
2007-06-13, by wenzelm
tuned proofs: avoid implicit prems;
2007-06-13, by wenzelm
removed constant int :: nat => int;
2007-06-13, by huffman
thm antiquotations
2007-06-13, by huffman
transaction: context_position (non-destructive only);
2007-06-13, by wenzelm
added map_current;
2007-06-13, by wenzelm
tuned msg;
2007-06-13, by wenzelm
apply_method/end_proof: pass position;
2007-06-13, by wenzelm
renamed map to map_current;
2007-06-13, by wenzelm
tuned;
2007-06-13, by wenzelm
removed unused is_atomic;
2007-06-13, by wenzelm
renamed prove_raw to prove_internal;
2007-06-13, by wenzelm
merge/merge_refs: plain error instead of exception TERM;
2007-06-13, by wenzelm
Context positions.
2007-06-13, by wenzelm
added context_position.ML;
2007-06-13, by wenzelm
renamed Goal.prove_raw to Goal.prove_internal;
2007-06-13, by wenzelm
Method.Basic: include position;
2007-06-13, by wenzelm
tuned proofs: avoid implicit prems;
2007-06-13, by wenzelm
Basic text: include position;
2007-06-13, by wenzelm
thm antiquotations
2007-06-12, by huffman
add lemma inj_of_nat
2007-06-12, by huffman
thm antiquotations
2007-06-12, by huffman
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, by chaieb
changed int stuff into integer for SMLNJ compatibility
2007-06-12, by chaieb
more of_rat lemmas
2007-06-12, by huffman
add function of_rat and related lemmas
2007-06-12, by huffman
turned curry (op opr) into curry op opr --- because of smlnj
2007-06-12, by chaieb
De-overloaded operations for int and real.
2007-06-12, by wenzelm
SML basis with type int representing proper integers, not machine words.
2007-06-12, by wenzelm
Tuned proofs : now use 'algebra ad: ...'
2007-06-12, by chaieb
cooper_tac takes now two lists of theorems to be added/deleted from the simpset dor pre-simplification
2007-06-12, by chaieb
changed val restriction to local due to smlnj
2007-06-12, by chaieb
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, by chaieb
Added algebra_tac; tuned;
2007-06-12, by chaieb
Method now takes theorems to be added or deleted from a simpset for simplificatio before the core method starts
2007-06-12, by chaieb
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-12, by chaieb
nex example
2007-06-11, by nipkow
Conversion for computation on constants now depends on the context
2007-06-11, by chaieb
tuned setup for the fields instantiation for Groebner Bases;
2007-06-11, by chaieb
Added dependency on file Groebner_Basis.thy
2007-06-11, by chaieb
Added instantiation of algebra method to fields
2007-06-11, by chaieb
hid constant "dom"
2007-06-11, by nipkow
Removed from CVS, since obselete in the new Presburger Method;
2007-06-11, by chaieb
Generated reflected QE procedure for Presburger Arithmetic-- Cooper's Algorithm -- see HOL/ex/Reflected_Presburger.thy
2007-06-11, by chaieb
Added more examples
2007-06-11, by chaieb
Now only contains generic conversion for quantifier elimination in HOL
2007-06-11, by chaieb
A new tactic for Presburger;
2007-06-11, by chaieb
tuned
2007-06-11, by chaieb
Temporarily added theorems for QE that were in old Presburger.thy ; This will diseappear with the new Ferrante and Rackoff shortly;
2007-06-11, by chaieb
tuned tactic
2007-06-11, by chaieb
Temporarily use int instead of IntInf.int but Code generator should map HOL's int to ML's IntInf.int --- To be fixed
2007-06-11, by chaieb
tuned Proof and Document
2007-06-11, by chaieb
tuned Proof
2007-06-11, by chaieb
A new and cleaned up Theory for QE. for Presburger arithmetic
2007-06-11, by chaieb
Added new files for Presburger (cooper_data.ML, cooper.ML) and deleted old unused ones cooper_dec, cooper_proof, reflected_cooper etc..
2007-06-11, by chaieb
explicitely depends on file groebner.ML
2007-06-11, by chaieb
Context Data for the new presburger Method
2007-06-11, by chaieb
A new simpler and cleaner implementation of proof Synthesis for Presburger Arithmetic --- Cooper's Algorithm
2007-06-11, by chaieb
remove references to constant int::nat=>int
2007-06-11, by huffman
simplify int proofs
2007-06-11, by huffman
modify proofs to avoid referring to int::nat=>int
2007-06-11, by huffman
add int_of_nat versions of lemmas about int::nat=>int
2007-06-11, by huffman
add lemma of_nat_power
2007-06-11, by huffman
add int_of_nat versions of lemmas about int::nat=>int
2007-06-11, by huffman
add abbreviation int_of_nat for of_nat::nat=>int;
2007-06-11, by huffman
disabled theory "Reflected_Presburger" for smlnj (temporarily);
2007-06-10, by wenzelm
disabled theories MIR and ReflectedFerrack for smlnj (temporarily);
2007-06-10, by wenzelm
*** empty log message ***
2007-06-10, by nipkow
remove dependencies of proofs on constant int::nat=>int, preparing to remove it
2007-06-09, by huffman
eqtype int -- explicitly encourage overloaded equality;
2007-06-09, by wenzelm
simplified type integer;
2007-06-09, by wenzelm
Adapted Proofterm.bicompose_proof to Larry's changes in
2007-06-08, by berghofe
Method "algebra" solves polynomial equations over (semi)rings
2007-06-08, by chaieb
generalize zpower_number_of_{even,odd} lemmas
2007-06-08, by huffman
deleted comments
2007-06-07, by obua
deleted legacy lemmas
2007-06-07, by obua
somebody elses problem fixed
2007-06-07, by nipkow
filter syntax change
2007-06-07, by nipkow
remove redundant lemmas
2007-06-07, by huffman
remove references to preal-specific theorems
2007-06-07, by huffman
define (1::preal); clean up instance declarations
2007-06-07, by huffman
tuned
2007-06-07, by huffman
instance preal :: ordered_cancel_ab_semigroup_add
2007-06-07, by huffman
use new-style class for sq_ord; rename op << to sq_le
2007-06-06, by huffman
take out Class.thy again, because it does not yet compile cleanly
2007-06-06, by urbanc
add axclass semiring_char_0 for types where of_nat is injective
2007-06-06, by huffman
changed filter syntax from : to <-
2007-06-06, by nipkow
hide filter
2007-06-06, by nipkow
tuned list comprehension, changed filter syntax from : to <-
2007-06-06, by nipkow
clean up proofs of exp_zero, sin_zero, cos_zero
2007-06-06, by huffman
generalize class constraints on some lemmas
2007-06-06, by huffman
generalize of_nat and related constants to class semiring_1
2007-06-06, by huffman
declare complex_diff as simp rule
2007-06-06, by huffman
New Reflected Presburger added to HOL/ex
2007-06-06, by chaieb
Groebner Basis Examples.
2007-06-05, by wenzelm
print_antiquotations: sort_strings;
2007-06-05, by wenzelm
tuned document;
2007-06-05, by wenzelm
tuned source deps;
2007-06-05, by wenzelm
simplified/renamed add_numerals;
2007-06-05, by wenzelm