20070613 
wenzelm 
20070613 
tuned proofs: avoid implicit prems;
tuned;

changeset 
files

20070613 
wenzelm 
20070613 
tuned proofs: avoid implicit prems;
major cleanup of proofs/document;

changeset 
files

20070613 
wenzelm 
20070613 
tuned comments;

changeset 
files

20070613 
wenzelm 
20070613 
tuned proofs: avoid implicit prems;

changeset 
files

20070613 
huffman 
20070613 
clean up instance proofs; reorganize section headings

changeset 
files

20070613 
wenzelm 
20070613 
reactivated theory Class;

changeset 
files

20070613 
urbanc 
20070613 
added the Q_Unit rule (was missing) and adjusted the proof accordingly

changeset 
files

20070613 
wenzelm 
20070613 
* Isar: method "assumption" (implicit closing of subproofs) takes nonatomic goal assumptions into account;
* Isar: implicit use of prems from the Isar proof context is considered a legacy feature;

changeset 
files

20070613 
narboux 
20070613 
generate_fresh works even if there is no free variable in the goal

changeset 
files

20070613 
wenzelm 
20070613 
tuned;

changeset 
files

20070613 
wenzelm 
20070613 
tuned proofs: avoid implicit prems;

changeset 
files

20070613 
huffman 
20070613 
removed constant int :: nat => int;
int is now an abbreviation for of_nat :: nat => int

changeset 
files

20070613 
huffman 
20070613 
thm antiquotations

changeset 
files

20070613 
wenzelm 
20070613 
transaction: context_position (nondestructive only);

changeset 
files

20070613 
wenzelm 
20070613 
added map_current;
simplified internal type proof;

changeset 
files

20070613 
wenzelm 
20070613 
tuned msg;

changeset 
files

20070613 
wenzelm 
20070613 
apply_method/end_proof: pass position;
Method.Basic: include position;

changeset 
files

20070613 
wenzelm 
20070613 
renamed map to map_current;

changeset 
files

20070613 
wenzelm 
20070613 
tuned;

changeset 
files

20070613 
wenzelm 
20070613 
removed unused is_atomic;

changeset 
files

20070613 
wenzelm 
20070613 
renamed prove_raw to prove_internal;
tuned;

changeset 
files

20070613 
wenzelm 
20070613 
merge/merge_refs: plain error instead of exception TERM;

changeset 
files

20070613 
wenzelm 
20070613 
Context positions.

changeset 
files

20070613 
wenzelm 
20070613 
added context_position.ML;

changeset 
files

20070613 
wenzelm 
20070613 
renamed Goal.prove_raw to Goal.prove_internal;

changeset 
files

20070613 
wenzelm 
20070613 
Method.Basic: include position;

changeset 
files

20070613 
wenzelm 
20070613 
tuned proofs: avoid implicit prems;

changeset 
files

20070613 
wenzelm 
20070613 
Basic text: include position;
assumption/close: refer to nonatomic assumptions as well, implicit use of prems now considered legacy feature;

changeset 
files

20070612 
huffman 
20070612 
thm antiquotations

changeset 
files

20070612 
huffman 
20070612 
add lemma inj_of_nat

changeset 
files

20070612 
huffman 
20070612 
thm antiquotations

changeset 
files

20070612 
chaieb 
20070612 
Unfortunately needed patch due to incompatibility with SML  oo is infix and hence can not appear on the left handside of patterns

changeset 
files

20070612 
chaieb 
20070612 
changed int stuff into integer for SMLNJ compatibility

changeset 
files

20070612 
huffman 
20070612 
more of_rat lemmas

changeset 
files

20070612 
huffman 
20070612 
add function of_rat and related lemmas

changeset 
files

20070612 
chaieb 
20070612 
turned curry (op opr) into curry op opr  because of smlnj

changeset 
files

20070612 
wenzelm 
20070612 
Deoverloaded operations for int and real.

changeset 
files

20070612 
wenzelm 
20070612 
SML basis with type int representing proper integers, not machine words.

changeset 
files

20070612 
chaieb 
20070612 
Tuned proofs : now use 'algebra ad: ...'

changeset 
files

20070612 
chaieb 
20070612 
cooper_tac takes now two lists of theorems to be added/deleted from the simpset dor presimplification

changeset 
files

20070612 
chaieb 
20070612 
changed val restriction to local due to smlnj

changeset 
files

20070612 
chaieb 
20070612 
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;

changeset 
files

20070612 
chaieb 
20070612 
Added algebra_tac; tuned;

changeset 
files

20070612 
chaieb 
20070612 
Method now takes theorems to be added or deleted from a simpset for simplificatio before the core method starts

changeset 
files

20070612 
chaieb 
20070612 
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

changeset 
files

20070611 
nipkow 
20070611 
nex example

changeset 
files

20070611 
chaieb 
20070611 
Conversion for computation on constants now depends on the context

changeset 
files

20070611 
chaieb 
20070611 
tuned setup for the fields instantiation for Groebner Bases;

changeset 
files

20070611 
chaieb 
20070611 
Added dependency on file Groebner_Basis.thy

changeset 
files

20070611 
chaieb 
20070611 
Added instantiation of algebra method to fields

changeset 
files

20070611 
nipkow 
20070611 
hid constant "dom"

changeset 
files

20070611 
chaieb 
20070611 
Removed from CVS, since obselete in the new Presburger Method;

changeset 
files

20070611 
chaieb 
20070611 
Generated reflected QE procedure for Presburger Arithmetic Cooper's Algorithm  see HOL/ex/Reflected_Presburger.thy

changeset 
files

20070611 
chaieb 
20070611 
Added more examples

changeset 
files

20070611 
chaieb 
20070611 
Now only contains generic conversion for quantifier elimination in HOL

changeset 
files

20070611 
chaieb 
20070611 
A new tactic for Presburger;

changeset 
files

20070611 
chaieb 
20070611 
tuned

changeset 
files

20070611 
chaieb 
20070611 
Temporarily added theorems for QE that were in old Presburger.thy ; This will diseappear with the new Ferrante and Rackoff shortly;

changeset 
files

20070611 
chaieb 
20070611 
tuned tactic

changeset 
files

20070611 
chaieb 
20070611 
Temporarily use int instead of IntInf.int but Code generator should map HOL's int to ML's IntInf.int  To be fixed

changeset 
files
