Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-10000
-3000
-1000
-224
+224
+1000
+3000
+10000
+30000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
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
renamed ex/Eval_Examples.thy;
2007-06-05, by wenzelm
added ex/Groebner_Examples.thy;
2007-06-05, by wenzelm
tuned document;
2007-06-05, by wenzelm
Added two examples in Complex/ex :Reflected QE for linear real arith and QE for mixed integer real linear arithmetic
2007-06-05, by chaieb
Added twe Examples for Quantifier elimination ofer linear real arithmetic and over the mixed theory of linear real artihmetic with integers
2007-06-05, by chaieb
tuned boostrap
2007-06-05, by haftmann
eliminated Code_Generator.thy
2007-06-05, by haftmann
tuned integers
2007-06-05, by haftmann
tuned;
2007-06-05, by wenzelm
fixed type int vs. integer;
2007-06-05, by wenzelm
renamed locale ring/semiring to gb_ring/gb_semiring to avoid clash with Ring_and_Field versions;
2007-06-05, by wenzelm
add new lemmas
2007-06-05, by huffman
Polynomials now only depend on Deriv; Definition of degree changed
2007-06-05, by chaieb
lemma lemma_DERIV_subst moved to Deriv.thy
2007-06-05, by chaieb
tuned proofs;
2007-06-05, by wenzelm
tuned comments;
2007-06-05, by wenzelm
Semiring normalization and Groebner Bases.
2007-06-05, by wenzelm
moved generic algebra modules
2007-06-05, by haftmann
updated documentation
2007-06-05, by haftmann
fixed broken execption handling
2007-06-05, by haftmann
simplified notion of "operational classes"
2007-06-05, by haftmann
merged Code_Generator.thy into HOL.thy
2007-06-05, by haftmann
added a function partition and a few lemmas
2007-06-05, by chaieb
added a few theorems about foldl and set
2007-06-05, by chaieb
added lcm, ilcm (lcm for integers) and some lemmas about them;
2007-06-05, by chaieb
included Class.thy in the compiling process for Nominal/Examples
2007-06-05, by urbanc
remove simp attribute from lemma_STAR theorems
2007-06-05, by huffman
add lemma exp_of_real
2007-06-05, by huffman
tuned list comprehension
2007-06-04, by nipkow
tuned;
2007-06-04, by wenzelm
added is_atomic;
2007-06-04, by wenzelm
added assume_rule_tac;
2007-06-04, by wenzelm
reverted appnd to append
2007-06-04, by haftmann
authentic syntax for List.append
2007-06-04, by haftmann
tuned comments
2007-06-04, by haftmann
added a few comments to the proofs
2007-06-04, by urbanc
removed fixmes
2007-06-04, by chaieb
opaque-constraint removed
2007-06-04, by chaieb
tuned;
2007-06-04, by chaieb
monomorphic equality: let ML work out the details;
2007-06-03, by wenzelm
added gen_merge_lists/merge_lists/merge_alists (legacy operations from library.ML);
2007-06-03, by wenzelm
tuned Tactic signature;
2007-06-03, by wenzelm
removed obsolete Library.seq;
2007-06-03, by wenzelm
moved flip to library.ML;
2007-06-03, by wenzelm
added CSUBGOAL;
2007-06-03, by wenzelm
cleaned up signature;
2007-06-03, by wenzelm
added downto0 (from library.ML);
2007-06-03, by wenzelm
merge_ss: plain merge of prems;
2007-06-03, by wenzelm
added flip (from General/basics.ML);
2007-06-03, by wenzelm
tuned document;
2007-06-03, by wenzelm
use antiquotations instead of raw TeX code;
2007-06-03, by wenzelm
name_of_fqgar: precise type;
2007-06-03, by wenzelm
added plural (from Pure/library.ML);
2007-06-03, by wenzelm
local open FundefLib;
2007-06-03, by wenzelm
renamed gen_submultiset to submultiset;
2007-06-03, by wenzelm
HOL-ex: tuned deps;
2007-06-03, by wenzelm
tuned list comprehension, added lemma
2007-06-03, by nipkow
fixed tex error
2007-06-03, by nipkow
*** empty log message ***
2007-06-03, by nipkow
*** empty log message ***
2007-06-03, by nipkow
extended
2007-06-02, by webertj
cosmetic
2007-06-02, by webertj
made SML/NJ happy;
2007-06-02, by wenzelm
added target/local_abbrev (from proof_context.ML);
2007-06-02, by wenzelm
moved specific target/local_abbrev to theory_target.ML;
2007-06-02, by wenzelm
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
2007-06-02, by krauss
added "plural : 'a -> 'a -> 'b list -> 'a" for convenient error msg construction
2007-06-02, by krauss
proper handling of Tools;
2007-06-02, by wenzelm
cosmetic
2007-06-02, by webertj
refute_tac made more deterministic
2007-06-02, by webertj
extended
2007-06-02, by webertj
cosmetic
2007-06-02, by webertj
tracing disabled
2007-06-02, by webertj
additional tracing information
2007-06-01, by webertj
tuned
2007-06-01, by webertj
some tests for arith added
2007-06-01, by webertj
Moved list comprehension into List
2007-06-01, by nipkow
MiniSAT mentioned in comment
2007-06-01, by webertj
fixed handling of meta-logic propositions
2007-06-01, by webertj
simplified interfaces, some restructuring
2007-06-01, by krauss
updated
2007-06-01, by krauss
added some bibtex entries
2007-06-01, by krauss
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
2007-06-01, by krauss
Added simp-rules: "R O {} = {}" and "{} O R = {}"
2007-06-01, by krauss
rudimenary
2007-06-01, by haftmann
tuned
2007-06-01, by haftmann
dropped superfluous name bindings
2007-06-01, by haftmann
localized
2007-06-01, by haftmann
fixed typo
2007-06-01, by haftmann
insert: canonical argument order;
2007-05-31, by wenzelm
simplified/unified list fold;
2007-05-31, by wenzelm
replace (- 1) with -1
2007-05-31, by huffman
simplify some proofs
2007-05-31, by huffman
tuned headers -- adapted to usual conventions;
2007-05-31, by wenzelm
moved Compute_Oracle from Pure/Tools to Tools;
2007-05-31, by wenzelm
proper theory setup for compute oracle (based on CPure);
2007-05-31, by wenzelm
moved IsaPlanner from Provers to Tools;
2007-05-31, by wenzelm
moved IsaPlanner from Provers to Tools;
2007-05-31, by wenzelm
made aconvc pervasive;
2007-05-31, by wenzelm
moved aconvc to more_thm.ML;
2007-05-31, by wenzelm
tuned ML setup;
2007-05-31, by wenzelm
decode_term: force qualified name into Const;
2007-05-31, by wenzelm
proper loading of ML files (in HOL.thy);
2007-05-31, by wenzelm
HOL_proofs;
2007-05-31, by wenzelm
moved Integ files to canonical place;
2007-05-31, by wenzelm
proper loading of ML files;
2007-05-31, by wenzelm
removed dead code;
2007-05-31, by wenzelm
tuned header;
2007-05-31, by wenzelm
doc: exclude isabelle_isar.pdf;
2007-05-31, by wenzelm
tuned the proof
2007-05-31, by urbanc
introduced symmetric variants of the lemmas for alpha-equivalence
2007-05-31, by urbanc
proper loading of ML files;
2007-05-31, by wenzelm
removed obsolete IFOL.thy/FOL.thy values;
2007-05-31, by wenzelm
less
more
|
(0)
-10000
-3000
-1000
-224
+224
+1000
+3000
+10000
+30000
tip