Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-10000
-3000
-1000
-448
+448
+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.
New wrapper for defining inductive sets with new inductive
2007-07-11, by berghofe
Old (co)inductive command is now replaced by (co)inductive_set.
2007-07-11, by berghofe
Reorganization due to introduction of inductive_set wrapper.
2007-07-11, by berghofe
Improved code generator for Collect.
2007-07-11, by berghofe
Renamed inductive2 to inductive.
2007-07-11, by berghofe
Fix nested PGIP messages. Update for schema simplifications.
2007-07-11, by aspinall
Moved unify_consts to PrimrecPackage.
2007-07-11, by berghofe
- Renamed inductive2 to inductive
2007-07-11, by berghofe
Adapted to changes in Predicate theory.
2007-07-11, by berghofe
Adapted to new inductive definition package.
2007-07-11, by berghofe
Renamed accessible part for predicates to accp.
2007-07-11, by berghofe
Track schema changes: merge messagecategory with area attributes
2007-07-11, by aspinall
bot is now a constant.
2007-07-11, by berghofe
Restored set notation.
2007-07-11, by berghofe
- Renamed inductive2 to inductive
2007-07-11, by berghofe
Track schema changes: remove cleardisplay, proofstate messages. Simplify attributes on cleardisplay, normalresponse.
2007-07-11, by aspinall
Track schema changes: add area attribute to pgml packet. Also add quoted Raw element [hack for Isabelle bottom-up XML production]
2007-07-11, by aspinall
Renamed inductive2 to inductive.
2007-07-11, by berghofe
Adapted to new inductive definition package.
2007-07-11, by berghofe
New operations on tuples with specific arities.
2007-07-11, by berghofe
Adapted to changes in infrastructure for converting between
2007-07-11, by berghofe
rtrancl and trancl are now defined using inductive_set.
2007-07-11, by berghofe
Removed wf_implies_wfP and wfP_implies_wf from list of hints again.
2007-07-11, by berghofe
- Moved infrastructure for converting between sets and predicates
2007-07-11, by berghofe
Adapted to new package for inductive sets.
2007-07-11, by berghofe
Inserted definition of in_rel again (since member2 was removed).
2007-07-11, by berghofe
Added ML bindings for sup_fun_eq and sup_bool_eq.
2007-07-11, by berghofe
top and bot are now constants.
2007-07-11, by berghofe
Renamed inductive2 to inductive.
2007-07-11, by berghofe
acc is now defined using inductive_set.
2007-07-11, by berghofe
Added new package for inductive sets.
2007-07-11, by berghofe
Adapted to new inductive definition package.
2007-07-11, by berghofe
Adapted to changes in inductive definition package.
2007-07-11, by berghofe
tuned comment markup;
2007-07-11, by wenzelm
treat OuterLex.Error;
2007-07-11, by wenzelm
separated Malformed (symbolic char) from Error (bad input);
2007-07-11, by wenzelm
Output.escape_malformed;
2007-07-11, by wenzelm
added escape_malformed (failsafe);
2007-07-11, by wenzelm
Basic editing of theory sources.
2007-07-10, by wenzelm
tuned;
2007-07-10, by wenzelm
export html_mode, begin_document, end_document;
2007-07-10, by wenzelm
renamed XML.Rawtext to XML.Output;
2007-07-10, by wenzelm
export get_lexicons;
2007-07-10, by wenzelm
added kind_of;
2007-07-10, by wenzelm
Markup.enclose;
2007-07-10, by wenzelm
more markup for inner and outer syntax;
2007-07-10, by wenzelm
simplified funpow, untabify;
2007-07-10, by wenzelm
added Thy/thy_edit.ML;
2007-07-10, by wenzelm
added some markup for outer syntax;
2007-07-10, by wenzelm
clarified merge of module names
2007-07-10, by haftmann
now a monolithic module
2007-07-10, by haftmann
now works with SML/NJ
2007-07-10, by haftmann
tuned
2007-07-10, by haftmann
improvement for code names
2007-07-10, by haftmann
removed proof dependency on transitivity theorems
2007-07-10, by haftmann
moved lfp_induct2 here
2007-07-10, by haftmann
clarified import
2007-07-10, by haftmann
moved lfp_induct2 to Relation.thy
2007-07-10, by haftmann
moved some finite lemmas here
2007-07-10, by haftmann
moved finite lemmas to Finite_Set.thy
2007-07-10, by haftmann
added print_mode setup (from pretty.ML);
2007-07-10, by wenzelm
Markup.add_mode;
2007-07-10, by wenzelm
removed no_state markup -- produce empty state;
2007-07-10, by wenzelm
Markup.output;
2007-07-10, by wenzelm
moved source cascading from scan.ML to source.ML;
2007-07-10, by wenzelm
infixr || (more efficient);
2007-07-10, by wenzelm
moved print_mode setup for markup to markup.ML;
2007-07-10, by wenzelm
Markup.output;
2007-07-10, by wenzelm
use position.ML earlier;
2007-07-10, by wenzelm
Add widthN to signature
2007-07-10, by aspinall
cd ISABELLE_HOME/etc;
2007-07-10, by wenzelm
adjusted
2007-07-10, by haftmann
updated keywords
2007-07-10, by haftmann
simplified, tuned
2007-07-10, by haftmann
re-expanded paths
2007-07-10, by haftmann
replaced code generator framework for reflected cooper
2007-07-10, by haftmann
expanded fragile proof
2007-07-10, by haftmann
extended - convers now basic lcm properties also
2007-07-10, by haftmann
constant dvd now in class target
2007-07-10, by haftmann
moved lemma zdvd_period here
2007-07-10, by haftmann
introduced (auxiliary) class dvd_mod for more convenient code generation
2007-07-10, by haftmann
tuned;
2007-07-10, by wenzelm
nested source: explicit interactive flag for recover avoids duplicate errors;
2007-07-10, by wenzelm
tuned dead code;
2007-07-09, by wenzelm
use Position.file_of;
2007-07-09, by wenzelm
toplevel_source: interactive flag indicates intermittent error_msg;
2007-07-09, by wenzelm
Malformed token: error msg;
2007-07-09, by wenzelm
adapted OuterLex/T.source;
2007-07-09, by wenzelm
scan: changed treatment of malformed symbols, passed to next stage;
2007-07-09, by wenzelm
nested source: error msg passed to recover;
2007-07-09, by wenzelm
tuned signature;
2007-07-09, by wenzelm
replaced name by file (unquoted);
2007-07-09, by wenzelm
moved Path.position to Position.path;
2007-07-09, by wenzelm
proper position markup;
2007-07-09, by wenzelm
use position.ML after pretty.ML;
2007-07-09, by wenzelm
removed target RAW-ProofGeneral (impractical to maintain);
2007-07-09, by wenzelm
declare: disallow quote (") in names;
2007-07-09, by wenzelm
removed legacy ML file;
2007-07-09, by wenzelm
HOL-Complex-Matrix: fixed deps -- sort of;
2007-07-09, by wenzelm
adopted to new computing oracle and fixed bugs introduced by tuning
2007-07-09, by obua
added computing oracle support for HOL and numerals
2007-07-09, by obua
new version of computing oracle
2007-07-09, by obua
simplified writeln_fn;
2007-07-09, by wenzelm
prompt: plain string, not output;
2007-07-09, by wenzelm
type output = string indicates raw system output;
2007-07-09, by wenzelm
symbolic output: avoid empty blocks, 1 space for fbreak;
2007-07-08, by wenzelm
tuned;
2007-07-08, by wenzelm
thm tag: Markup.property list;
2007-07-08, by wenzelm
gensym: slightly more obscure prefix descreases probability of name clash;
2007-07-08, by wenzelm
replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
2007-07-08, by wenzelm
attribute tagged: single argument;
2007-07-08, by wenzelm
updated;
2007-07-08, by wenzelm
simplified Symtab;
2007-07-08, by wenzelm
renamed ML_exc to ML_exn;
2007-07-08, by wenzelm
Show the use of reflection attribute; fixed comments about the order of absorbing equations : f (C x) = x ; now automaically tried as last;
2007-07-08, by chaieb
Changed syntax for the reflection method (reify unchanged). reflection takes an optional set of theorems for reification then several correctness theorems are specified by rules:'' then the optional term is specified by only:
2007-07-08, by chaieb
Try several correctness theorems for reflection; rearrange cong rules to avoid the absoption cases;
2007-07-08, by chaieb
Context data now consist of eqations for reification and equations for correctness theorems for reflection; Added attribute reflection to store correctness theorems to be trued by default
2007-07-08, by chaieb
simplified/more robust print_state;
2007-07-08, by wenzelm
export mode_markup;
2007-07-08, by wenzelm
added markup for pretty printing;
2007-07-08, by wenzelm
Corrected erronus use of compiletime context to the runtime context
2007-07-08, by chaieb
make smlnj happy;
2007-07-07, by wenzelm
toplevel prompt/print_state: proper markup, removed hooks;
2007-07-07, by wenzelm
toplevel prompt/print_state: proper markup, removed hooks;
2007-07-07, by wenzelm
pretty_state: subgoal markup;
2007-07-07, by wenzelm
added markup_chunks;
2007-07-07, by wenzelm
added toplevel markup;
2007-07-07, by wenzelm
use markup.ML earlier;
2007-07-07, by wenzelm
removed obsolete disable_pr/enable_pr;
2007-07-07, by wenzelm
pretty_goals_aux: subgoal markup;
2007-07-07, by wenzelm
pr_goals: adapted Display.pretty_goals_aux;
2007-07-07, by wenzelm
export attribute;
2007-07-07, by wenzelm
pretty_sort/typ/term: markup;
2007-07-07, by wenzelm
pretty: markup for syntax/name of authentic consts;
2007-07-07, by wenzelm
depend on alist.ML, markup.ML;
2007-07-07, by wenzelm
markup: emit as control information -- no indent text;
2007-07-07, by wenzelm
added property conversions;
2007-07-07, by wenzelm
position: line and name;
2007-07-07, by wenzelm
moved markup.ML before position.ML;
2007-07-07, by wenzelm
The order for parameter for interpretation is now inversted:
2007-07-07, by chaieb
Common markup elements.
2007-07-07, by wenzelm
simplified pretty token metric: type int;
2007-07-07, by wenzelm
simplified pretty token metric: type int;
2007-07-07, by wenzelm
moved General/xml.ML to Tools/xml.ML;
2007-07-07, by wenzelm
tuned;
2007-07-07, by wenzelm
simplified output mode setup;
2007-07-07, by wenzelm
added print_mode setup: indent and markup;
2007-07-07, by wenzelm
renamed raw to escape;
2007-07-07, by wenzelm
simplified pretty token metric: type int;
2007-07-07, by wenzelm
moved General/xml.ML to Tools/xml.ML;
2007-07-07, by wenzelm
added General/markup.ML;
2007-07-07, by wenzelm
added class skolem, command;
2007-07-07, by wenzelm
more interpretations
2007-07-06, by nipkow
Produce good PGML 2.0
2007-07-06, by aspinall
cosmetic (line length fixed)
2007-07-06, by webertj
Some examples for reifying type variables
2007-07-06, by chaieb
Tuned document
2007-07-06, by chaieb
Cleaned add and del attributes
2007-07-06, by chaieb
Reification now deals with type variables
2007-07-06, by chaieb
Cumulative reports for Poly/ML profiling output.
2007-07-06, by wenzelm
Update PGML version, add system name
2007-07-05, by aspinall
tuned interfaces: atomize, atomize_prems, atomize_prems_tac;
2007-07-05, by wenzelm
added type conv;
2007-07-05, by wenzelm
removed comments -- no exception TERM;
2007-07-05, by wenzelm
added is_reflexive;
2007-07-05, by wenzelm
tuned;
2007-07-05, by wenzelm
simplified has_meta_prems;
2007-07-05, by wenzelm
moved type conv to thm.ML;
2007-07-05, by wenzelm
the_theory/proof: error instead of exception Fail;
2007-07-05, by wenzelm
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
2007-07-05, by wenzelm
renamed Conv.is_refl to Thm.is_reflexive;
2007-07-05, by wenzelm
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
2007-07-05, by wenzelm
simplified ObjectLogic.atomize;
2007-07-05, by wenzelm
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
2007-07-05, by wenzelm
Revert body of pgml to match schema for now [change bad for Broker]
2007-07-05, by aspinall
Classify -- comments as ordinary comments (no undo)
2007-07-05, by aspinall
tuned;
2007-07-05, by wenzelm
avoid polymorphic equality;
2007-07-05, by wenzelm
sort_le: tuned eq case;
2007-07-05, by wenzelm
tuned goal conversion interfaces;
2007-07-05, by wenzelm
else_conv: only handle THM | CTERM | TERM | TYPE;
2007-07-05, by wenzelm
avoid polymorphic equality;
2007-07-05, by wenzelm
tuned;
2007-07-05, by wenzelm
moved mk_cnumeral/mk_cnumber to Tools/numeral.ML;
2007-07-05, by wenzelm
avoid polymorphic equality;
2007-07-05, by wenzelm
avoid polymorphic equality;
2007-07-05, by wenzelm
avoid polymorphic equality;
2007-07-05, by wenzelm
removed dest_cTrueprop (cf. ObjectLogic.dest_judgment);
2007-07-05, by wenzelm
Logical operations on numerals (see also HOL/hologic.ML).
2007-07-05, by wenzelm
added Tools/numeral.ML;
2007-07-05, by wenzelm
common normalizer_funs, avoid cterm_of;
2007-07-05, by wenzelm
Numeral.mk_cnumber;
2007-07-05, by wenzelm
PGML abstraction, draft version
2007-07-04, by aspinall
Use pgml
2007-07-04, by aspinall
fixed argument order in calls to Integer.pow
2007-07-04, by obua
added binop_cong_rule;
2007-07-04, by wenzelm
export dlo_conv;
2007-07-04, by wenzelm
replaced HOLogic.Trueprop_conv by ObjectLogic.judgment_conv;
2007-07-04, by wenzelm
*** empty log message ***
2007-07-04, by nipkow
*** empty log message ***
2007-07-04, by nipkow
simplified a proof
2007-07-04, by paulson
tuned;
2007-07-03, by wenzelm
CONVERSION: handle TYPE | TERM | CTERM | THM;
2007-07-03, by wenzelm
proper use of ioa_package.ML;
2007-07-03, by wenzelm
tuned;
2007-07-03, by wenzelm
tuned is_comb/is_binop -- avoid construction of cterms;
2007-07-03, by wenzelm
HOLogic.conj_intr/elims;
2007-07-03, by wenzelm
use mucke_oracle.ML only once;
2007-07-03, by wenzelm
assume basic HOL context for compilation (antiquotations);
2007-07-03, by wenzelm
proper use of function_package ML files;
2007-07-03, by wenzelm
use hologic.ML in basic HOL context;
2007-07-03, by wenzelm
to handle non-atomic assumptions
2007-07-03, by paulson
rename class dom to ring_1_no_zero_divisors (cf. HOL/Ring_and_Field.thy 1.84 by huffman);
2007-07-03, by wenzelm
convert instance proofs to Isar style
2007-07-03, by huffman
Dependency on reflection_data.ML to build HOL-ex
2007-07-03, by chaieb
Generalized case for atoms. Selection of environment lists is allowed more than once.
2007-07-03, by chaieb
More examples
2007-07-03, by chaieb
reflection and reification methods now manage Context data
2007-07-03, by chaieb
Context Data for the reflection and reification methods
2007-07-03, by chaieb
rename class dom to ring_1_no_zero_divisors
2007-07-03, by huffman
rewrite_goal_tac;
2007-07-03, by wenzelm
replaced Conv.goals_conv by Conv.prems_conv;
2007-07-03, by wenzelm
exported meta_rewrite_conv;
2007-07-03, by wenzelm
CONVERSION tactical;
2007-07-03, by wenzelm
removed obsolete eta_long_tac;
2007-07-03, by wenzelm
added CONVERSION tactical;
2007-07-03, by wenzelm
tuned rotate_prems;
2007-07-03, by wenzelm
moved (asm_)rewrite_goal_tac from goal.ML to meta_simplifier.ML (no longer depends on SELECT_GOAL);
2007-07-03, by wenzelm
removed obsolete mk_conjunction_list, intr/elim_list;
2007-07-03, by wenzelm
removed obsolete goals_conv (cf. prems_conv);
2007-07-03, by wenzelm
Conjunction.intr/elim_balanced;
2007-07-03, by wenzelm
CONVERSION tactical;
2007-07-03, by wenzelm
Conjunction.mk_conjunction_balanced;
2007-07-03, by wenzelm
CONVERSION tactical;
2007-07-03, by wenzelm
Fixed problem with patterns in lambdas
2007-07-03, by nipkow
fixed an issue with mutual recursion
2007-07-03, by krauss
instance pordered_comm_ring < pordered_ring
2007-07-03, by huffman
Added pattern maatching for lambda abstraction
2007-07-02, by nipkow
revised the discussion of type classes
2007-07-02, by paulson
Generic QE need no Context anymore
2007-07-02, by chaieb
Handle exception TYPE
2007-07-02, by chaieb
Tuned proofs
2007-07-02, by chaieb
added ordered_ring and ordered_semiring
2007-06-30, by obua
tuned arithmetic modules
2007-06-29, by haftmann
bug fixes to proof reconstruction
2007-06-29, by paulson
dropped local cg cmd
2007-06-29, by haftmann
dropped toplevel lcm, gcd
2007-06-28, by haftmann
proper collapse_let
2007-06-28, by haftmann
new code generator framework
2007-06-28, by haftmann
dropped Library.lcm
2007-06-28, by haftmann
tuned
2007-06-28, by haftmann
code generation for dvd
2007-06-28, by haftmann
simplified keyword setup
2007-06-28, by haftmann
GPL -> BSD
2007-06-27, by paulson
*** empty log message ***
2007-06-27, by nipkow
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
less
more
|
(0)
-10000
-3000
-1000
-448
+448
+1000
+3000
+10000
+30000
tip