Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-10000
-1792
+1792
+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.
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
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
proper loading of ML files;
2007-05-31, by wenzelm
tuned header;
2007-05-31, by wenzelm
tuned oracle setup;
2007-05-31, by wenzelm
moved HOLCF tools to canonical place;
2007-05-31, by wenzelm
moved TFL files to canonical place;
2007-05-31, by wenzelm
moved TFL files to canonical place;
2007-05-31, by wenzelm
added src/Tools;
2007-05-31, by wenzelm
fixed title;
2007-05-31, by wenzelm
Tools: generic tools outside of Pure.
2007-05-31, by wenzelm
moved Integ files to canonical place;
2007-05-31, by wenzelm
fixed use_thy "LocalWeakening";
2007-05-31, by wenzelm
included new example in the compiling process
2007-05-31, by urbanc
a theory using locally nameless terms and strong induction principles
2007-05-31, by urbanc
tuned the proof
2007-05-31, by urbanc
emulate later version of TextIO.inputLine;
2007-05-31, by wenzelm
reversed SML B library patches;
2007-05-31, by wenzelm
TextIO.inputLine: use present SML B library version;
2007-05-31, by wenzelm
tuned USEDIR_OPTIONS;
2007-05-30, by wenzelm
removed HOL4 image, which seldom works;
2007-05-30, by wenzelm
simplified data setup
2007-05-30, by haftmann
instance: always print sorts on failure
2007-05-30, by haftmann
more example
2007-05-30, by haftmann
fixed typo
2007-05-30, by haftmann
updated
2007-05-30, by haftmann
generalized lemmas
2007-05-30, by haftmann
eliminated strings
2007-05-30, by haftmann
tuned
2007-05-30, by haftmann
clarified error message
2007-05-30, by krauss
simplify names of locale interpretations
2007-05-30, by huffman
renamed some lemmas in Complex.thy
2007-05-30, by huffman
cleaned up proofs; reorganized sections; removed redundant lemmas
2007-05-30, by huffman
use new-style instance declarations
2007-05-29, by huffman
instance complex :: banach
2007-05-29, by huffman
add lemma real_sqrt_sum_squares_less
2007-05-29, by huffman
cleaned up some proofs
2007-05-29, by huffman
interpretation bounded_linear_divide
2007-05-29, by huffman
add bounded_linear lemmas
2007-05-29, by huffman
add isUCont lemmas
2007-05-29, by huffman
updated examples to include an instance of (lexicographic_order simp:...)
2007-05-29, by krauss
Complex: generalized type of exp
2007-05-28, by huffman
generalized exp to work over any complete field; new proof of exp_add
2007-05-28, by huffman
add type annotations for exp
2007-05-28, by huffman
interpretations additive_scaleR_left, additive_scaleR_right
2007-05-28, by huffman
remove division_by_zero requirement from termdiffs lemmas; cleaned up some proofs
2007-05-28, by huffman
new proof of Cauchy product formula for series
2007-05-27, by huffman
What it says
2007-05-26, by nipkow
improved error handling
2007-05-25, by haftmann
using rudimentary class target mechanism
2007-05-25, by haftmann
*** empty log message ***
2007-05-25, by haftmann
fixed typo
2007-05-25, by haftmann
fix typos
2007-05-25, by huffman
*** empty log message ***
2007-05-25, by nipkow
*** empty log message ***
2007-05-25, by nipkow
*** empty log message ***
2007-05-25, by nipkow
tuned
2007-05-25, by nipkow
Added List_Comprehension
2007-05-25, by nipkow
adapted to fix for fresh_fun_simp
2007-05-25, by urbanc
took out Class.thy from the compiling process until memory problems are solved
2007-05-25, by urbanc
simplify some proofs
2007-05-25, by huffman
*** empty log message ***
2007-05-24, by nipkow
Squared things out.
2007-05-24, by obua
fix a bug : the semantics of no_asm was the opposite
2007-05-24, by narboux
temporary fix for a bug in fresh_fun_simp
2007-05-24, by urbanc
formalisation of my PhD (the result was correct, but the proof needed several corrections)
2007-05-24, by urbanc
add an option in fresh_fun_simp to prevent rewriting in assumptions
2007-05-24, by narboux
fixes tvar issue in type inference
2007-05-24, by haftmann
tuned
2007-05-24, by haftmann
tuned warning
2007-05-24, by haftmann
rudimentary class target implementation
2007-05-24, by haftmann
tuned Pure/General/name_space.ML
2007-05-24, by haftmann
Introduced new classes monoid_add and group_add
2007-05-24, by nipkow
add lemma complete_algebra_summable_geometric
2007-05-23, by huffman
formatting
2007-05-23, by paulson
generalize powerseries and termdiffs lemmas using axclasses
2007-05-23, by huffman
remove unused simproc definition
2007-05-23, by huffman
remove redundant simproc; remove legacy ML bindings
2007-05-23, by huffman
remove redundant simproc
2007-05-23, by huffman
new simp rule Infinitesimal_of_hypreal_iff
2007-05-22, by huffman
removed redundant lemmas
2007-05-22, by huffman
generalize uniqueness of limits to class real_normed_algebra_1
2007-05-22, by huffman
Some hacks for SPASS format
2007-05-22, by paulson
some optimizations, cleanup
2007-05-22, by krauss
add missing instance declarations
2007-05-22, by huffman
adjusted to change in Provers/Arith/combine_numerals.ML
2007-05-22, by haftmann
adjusted to change in Provers/Arith/combine_numerals.ML
2007-05-22, by haftmann
regression tests: send failure reports to krauss@in.tum.de, too
2007-05-22, by krauss
rename lemmas LIM_ident, isCont_ident, DERIV_ident
2007-05-22, by huffman
remove obsolete CSeries.thy
2007-05-22, by huffman
generalized ring_eq_cancel simprocs to class idom; removed redundant field_eq_cancel simprocs
2007-05-22, by huffman
new field_combine_numerals simproc, which uses fractions as coefficients
2007-05-21, by huffman
search bottom up to get the inner fresh fun
2007-05-21, by narboux
add a bottom up search function
2007-05-21, by narboux
tuned
2007-05-21, by haftmann
evaluation for integers
2007-05-21, by haftmann
added lemma divAlg_div_mof
2007-05-21, by haftmann
improved code for rev
2007-05-21, by haftmann
min/max
2007-05-21, by haftmann
generalize CombineNumerals functor to allow coefficients with types other than IntInf.int
2007-05-21, by huffman
add lemmas divide_numeral_1 and inverse_numeral_1
2007-05-21, by huffman
fixed signature
2007-05-21, by krauss
Method "lexicographic_order" now takes the same arguments as "auto"
2007-05-21, by krauss
change fresh_fun_simp to treat occurences in assumptions and try to solve the generated subgoals
2007-05-21, by narboux
define pi with THE instead of SOME; cleaned up
2007-05-20, by huffman
add lemmas for sin,cos,tan of 30,45,60 degrees; cleaned up
2007-05-20, by huffman
add lemma power2_eq_imp_eq
2007-05-20, by huffman
added lemma for permutations on strings
2007-05-20, by urbanc
moved sqrt lemmas from Transcendental.thy to NthRoot.thy
2007-05-20, by huffman
remove obsolete DERIV_ln lemmas
2007-05-20, by huffman
add realpow_pos_nth2 back in
2007-05-20, by huffman
add odd_real_root lemmas
2007-05-20, by huffman
add lemmas about inverse functions; cleaned up proof of polar_ex
2007-05-20, by huffman
change premises of DERIV_inverse_function lemma
2007-05-20, by huffman
rearranged sections
2007-05-20, by huffman
add lemmas about continuity and derivatives of roots
2007-05-20, by huffman
add lemma DERIV_inverse_function
2007-05-20, by huffman
add lemmas LIM_compose2, isCont_LIM_compose2
2007-05-20, by huffman
improved aliassing
2007-05-19, by haftmann
more robust thm handling
2007-05-19, by haftmann
added a set of NNF normalization lemmas and nnf_conv
2007-05-19, by chaieb
added lt and some other infix operation analogous to Ocaml's num library
2007-05-19, by chaieb
added a generic conversion for quantifier elimination and a special useful instance
2007-05-19, by chaieb
added binop_conv, aconvc
2007-05-19, by chaieb
added cpat antiquotation for reading certified patterns
2007-05-19, by chaieb
unfold min/max in Stefans code generator
2007-05-19, by nipkow
added code generation based on Isabelle's rat type.
2007-05-19, by nipkow
Disabled Stefancs code generator - already enabled in RealDef.
2007-05-19, by nipkow
constant op @ now named append
2007-05-19, by haftmann
fixed comment
2007-05-19, by haftmann
dropped legacy
2007-05-19, by haftmann
improved eta expansion
2007-05-19, by haftmann
dropped nonsense comment
2007-05-19, by haftmann
fixed text
2007-05-19, by haftmann
eliminated name clash with List.append
2007-05-19, by haftmann
added qualification for ambiguous definition names
2007-05-19, by haftmann
tuned
2007-05-19, by haftmann
typ_of instance for int
2007-05-19, by haftmann
hide locale predicate "field" from HOL library
2007-05-19, by haftmann
no special treatment in naming of locale predicates stemming form classes
2007-05-19, by haftmann
uniform module names for code generation
2007-05-19, by haftmann
added Executable_Real
2007-05-19, by haftmann
updated
2007-05-19, by haftmann
Had to replace "case 1/2" by "case base/step". No idea why.
2007-05-19, by nipkow
*** empty log message ***
2007-05-19, by nipkow
remove dependence on Hilbert_Choice.thy
2007-05-19, by huffman
use THE instead of SOME
2007-05-19, by huffman
minimize imports
2007-05-18, by huffman
Prove existence of nth roots using Intermediate Value Theorem
2007-05-18, by huffman
avoid using real_mult_inverse_left; cleaned up
2007-05-18, by huffman
use mult_strict_mono instead of real_mult_less_mono
2007-05-18, by huffman
Fixed bug in subst causing primrec functions returning functions
2007-05-18, by berghofe
dropped word_setup.ML
2007-05-18, by haftmann
added files
2007-05-17, by krauss
updated
2007-05-17, by krauss
moved lemmas to Nat.thy
2007-05-17, by krauss
added induction principles for induction "backwards": P (Suc n) ==> P n
2007-05-17, by krauss
added pointer to new Unification theory
2007-05-17, by krauss
Added unification case study (using new function package)
2007-05-17, by krauss
avoid using redundant lemmas from RealDef.thy
2007-05-17, by huffman
canonical prefixing of class constants
2007-05-17, by haftmann
dropped beta/eta normalization of defining equations
2007-05-17, by haftmann
refined pow function
2007-05-17, by haftmann
abstract size function in hologic.ML
2007-05-17, by haftmann
tuned
2007-05-17, by haftmann
add classes ring_no_zero_divisors and dom
2007-05-17, by huffman
generalize class restrictions on some lemmas
2007-05-17, by huffman
added classes ring_no_zero_divisors and dom (non-commutative version of idom);
2007-05-17, by huffman
Added three items to the signature
2007-05-17, by paulson
generalize some lemmas from field to division_ring
2007-05-17, by huffman
instance division_ring < no_zero_divisors; clean up field instance proofs
2007-05-17, by huffman
remove redundant instance declaration
2007-05-17, by huffman
cleaned up proof of Maclaurin_sin_bound
2007-05-17, by huffman
section labels
2007-05-16, by huffman
minimize imports
2007-05-16, by huffman
dropped |R
2007-05-16, by chaieb
A verified theory for rational numbers representation and simple calculations;
2007-05-15, by chaieb
Fixed bug that caused proof of induction theorem to fail if
2007-05-15, by berghofe
minimize imports
2007-05-15, by huffman
clean up polar_Ex proofs; remove unnecessary lemmas
2007-05-15, by huffman
remove simp attribute from various polar_Ex lemmas
2007-05-15, by huffman
tuned proofs
2007-05-14, by huffman
spelling: rename arcos -> arccos
2007-05-14, by huffman
tuned proofs
2007-05-14, by huffman
add lemma sgn_mult; declare real_scaleR_def and scaleR_eq_0_iff as simp rules
2007-05-14, by huffman
generalized sgn function to work on any real normed vector space
2007-05-14, by huffman
root and sqrt on negative inputs
2007-05-14, by huffman
move lemmas to RealPow.thy; tuned proofs
2007-05-14, by huffman
tuned proofs
2007-05-14, by huffman
tuned
2007-05-14, by huffman
added general sum-squares lemmas
2007-05-14, by huffman
new lemmas
2007-05-14, by huffman
ProofGeneral: Find Theorems search form
2007-05-14, by webertj
reorganized float arithmetic
2007-05-14, by haftmann
fixed IntInf ambiguity
2007-05-14, by haftmann
remove redundant lemmas
2007-05-14, by huffman
remove redundant lemmas
2007-05-14, by huffman
remove redundant lemmas
2007-05-14, by huffman
remove redundant lemmas
2007-05-14, by huffman
cleaned up
2007-05-14, by huffman
tuned
2007-05-14, by huffman
define roots of negative reals so that many lemmas no longer require side conditions; simplification solves more goals than previously
2007-05-13, by huffman
add lemma power_eq_imp_eq_base
2007-05-13, by huffman
added module int
2007-05-13, by haftmann
dropped legacy
2007-05-13, by haftmann
removed module rat.ML
2007-05-13, by haftmann
whitespace tuned
2007-05-13, by haftmann
tuned
2007-05-13, by haftmann
fixed omission
2007-05-13, by haftmann
tuned setup
2007-05-13, by haftmann
refined module rat
2007-05-13, by haftmann
added modules rat.ML and int.ML
2007-05-13, by haftmann
Removed junk
2007-05-13, by nipkow
Got rid of listsp
2007-05-13, by nipkow
removed redundant lemmas
2007-05-13, by huffman
add lemma additive.setsum
2007-05-12, by huffman
*** empty log message ***
2007-05-11, by nipkow
*** empty log message ***
2007-05-11, by nipkow
proper type for fun/arg_cong_rule;
2007-05-11, by wenzelm
added fun/arg_cong_rule;
2007-05-11, by wenzelm
unified names: foo_conv;
2007-05-11, by wenzelm
tuned;
2007-05-11, by wenzelm
added fun flip f x y = f y x
2007-05-11, by krauss
generalize setsum lemmas from semiring_0_cancel to semiring_0
2007-05-11, by huffman
tuned proofs;
2007-05-11, by wenzelm
bang_facts: warning;
2007-05-11, by wenzelm
tuned proofs;
2007-05-11, by wenzelm
(class target)
2007-05-10, by haftmann
cleaned up
2007-05-10, by haftmann
beta/eta conversion after preprocessor
2007-05-10, by haftmann
fixed typo
2007-05-10, by haftmann
more conversions;
2007-05-10, by wenzelm
Moved extraction_expand declaration of listall_def outside of definition.
2007-05-10, by berghofe
Adapted to new naming scheme for definitions.
2007-05-10, by berghofe
Changed name of raw definition.
2007-05-10, by berghofe
Name of ML function "not" is now qualified in order to avoid
2007-05-10, by berghofe
consts in consts_code Isar commands are now referred to by usual term syntax
2007-05-10, by haftmann
size [nat] is identity
2007-05-10, by haftmann
explicit import of Datatype.thy due to hook bootstrap problem
2007-05-10, by haftmann
localized Sup/Inf
2007-05-10, by haftmann
localized Min/Max
2007-05-10, by haftmann
tuned
2007-05-10, by haftmann
fix proofs
2007-05-10, by huffman
remove redundant lemmas
2007-05-10, by huffman
lemmas iszero_(h)complex_number_of are no longer needed
2007-05-10, by huffman
instance real_algebra_1 < ring_char_0
2007-05-10, by huffman
new axclass ring_char_0 for rings with characteristic 0, used for of_int_eq_iff and related lemmas
2007-05-10, by huffman
moved conversions to structure Conv;
2007-05-10, by wenzelm
added dest_fun/fun2/arg1;
2007-05-10, by wenzelm
tuned argument_type_of;
2007-05-10, by wenzelm
added destructors from drule.ML;
2007-05-10, by wenzelm
moved some operations to more_thm.ML and conv.ML;
2007-05-10, by wenzelm
Conversions: primitive equality reasoning (from drule.ML);
2007-05-10, by wenzelm
added conv.ML;
2007-05-10, by wenzelm
Thm.match;
2007-05-10, by wenzelm
moved some Drule operations to Thm (see more_thm.ML);
2007-05-10, by wenzelm
Thm.first_order_match;
2007-05-10, by wenzelm
moved conversions to structure Conv;
2007-05-10, by wenzelm
"fun" command: Changed pattern compatibility proof back from "simp_all" to the slower but more robust "auto"
2007-05-09, by krauss
add lemma norm_diff_ineq; shorten other proofs
2007-05-09, by huffman
removed Complex/ComplexBin.thy;
2007-05-09, by wenzelm
tuned ML setup;
2007-05-09, by wenzelm
tuned syntax;
2007-05-09, by wenzelm
eliminated unnamed infixes;
2007-05-09, by wenzelm
removed unused mk_cond_defpair;
2007-05-09, by wenzelm
simp_depth: now proper value in simpset (prevents problems with lost exception trace, enables multi-threaded simplification);
2007-05-09, by wenzelm
remove empty, unused theory
2007-05-09, by huffman
remove redundant lemmas
2007-05-09, by huffman
add lemma hnorm_hyperpow
2007-05-09, by huffman
add lemma of_hypreal_hyperpow
2007-05-09, by huffman
tuned
2007-05-09, by haftmann
moved recfun_codegen.ML to Code_Generator.thy
2007-05-09, by haftmann
continued
2007-05-09, by haftmann
remove redundant lemmas
2007-05-09, by huffman
hcomplex_of_hypreal abbreviates of_hypreal; removed redundant lemmas
2007-05-09, by huffman
add lemma hnorm_divide
2007-05-09, by huffman
add lemmas abs_hnorm_cancel, hnorm_of_hypreal
2007-05-09, by huffman
add lemmas norm_add_less, norm_mult_less
2007-05-09, by huffman
add lemma Standard_hyperpow
2007-05-08, by huffman
tuned;
2007-05-08, by wenzelm
add of_hypreal constant with lemmas
2007-05-08, by huffman
add lemmas norm_number_of, norm_of_int, norm_of_nat
2007-05-08, by huffman
quoted 'declaration';
2007-05-08, by wenzelm
simplified pretty_thm(_legacy);
2007-05-08, by wenzelm
is_sid: include '::';
2007-05-08, by wenzelm
tuned ProofDisplay.pretty_full_theory;
2007-05-08, by wenzelm
tuned;
2007-05-08, by wenzelm
updated;
2007-05-08, by wenzelm
simplified context data;
2007-05-08, by wenzelm
tuned;
2007-05-08, by wenzelm
legacy_intern_skolem: legacy_feature;
2007-05-08, by wenzelm
tuned;
2007-05-08, by wenzelm
renamed call_atp to sledgehammer;
2007-05-08, by wenzelm
updated;
2007-05-08, by wenzelm
tuned context data;
2007-05-08, by wenzelm
ML adaptions
2007-05-08, by haftmann
clean up complex norm proofs, remove redundant lemmas
2007-05-08, by huffman
remove redundant lemmas
2007-05-08, by huffman
fix proof of hypreal_sqrt_sum_squares_ge1
2007-05-08, by huffman
add lemma real_sqrt_sum_squares_triangle_ineq
2007-05-08, by huffman
add lemma abs_norm_cancel
2007-05-08, by huffman
cleaned up
2007-05-08, by huffman
polished some proofs
2007-05-08, by urbanc
add lemmas power2_le_imp_le and power2_less_imp_less
2007-05-08, by huffman
add lemma power_less_imp_less_base
2007-05-08, by huffman
clean up RealVector classes
2007-05-07, by huffman
First-order variant of the fully-typed translation
2007-05-07, by paulson
added further equality example
2007-05-07, by haftmann
changed 'code nofunc' to 'code func del'
2007-05-07, by haftmann
* Context data interfaces;
2007-05-07, by wenzelm
simplified DataFun interfaces: removed name/print, use adhoc value for uninitialized data, init only required for impure data;
2007-05-07, by wenzelm
simplified DataFun interfaces;
2007-05-07, by wenzelm
changed code generator invocation syntax
2007-05-06, by haftmann
PreList imports RecDef
2007-05-06, by haftmann
dropped legacy ML binding
2007-05-06, by haftmann
added auxiliary lemmas for proof tools
2007-05-06, by haftmann
dropped preorders, unified syntax
2007-05-06, by haftmann
minimal import
2007-05-06, by haftmann
dropped HOL.ML
2007-05-06, by haftmann
tuned
2007-05-06, by haftmann
updated Alice version;
2007-05-06, by wenzelm
IntInf.fromInt;
2007-05-06, by wenzelm
added "set" supression
2007-05-06, by nipkow
added test about "set" supression
2007-05-06, by nipkow
polished all proofs and made the theory "self-contained"
2007-05-04, by urbanc
deleted some unnecessary type-annotations
2007-05-03, by urbanc
tuned some of the proofs and added the lemma fresh_bool
2007-05-03, by urbanc
tuned allpairs
2007-05-02, by nipkow
tuned some proofs and changed variable names in some definitions of Nominal.thy
2007-05-02, by urbanc
added allpairs
2007-04-30, by nipkow
removed obsolete get_sg;
2007-04-30, by wenzelm
explicit treatment of legacy_features;
2007-04-30, by wenzelm
Fixing bugs in the partial-typed and fully-typed translations
2007-04-30, by paulson
Removal of dead code
2007-04-30, by paulson
tuned some proofs in CR and properly included CR_Takahashi
2007-04-27, by urbanc
removed obsolete induct/simp tactic;
2007-04-27, by wenzelm
alternative and much simpler proof for Church-Rosser of Beta-Reduction
2007-04-27, by urbanc
use correct email program for sunbroy2
2007-04-27, by kleing
removed legacy ML files;
2007-04-26, by wenzelm
eliminated unnamed infixes;
2007-04-26, by wenzelm
added header;
2007-04-26, by wenzelm
added header;
2007-04-26, by wenzelm
added
2007-04-26, by haftmann
removed lagacy ML files;
2007-04-26, by wenzelm
updated;
2007-04-26, by wenzelm
eliminated unnamed infixes;
2007-04-26, by wenzelm
renamed some old names Theory.xxx to Sign.xxx;
2007-04-26, by wenzelm
eliminated unnamed infixes;
2007-04-26, by wenzelm
added header;
2007-04-26, by wenzelm
eliminated unnamed infixes, tuned syntax;
2007-04-26, by wenzelm
clarified naming policy
2007-04-26, by haftmann
clarified semantics of merge
2007-04-26, by haftmann
moved stuff to Char_nat.thy
2007-04-26, by haftmann
tuned
2007-04-26, by haftmann
slightly tuned
2007-04-26, by haftmann
replaced recdef by function
2007-04-26, by haftmann
cleaned up code generator setup for int
2007-04-26, by haftmann
added lemmatas
2007-04-26, by haftmann
moved code generation pretty integers and characters to separate theories
2007-04-26, by haftmann
updated doc
2007-04-26, by haftmann
mk_const_def: Sign.intern_term (legacy);
2007-04-26, by wenzelm
renamed some old names Theory.xxx to Sign.xxx;
2007-04-26, by wenzelm
updated;
2007-04-26, by wenzelm
add the lemma supp_eqvt and put the right attribute
2007-04-25, by narboux
new lemma splice_length
2007-04-25, by nipkow
fix sml compilation
2007-04-25, by narboux
Moved function params_of to inductive_package.ML.
2007-04-25, by berghofe
Moved functions infer_intro_vars, arities_of, params_of, and
2007-04-25, by berghofe
Added functions arities_of, params_of, partition_rules, and
2007-04-25, by berghofe
eqvt_tac now instantiates introduction rules before applying them.
2007-04-25, by berghofe
update fresh_fun_simp for debugging purposes
2007-04-24, by narboux
fixes last commit
2007-04-24, by narboux
add two lemmas dealing with freshness on permutations.
2007-04-24, by narboux
Added datatype_case.ML and nominal_fresh_fun.ML.
2007-04-24, by berghofe
Added datatype_case.
2007-04-24, by berghofe
Added intro / elim rules for prod_case.
2007-04-24, by berghofe
sum_case is now authentic.
2007-04-24, by berghofe
Adapted to new parse translation for case expressions.
2007-04-24, by berghofe
Parse / print translations for nested case expressions, taken
2007-04-24, by berghofe
Streamlined datatype_codegen function using new datatype_of_case
2007-04-24, by berghofe
- Moved parse / print translations for case to datatype_case.ML
2007-04-24, by berghofe
case constants are now authentic.
2007-04-24, by berghofe
oups : wrong commit
2007-04-24, by narboux
adds op in front of an infix to fix SML compilation
2007-04-24, by narboux
sane version of read_termTs (proper freeze);
2007-04-23, by wenzelm
read_instantiations: proper type-inference with fixed variables, infer parameter types as well;
2007-04-23, by wenzelm
added paramify_vars;
2007-04-23, by wenzelm
def_simproc(_i): proper ProofContext.read/cert_terms;
2007-04-23, by wenzelm
simplified ProofContext.read_termTs;
2007-04-23, by wenzelm
simplified the proof of pt_set_eqvt (as suggested by Randy Pollack)
2007-04-23, by urbanc
initial commit
2007-04-23, by haftmann
faster proof of wf_eq_minimal
2007-04-21, by huffman
export get_sort (belongs to Syntax module);
2007-04-21, by wenzelm
TypeExt.decode_term;
2007-04-21, by wenzelm
added decode_term (belongs to Syntax module);
2007-04-21, by wenzelm
tuned the setup of fresh_fun
2007-04-21, by urbanc
defs are added to code data
2007-04-20, by haftmann
repaired value restriction problem
2007-04-20, by haftmann
reverted to classical syntax for K_record
2007-04-20, by haftmann
tuned
2007-04-20, by haftmann
Interpretation equations applied to attributes
2007-04-20, by ballarin
Interpretation equations applied to attributes;
2007-04-20, by ballarin
Modified eqvt_tac to avoid failure due to introduction rules
2007-04-20, by berghofe
clarifed
2007-04-20, by haftmann
modify fresh_fun_simp to ease debugging
2007-04-20, by narboux
updated code generator
2007-04-20, by haftmann
updated
2007-04-20, by haftmann
adds extracted program to code theorem table
2007-04-20, by haftmann
unfold attribute now also accepts HOL equations
2007-04-20, by haftmann
added more stuff
2007-04-20, by haftmann
add definitions explicitly to code generator table
2007-04-20, by haftmann
cleared dead code
2007-04-20, by haftmann
moved axclass module closer to core system
2007-04-20, by haftmann
Isar definitions are now added explicitly to code theorem table
2007-04-20, by haftmann
improved case unfolding
2007-04-20, by haftmann
switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
2007-04-20, by haftmann
tuned syntax: K_record is now an authentic constant
2007-04-20, by haftmann
tuned: now using function package
2007-04-20, by haftmann
transfer_tac accepts also HOL equations as theorems
2007-04-20, by haftmann
shifted min/max to class order
2007-04-20, by haftmann
tuned
2007-04-20, by haftmann
added class tutorial
2007-04-20, by haftmann
code generator changes
2007-04-20, by haftmann
generate page labels
2007-04-20, by krauss
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
2007-04-20, by krauss
declared lemmas true_eqvt and false_eqvt to be equivariant (suggested by samth at ccs.neu.edu)
2007-04-20, by urbanc
trying to make single-step proofs work better, especially if they contain
2007-04-19, by paulson
nominal_inductive no longer proves equivariance.
2007-04-19, by berghofe
add a tactic to generate fresh names
2007-04-19, by narboux
simplified ProofContext.infer_types(_pats);
2007-04-18, by wenzelm
Improved comments.
2007-04-18, by dixon
proper header, added regression tests
2007-04-18, by krauss
added temporary hack to avoid schematic goals in "termination".
2007-04-18, by krauss
Fixes for proof reconstruction, especially involving abstractions and definitions
2007-04-18, by paulson
export is_dummy_pattern;
2007-04-17, by wenzelm
lemma isCont_inv_fun is same as isCont_inverse_function
2007-04-17, by huffman
moved root and sqrt lemmas from Transcendental.thy to NthRoot.thy
2007-04-17, by huffman
remove use of pos_boundedE
2007-04-17, by huffman
lemma geometric_sum no longer needs class division_by_zero
2007-04-17, by huffman
tuned proofs;
2007-04-17, by wenzelm
canonical merge operations
2007-04-16, by haftmann
added print_indexname;
2007-04-16, by wenzelm
improved the equivariance lemmas for the quantifiers; had to export the lemma eqvt_force_add and eqvt_force_del in the thmdecls
2007-04-16, by urbanc
added a more usuable lemma for dealing with fresh_fun
2007-04-16, by urbanc
generalized type of lemma geometric_sum
2007-04-16, by huffman
replaced read_term_legacy by read_prop_legacy;
2007-04-15, by wenzelm
removed obsolete redeclare_skolems;
2007-04-15, by wenzelm
read prop as prop, not term;
2007-04-15, by wenzelm
removed obsolete TypeInfer.logicT -- use dummyT;
2007-04-15, by wenzelm
avoid internal names;
2007-04-15, by wenzelm
tuned;
2007-04-15, by wenzelm
legacy_infer_term/prop -- including intern_term;
2007-04-15, by wenzelm
Thm.plain_prop_of;
2007-04-15, by wenzelm
added decode_types (from type_infer.ML);
2007-04-15, by wenzelm
added read_term;
2007-04-15, by wenzelm
added mixfixT (from type_infer.ML);
2007-04-15, by wenzelm
proper interface infer_types(_pat);
2007-04-15, by wenzelm
Thm.fold_terms;
2007-04-15, by wenzelm
removed unused Output.panic hook -- internal to PG wrapper;
2007-04-15, by wenzelm
moved get_sort to sign.ML;
2007-04-15, by wenzelm
removed obsolete inferT_axm;
2007-04-15, by wenzelm
removed obsolete infer_types(_simult);
2007-04-15, by wenzelm
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
2007-04-15, by wenzelm
load type_infer.ML early;
2007-04-15, by wenzelm
adapted decode_type;
2007-04-15, by wenzelm
proper ProofContext.infer_types;
2007-04-15, by wenzelm
Thm.fold_terms;
2007-04-15, by wenzelm
replaced axioms/finalconsts by proper axiomatization;
2007-04-15, by wenzelm
simplified read_axm;
2007-04-14, by wenzelm
tuned comment;
2007-04-14, by wenzelm
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
2007-04-14, by wenzelm
removed redundant string_of_vname (see term.ML);
2007-04-14, by wenzelm
removed obsolete read_ctyp, read_def_cterm;
2007-04-14, by wenzelm
tuned signature;
2007-04-14, by wenzelm
read_typ_XXX: no sorts;
2007-04-14, by wenzelm
added read_def_cterms, read_cterm (from thm.ML);
2007-04-14, by wenzelm
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
2007-04-14, by wenzelm
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
2007-04-14, by wenzelm
removed Pure/Syntax/ROOT.ML;
2007-04-14, by wenzelm
Term.string_of_vname;
2007-04-14, by wenzelm
Theory.inferT_axm;
2007-04-14, by wenzelm
do not enable Toplevel.debug globally;
2007-04-14, by wenzelm
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
2007-04-14, by wenzelm
canonical merge operations
2007-04-14, by haftmann
declarations: apply target_morphism;
2007-04-14, by wenzelm
inst(T)_morphism: avoid reference to static theory value;
2007-04-14, by wenzelm
tuned signature;
2007-04-14, by wenzelm
added Morphism.transform/form (generic non-sense);
2007-04-14, by wenzelm
Morphism.transform/form;
2007-04-14, by wenzelm
data declaration: removed obsolete target_morphism (still required for local data!?);
2007-04-14, by wenzelm
data declaration: removed obsolete target_morphism;
2007-04-14, by wenzelm
added eval_antiquotes_fn (tmp);
2007-04-13, by wenzelm
tuned document (headers, sections, spacing);
2007-04-13, by wenzelm
do translation: CONST;
2007-04-13, by wenzelm
eval_antiquotes: proper parentheses for projection;
2007-04-13, by wenzelm
canonical merge operations
2007-04-13, by haftmann
Removed erroneous application of rev in get_clauses that caused
2007-04-13, by berghofe
more robust proof
2007-04-13, by krauss
Experimental code for the interpretation of definitions.
2007-04-13, by ballarin
Experimental interpretation code for definitions.
2007-04-13, by ballarin
New file for locale regression tests.
2007-04-13, by ballarin
debug versions of finite_guess and fresh_guess do not fail if they can not solve the goal
2007-04-13, by narboux
minimize imports
2007-04-13, by huffman
new simp rule exp_ln; new standard proof of DERIV_exp_ln_one; changed imports
2007-04-13, by huffman
moved nonstandard derivative stuff from Deriv.thy into new file HDeriv.thy
2007-04-13, by huffman
added proj_value_antiq;
2007-04-12, by wenzelm
absdummy: use internal name uu to avoid renaming of popular names;
2007-04-12, by wenzelm
tuned the proof of lemma pt_list_set_fresh (as suggested by Randy Pollack) and tuned the syntax for sub_contexts
2007-04-12, by urbanc
updated;
2007-04-12, by wenzelm
output_basic: added isaantiq markup (only inside verbatim tokens);
2007-04-12, by wenzelm
newenvironment{isaantiq};
2007-04-12, by wenzelm
Zero variable indexes in clauses
2007-04-12, by paulson
Improved treatment of classrel/arity clauses
2007-04-12, by paulson
Fixed the treatment of TVars in conjecture clauses (they are deleted, not frozen)
2007-04-12, by paulson
Improved and simplified the treatment of classrel/arity clauses
2007-04-12, by paulson
canonical merge operations
2007-04-12, by haftmann
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
2007-04-12, by huffman
run annomaly from makedist
2007-04-12, by kleing
set special ISABELLE_USER_HOME as in other isatest settings
2007-04-12, by isatest
isatest version of annomaly script. to be run from istatest-makedist.
2007-04-12, by kleing
new standard proof of lemma LIM_inverse
2007-04-12, by huffman
new class syntax for scaleR and norm classes
2007-04-11, by huffman
removed debugging code
2007-04-11, by krauss
canonical merge operations
2007-04-11, by haftmann
tuned
2007-04-11, by haftmann
dropped legacy ML bindings
2007-04-11, by haftmann
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
2007-04-11, by huffman
move lemma real_of_nat_inverse_le_iff from NSA.thy to NthRoot.thy
2007-04-11, by huffman
new standard proof of convergent = Cauchy
2007-04-11, by huffman
new standard proof of LIMSEQ_realpow_zero
2007-04-10, by huffman
new LIM/isCont lemmas for abs, of_real, and power
2007-04-10, by huffman
some restructuring
2007-04-10, by krauss
interpretation bounded_linear_of_real
2007-04-10, by huffman
removed unnecessary premise from power_le_imp_le_base
2007-04-10, by huffman
proper handling of morphisms
2007-04-10, by krauss
Moving "FunDef" up in the HOL development graph, since it is independent from "Recdef" and "Datatype" now.
2007-04-10, by krauss
inline_antiq: no longer forces ML_Syntax.atomic;
2007-04-10, by wenzelm
removed dead code
2007-04-10, by krauss
tuned
2007-04-10, by krauss
added example for definitions in local contexts
2007-04-10, by krauss
removed obsolete workaround
2007-04-10, by krauss
generalized type of lemma setsum_product
2007-04-09, by huffman
new standard proofs of some LIMSEQ lemmas
2007-04-09, by huffman
rearranged sections
2007-04-08, by huffman
remove redundant lemmas
2007-04-08, by huffman
removed obsolete workarounds
2007-04-07, by krauss
deleted remaining instances of swap_simp_a and swap_simp_b (obsolete now)
2007-04-07, by urbanc
tuned slightly the previous commit
2007-04-07, by urbanc
perm_simp can now simplify using the rules (a,b) o a = b and (a,b) o b = a
2007-04-07, by narboux
add new standard proofs for limits of sequences
2007-04-06, by huffman
Replaced add_inductive_i by add_inductive_global.
2007-04-05, by berghofe
- Tried to make name_of_thm more robust against changes of the
2007-04-05, by berghofe
- Removed occurrences of ProofContext.export in add_ind_def that
2007-04-05, by berghofe
thy_deps: sort Context.thy_ord;
2007-04-05, by wenzelm
added thy_ord -- order of creation;
2007-04-05, by wenzelm
simplified thy_deps using Theory.ancestors_of (in order of creation);
2007-04-04, by wenzelm
renamed Variable.importT to importT_thms;
2007-04-04, by wenzelm
removed unused dep_graph;
2007-04-04, by wenzelm
theory: maintain ancestors in order of creation;
2007-04-04, by wenzelm
rep_thm/cterm/ctyp: removed obsolete sign field;
2007-04-04, by wenzelm
rebind HOL.refl as refl (hidden by widen.refl);
2007-04-04, by wenzelm
rep_thm/cterm/ctyp: removed obsolete sign field;
2007-04-04, by wenzelm
make fresh_guess fail if it does not solve the subgoal
2007-04-04, by narboux
add a few details in the Fst and Snd cases of unicity proof
2007-04-04, by narboux
find_first is just an alias
2007-04-04, by paulson
added print_mode (generic non-sense);
2007-04-04, by wenzelm
improved exception CTERM;
2007-04-04, by wenzelm
removed unused info channel;
2007-04-04, by wenzelm
added print_mode;
2007-04-04, by wenzelm
removed unused info channel;
2007-04-04, by wenzelm
renamed Output.has_mode to print_mode_active;
2007-04-04, by wenzelm
tuned comment;
2007-04-04, by wenzelm
cleaned-up Output functions;
2007-04-04, by wenzelm
improved exception CTERM;
2007-04-04, by wenzelm
added scanwords from library.ML (for obsolete rename_tac);
2007-04-04, by wenzelm
removed obsolete scanwords (see obsolete tactic.ML:rename_tac for its only use);
2007-04-04, by wenzelm
removed dead code;
2007-04-04, by wenzelm
cleaned-up Output functions;
2007-04-04, by wenzelm
eliminated obsolete rename_tac;
2007-04-04, by wenzelm
removed obsolete sign_of/sign_of_thm;
2007-04-04, by wenzelm
ML antiquotes;
2007-04-04, by wenzelm
tuned comments;
2007-04-03, by wenzelm
fixed chr/explode;
2007-04-03, by wenzelm
avoid overloaded integer constants (accomodate Alice);
2007-04-03, by wenzelm
avoid clash with Alice keywords;
2007-04-03, by wenzelm
signature: eqtype to accomodate Alice;
2007-04-03, by wenzelm
renamed comp to compose (avoid clash with Alice keywords);
2007-04-03, by wenzelm
renamed of_sort_derivation record fields (avoid clash with Alice keywords);
2007-04-03, by wenzelm
added ML-Systems/alice.ML;
2007-04-03, by wenzelm
renamed Variable.import to import_thms (avoid clash with Alice keywords);
2007-04-03, by wenzelm
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
2007-04-03, by wenzelm
ranamed CodegenData.lazy to lazy_thms (avoid clash with Alice keywords);
2007-04-03, by wenzelm
remove the lemma swap_fun which was not needed
2007-04-03, by narboux
slighltly improved the proof of unicity
2007-04-03, by narboux
Compatibility file for Alice 1.3 -- experimental!
2007-04-03, by wenzelm
rename bij and fresh into bijs and freshs and lookup for eqvts lemma using the ml value instead of the name
2007-04-02, by narboux
optimizing the null instantiation case
2007-04-02, by paulson
now exports distinct_subgoal_tac (needed by MetisAPI)
2007-04-02, by paulson
exception handling
2007-04-02, by paulson
added reserved words mod, div for SML
2007-04-01, by haftmann
added pt_bij' to the collection perm_swap and also added abs_perm to the collection of equivariance lemmas
2007-03-31, by urbanc
Fixed bug in dest_prem: premises of the form "p x_1 ... x_n"
2007-03-31, by berghofe
fixed typo
2007-03-31, by haftmann
simplified constant representation in code generator
2007-03-30, by haftmann
tuned
2007-03-30, by haftmann
equality on strings
2007-03-30, by haftmann
paraphrasing equality
2007-03-30, by haftmann
updated
2007-03-30, by haftmann
improved character output for SML
2007-03-29, by haftmann
dropped legacy ML bindings
2007-03-29, by haftmann
simplified some steps
2007-03-29, by paulson
MESON tactical takes an additional argument: the clausification function.
2007-03-29, by paulson
Now checks for types-only clause before outputting.
2007-03-29, by paulson
- Improved error messages in equivariance proof
2007-03-28, by berghofe
Renamed induct(s)_weak to weak_induct(s) in order to unify
2007-03-28, by berghofe
- Renamed <predicate>_eqvt to <predicate>.eqvt
2007-03-28, by berghofe
the name for the collection of equivariance lemmas is now eqvts (changed from eqvt) in order to avoid clashes with eqvt-lemmas generated in nominal_inductive
2007-03-28, by urbanc
adapted to new nominal_inductive
2007-03-28, by urbanc
Improved code generator for characters: now handles
2007-03-28, by berghofe
tuned proofs (taking full advantage of nominal_inductive)
2007-03-28, by urbanc
adapted to nominal_inductive infrastructure
2007-03-28, by urbanc
made the type sets instance of the "cp" type-class
2007-03-28, by urbanc
added extended the lemma for equivariance of freshness
2007-03-27, by urbanc
adapted to nominal_inductive
2007-03-27, by urbanc
adapted to new nominal_inductive infrastructure
2007-03-27, by urbanc
Adapted to new syntax of nominal_inductive.
2007-03-27, by berghofe
Adapted to changes in nominal_inductive.
2007-03-27, by berghofe
Implemented proof of strong induction rule.
2007-03-27, by berghofe
Exported perm_of_pair, mk_not_sym, and perm_simproc.
2007-03-27, by berghofe
cleaned up HOL/ex/Code*.thy
2007-03-27, by haftmann
fixed document preparation
2007-03-27, by haftmann
fixed problem with mutual recursion
2007-03-26, by krauss
cleaned up Library/ and ex/
2007-03-26, by haftmann
minimal intro rules
2007-03-26, by haftmann
exported interface for intro rules
2007-03-26, by haftmann
moved Eval theory to library
2007-03-26, by haftmann
Eval theory
2007-03-26, by haftmann
tuned
2007-03-26, by haftmann
importing Eval theory
2007-03-26, by haftmann
naming tuned
2007-03-26, by haftmann
cleaned up Library( and ex/
2007-03-26, by haftmann
Clause cache is now in theory data.
2007-03-26, by paulson
"generalize" now replaces ugly mes_XXX generated symbols by 1-letter identifiers.
2007-03-26, by paulson
moving lemmas into appropriate sections
2007-03-25, by urbanc
fixed typing bug in generated code
2007-03-23, by haftmann
fixed typing bug in generated code
2007-03-23, by haftmann
added the permutation operation on options to the list of equivariance lemmas
2007-03-23, by urbanc
dropped
2007-03-23, by haftmann
added empty cases
2007-03-23, by haftmann
added concept for term constructors
2007-03-23, by haftmann
tuned
2007-03-23, by haftmann
two further properties about lists
2007-03-23, by haftmann
removed outdated example
2007-03-23, by haftmann
fixed typo
2007-03-23, by haftmann
added some sketches about library functions
2007-03-23, by haftmann
fixed function syntax
2007-03-22, by krauss
fixed function syntax
2007-03-22, by krauss
corrected the lemmas min_nat_eqvt and min_int_eqvt
2007-03-22, by urbanc
fixed code generator setup
2007-03-22, by haftmann
made function syntax strict, requiring | to separate equations; cleanup
2007-03-22, by krauss
fixed problem with the construction of mutual simp rules
2007-03-22, by krauss
cleanup
2007-03-22, by krauss
clarified an error-message
2007-03-22, by urbanc
tuned some proofs
2007-03-22, by urbanc
added another rule for simultaneous induction, and lemmas for zip
2007-03-21, by krauss
Unified function syntax
2007-03-21, by krauss
Numerous bug fixes. Type clauses distinguished from empty clauses. Working proof reduction.
2007-03-21, by paulson
added example file
2007-03-21, by haftmann
Better documentation path rewriting for src dir, used in tarball build.
2007-03-20, by gagern
Changed AnnoMaLy build process from CVS to tarball sources.
2007-03-20, by gagern
simplified "eval" oracle method
2007-03-20, by krauss
updated keywords
2007-03-20, by haftmann
added theory dependency graph
2007-03-20, by haftmann
improved treatment of defining equations stemming from specification tools
2007-03-20, by haftmann
added instance for lattice
2007-03-20, by haftmann
dropped OrderedGroup.ML
2007-03-20, by haftmann
added class "default" and expansion axioms for undefined
2007-03-20, by haftmann
switched exception from arbitrary to undefined
2007-03-20, by haftmann
updated code generation sections
2007-03-20, by haftmann
fixed typo
2007-03-20, by haftmann
new lemmas
2007-03-20, by haftmann
pretty function arrow for diag serializer
2007-03-20, by haftmann
adjusted definition of defining equation
2007-03-20, by haftmann
fixed slip
2007-03-20, by haftmann
explizit "type" superclass
2007-03-20, by haftmann
tuned the proof
2007-03-19, by urbanc
Removal of axiom names from the theorem cache
2007-03-19, by paulson
No label on "show"; tries to remove dependencies more cleanly
2007-03-19, by paulson
dropped overwrite_warn
2007-03-19, by haftmann
moved Output.overwrite_warn here
2007-03-19, by haftmann
TrueElim and notTrueElim tested and added as safe elim rules.
2007-03-18, by dixon
dropped LOrder.thy in favor of Lattices.thy
2007-03-16, by haftmann
dropped LOrder.thy
2007-03-16, by haftmann
added "satisfies" interface
2007-03-16, by haftmann
dropping dead code
2007-03-16, by haftmann
clarified check of defining equations
2007-03-16, by haftmann
adjusted qualified thm reference
2007-03-16, by haftmann
inf_fun_eq and inf_bool_eq now with meta equality
2007-03-16, by haftmann
added "class"es
2007-03-16, by haftmann
tuned
2007-03-16, by haftmann
dropped superfluous hide
2007-03-16, by haftmann
added lattice definitions
2007-03-16, by haftmann
added instance of sets as distributive lattices
2007-03-16, by haftmann
integrated with LOrder.thy
2007-03-16, by haftmann
moved lattice instance here
2007-03-16, by haftmann
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
2007-03-16, by haftmann
added FIXME hints
2007-03-16, by haftmann
lattice cleanup
2007-03-16, by haftmann
updated
2007-03-16, by haftmann
adjusted for the example file SOS.thy
2007-03-16, by urbanc
added formalisations of typical SOS-proofs
2007-03-16, by urbanc
added eqvt-lemmas for integers and eqvt-tagged the lemma append_eqvt
2007-03-16, by urbanc
removed safe elim flag of trueElim and notFalseElim for testing.
2007-03-16, by dixon
added safe intro rules for removing "True" subgoals as well as "~ False" ones.
2007-03-16, by dixon
move sqrt_divide_self_eq to NthRoot.thy
2007-03-14, by huffman
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
2007-03-14, by huffman
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
2007-03-14, by webertj
deleted function for defining candidates and used nominal_primrec instead
2007-03-13, by urbanc
syntax: proper body priorty for derived binders;
2007-03-12, by wenzelm
tuned;
2007-03-12, by wenzelm
removes some unused code that used to try to derive a simpler version of the eqvt lemmas
2007-03-12, by narboux
Adapted to new inductive definition package.
2007-03-12, by berghofe
clarified code
2007-03-11, by haftmann
- Replaced fold by fold_rev to make sure that list of predicate
2007-03-10, by berghofe
- Changed format of descriptor contained in nominal_datatype_info
2007-03-10, by berghofe
Renamed INF to INFM to avoid clash with INF operator defined in FixedPoint theory.
2007-03-10, by berghofe
Adapted to changes in definition of SUP.
2007-03-10, by berghofe
Generalized version of SUP and INF (with index set).
2007-03-10, by berghofe
Eta-expanded codetype_hook to make SML/NJ happy.
2007-03-10, by berghofe
First stab at reconstructing HO problems
2007-03-09, by paulson
constant names now dependent on executable content
2007-03-09, by haftmann
resolved name clashes
2007-03-09, by haftmann
moved order on functions here
2007-03-09, by haftmann
*** empty log message ***
2007-03-09, by haftmann
dropped code datatype certificates
2007-03-09, by haftmann
stepping towards uniform lattice theory development in HOL
2007-03-09, by haftmann
correct typo in latex output
2007-03-06, by narboux
updated this file to the new infrastructure
2007-03-06, by urbanc
fixed function package bug in the handling of multiple guards
2007-03-06, by krauss
major update of the nominal package; there is now an infrastructure
2007-03-06, by urbanc
fix wrong default for find_theorems
2007-03-06, by kleing
document find_theorems syntax change
2007-03-06, by kleing
find_theorems: moved with_dup into the brackets, i.e.
2007-03-06, by kleing
an O(n log n) version of removing duplicates
2007-03-06, by kleing
clean up var/running dir before spawning new tests
2007-03-05, by kleing
additional settings for isatest runs on various platforms
2007-03-05, by kleing
adjust paths
2007-03-05, by kleing
moved all isatest/cron job related files to own directory
2007-03-05, by kleing
AnnoMaLy related files, as discussed in mails with Gerwin Klein
2007-03-05, by gagern
Simplify print mode. Support setproverflag.
2007-03-03, by aspinall
Update test for new parse result
2007-03-03, by aspinall
Add setproverflag, to replace other flag controls
2007-03-03, by aspinall
Add objtypes to openblock/closeblock and theory items (can be used to control folding).
2007-03-03, by aspinall
Add more attributes to openblock. Change theory item objtype field to proper objtype.
2007-03-03, by aspinall
Add Isabelle-specific objtypes
2007-03-03, by aspinall
Comment
2007-03-03, by aspinall
clarified code
2007-03-03, by haftmann
clarified error message
2007-03-03, by haftmann
moved instance option :: finite to Finite_Set.thy
2007-03-03, by haftmann
moved instance option :: finite here
2007-03-03, by haftmann
Fix idvalue output and PGML print mode raw encode/decode.
2007-03-03, by aspinall
permitting empty datatypes
2007-03-02, by haftmann
improved handling of nat numerals
2007-03-02, by haftmann
tuned code theorems for ord on integers
2007-03-02, by haftmann
simplified code generator setup
2007-03-02, by haftmann
tuned code theorems
2007-03-02, by haftmann
added add_numerals_of
2007-03-02, by haftmann
now using "class"
2007-03-02, by haftmann
using "fst" "snd" for Haskell code
2007-03-02, by haftmann
added code theorems for UNIV
2007-03-02, by haftmann
adjusted to latest changes
2007-03-02, by haftmann
new code theorems
2007-03-02, by haftmann
syntax for "class attach const"
2007-03-02, by haftmann
prefix of class interpretation not mandatory any longer
2007-03-02, by haftmann
Meson.is_fol_term now takes a theory as argument. Minor tidying.
2007-03-02, by paulson
New code to store theorem names in a concise form rather than as fully-qualified.
2007-03-02, by paulson
The first-order test now tests for the obscure case of a polymorphic constant like 1 being
2007-03-02, by paulson
abbrev: be permissive after transformation;
2007-02-28, by wenzelm
exported get_ss, map_ss;
2007-02-28, by wenzelm
tuned;
2007-02-28, by wenzelm
tuned ML setup;
2007-02-28, by wenzelm
added @{const_name}, @{const_syntax};
2007-02-28, by wenzelm
more cleanup
2007-02-28, by krauss
Add closeblock/openblock structure to proof-block commands
2007-02-28, by aspinall
Updated success string for Vampire.
2007-02-28, by paulson
Now outputs metis calls
2007-02-28, by paulson
added headers
2007-02-28, by krauss
cleanup, fixing sml/nj related problems
2007-02-28, by krauss
gensym: removed bits of dead code;
2007-02-28, by wenzelm
gensym no longer includes ' or _ in names (trailing _ is bad)
2007-02-27, by paulson
tuned document;
2007-02-27, by wenzelm
\usepackage{amssymb};
2007-02-27, by wenzelm
moved some non-kernel material to more_thm.ML;
2007-02-26, by wenzelm
removed obsolete eq_set;
2007-02-26, by wenzelm
Thm.internalK;
2007-02-26, by wenzelm
Further operations on type thm, outside the inference kernel.
2007-02-26, by wenzelm
added more_thm.ML;
2007-02-26, by wenzelm
moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
2007-02-26, by wenzelm
Added formalization of size-change principle (experimental).
2007-02-26, by krauss
added theorems_of;
2007-02-26, by wenzelm
removed obsolete theorem_space;
2007-02-26, by wenzelm
Added lemma lfp_const: "lfp (%x. t) = t
2007-02-26, by krauss
exported serializer parsers
2007-02-23, by haftmann
proper treatment of -> as type constructor
2007-02-23, by haftmann
tuned
2007-02-23, by haftmann
add_path for naming in proof contexts
2007-02-23, by haftmann
locale: add_locale accepts explicit predicate name, interpretation supports non-mandatory prefixes
2007-02-23, by haftmann
slightly tuned
2007-02-23, by haftmann
slight cleanup
2007-02-23, by haftmann
adjusted code lemmas
2007-02-23, by haftmann
continued
2007-02-23, by haftmann
dropped diagnostic switch
2007-02-23, by haftmann
Improved handling of situation when theorem in cache disagrees with theorem supplied: new clauses
2007-02-22, by paulson
Fixed print translations for quantifiers a la "ALL x>=t. P x". These used
2007-02-21, by krauss
prevent quadratic time removal of duplicates if filter list is empty (likely to have too many results)
2007-02-21, by kleing
added missing \
2007-02-20, by kleing
updated docs with new with_dups syntax for find_theorems
2007-02-20, by kleing
Remove duplicates from printed theorems in find_theorems
2007-02-20, by kleing
more precise error message in parameter unification
2007-02-19, by schirmer
Updated
2007-02-17, by aspinall
Fix <pgipquit>. Remove unused pgmlatomsN. Make showid match askids. Use string functions for showid, avoiding printwrap kludge.
2007-02-17, by aspinall
<idvalue>: add name attribute to allow unsolicited updates.
2007-02-17, by aspinall
pretty_full_theory: expose in signature.
2007-02-17, by aspinall
Clarify comment
2007-02-17, by aspinall
unified arity parser/arguments;
2007-02-16, by wenzelm
ML text: informative Output.debug only;
2007-02-16, by wenzelm
unified arity parser/arguments;
2007-02-16, by wenzelm
Replaced "raise RecError" by "primrec_err" in function
2007-02-16, by berghofe
added example for print-mode Axiom
2007-02-16, by schirmer
added print-mode Axiom to print theorems without premises with a rule on top.
2007-02-16, by schirmer
updated Makefile
2007-02-16, by krauss
start adding the attribute eqvt to some lemmas of the nominal library
2007-02-15, by narboux
changed termination goal to use object quantifier
2007-02-15, by krauss
added congruence rule for function composition
2007-02-15, by krauss
beta_eta_contract specification befor processing. These normal forms avoid unpleasant surprises later on.
2007-02-15, by krauss
continued
2007-02-14, by haftmann
class package now using Locale.interpretation_i
2007-02-14, by haftmann
clarified explanation
2007-02-14, by haftmann
cleanup
2007-02-14, by haftmann
simpliefied instance statement
2007-02-14, by haftmann
continued class tutorial
2007-02-14, by haftmann
added class "preorder"
2007-02-14, by haftmann
Added nominal_inductive keyword.
2007-02-13, by berghofe
Added new file Nominal/nominal_inductive.ML
2007-02-13, by berghofe
First steps towards strengthening of induction rules for
2007-02-13, by berghofe
Added new file nominal_inductive.ML
2007-02-13, by berghofe
Curried and exported mk_perm.
2007-02-13, by berghofe
COMP now performs a distinctness check on the multiple results before failing
2007-02-13, by paulson
improved lexicographic order termination tactic
2007-02-13, by bulwahn
added OCaml example
2007-02-10, by haftmann
Completing the bug fix from the previous update: the result of unifying type
2007-02-10, by paulson
changed representation of constants; consistent name handling
2007-02-10, by haftmann
changed representation of constants
2007-02-10, by haftmann
tuned
2007-02-10, by haftmann
new Isar command print_codesetup
2007-02-10, by haftmann
added experimental class target
2007-02-10, by haftmann
added class target stub
2007-02-10, by haftmann
internal interfaces for interpretation and interpret
2007-02-10, by haftmann
moved commands of class package here
2007-02-10, by haftmann
added class package to Isar bootstrap
2007-02-10, by haftmann
splut up code generation in two parts
2007-02-10, by haftmann
canonical interface for attributes
2007-02-10, by haftmann
changed name of interpretation linorder to order
2007-02-10, by haftmann
adjusted to changes in class package
2007-02-10, by haftmann
added outline for Isabelle library description
2007-02-10, by haftmann
adjusted to new code generator Isar commands and changes in implementation
2007-02-10, by haftmann
adjusted to new code generator Isar commands
2007-02-10, by haftmann
added references for code generator tutorial
2007-02-10, by haftmann
added antiquotation for exceptions
2007-02-10, by haftmann
updated keywords
2007-02-10, by haftmann
cterm_instantiate was calling a type instantiation function that works only for matching,
2007-02-08, by paulson
added get-functions
2007-02-08, by urbanc
Renamed member to memb to avoid confusion with member function
2007-02-07, by berghofe
Adapted to changes in Finite_Set theory.
2007-02-07, by berghofe
Adapted to new inductive definition package.
2007-02-07, by berghofe
- Adapted to new inductive definition package
2007-02-07, by berghofe
Added meta_spec to extraction_expand.
2007-02-07, by berghofe
Added functions hhf_proof and un_hhf_proof.
2007-02-07, by berghofe
Adapted to changes in Accessible_Part and Wellfounded_Recursion theories.
2007-02-07, by berghofe
Added split_rule attribute.
2007-02-07, by berghofe
Fixed bug in mk_AbsP.
2007-02-07, by berghofe
Introduction and elimination rules for <= on predicates
2007-02-07, by berghofe
- Improved handling of monotonicity rules involving <=
2007-02-07, by berghofe
Adapted to changes in Finite_Set theory.
2007-02-07, by berghofe
Adapted to changes in Finite_Set theory.
2007-02-07, by berghofe
- Adapted to new inductive definition package
2007-02-07, by berghofe
Adapted to new inductive definition package.
2007-02-07, by berghofe
Converted to predicate notation.
2007-02-07, by berghofe
Adapted to changes in List theory.
2007-02-07, by berghofe
- wfP has been moved to theory Wellfounded_Recursion
2007-02-07, by berghofe
Adapted to changes in Transitive_Closure theory.
2007-02-07, by berghofe
Adapted to new inductive definition package.
2007-02-07, by berghofe
Adapted to changes in Finite_Set theory.
2007-02-07, by berghofe
Theorems for converting between wf and wfP are now declared
2007-02-07, by berghofe
- Adapted to new inductive definition package
2007-02-07, by berghofe
Adapted to new inductive definition package.
2007-02-07, by berghofe
Adapted to changes in Transitive_Closure theory.
2007-02-07, by berghofe
Added Predicate theory.
2007-02-07, by berghofe
New theory for converting between predicates and sets.
2007-02-07, by berghofe
changes in lexicographic_order termination tactic
2007-02-07, by bulwahn
"prove" function now instantiates relation variable in order
2007-02-07, by berghofe
Made untabify function tail recursive.
2007-02-07, by berghofe
tuned matches_subterm;
2007-02-06, by wenzelm
trace/debug: avoid eager string concatenation;
2007-02-06, by wenzelm
cc: removed option -lstdc++, which seems to be unnecessry, but causes problems on some platforms;
2007-02-06, by wenzelm
pervasive exception Option;
2007-02-06, by wenzelm
added has_kind/get_kind;
2007-02-06, by wenzelm
fixed two stupid bugs of SML to do with the value restriction and missing type
2007-02-06, by urbanc
askids/qualified_thms_of_thy: version which returns names in domain of get_thm
2007-02-06, by aspinall
added eta expansion to imperative monad bind
2007-02-06, by haftmann
corrected typo introduced by me
2007-02-06, by urbanc
now obsolete
2007-02-06, by urbanc
moved the infrastructure from the nominal_tags file to nominal_thmdecls
2007-02-06, by urbanc
Exporting curried versions of tail recursive equations instead of internal ones
2007-02-05, by krauss
proper use of NameSpace.is_qualified (avoids compatibility issues of the SML B library);
2007-02-05, by wenzelm
removed non-modular comment;
2007-02-04, by wenzelm
interpretation: attempt to be more serious about name_morphism;
2007-02-04, by wenzelm
added full_naming;
2007-02-04, by wenzelm
tuned oracle interface;
2007-02-04, by wenzelm
added print_strings;
2007-02-04, by wenzelm
old-fashioned abstype ctyp/cterm/thm prevents accidental equality tests;
2007-02-04, by wenzelm
def_simproc(_i): tuned interface;
2007-02-04, by wenzelm
added cterm interface;
2007-02-04, by wenzelm
type simproc: explicitl dependency of morphism;
2007-02-04, by wenzelm
load morphism.ML later;
2007-02-04, by wenzelm
added the two renaming functions from my PhD
2007-02-03, by urbanc
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
2007-02-02, by urbanc
a few additions and deletions
2007-02-02, by nipkow
tuned;
2007-02-01, by wenzelm
proper use of PureThy.has_name_hint instead of hard-wired string'';
2007-02-01, by wenzelm
removed non-modular comment;
2007-02-01, by wenzelm
new theorem int_infinite
2007-02-01, by paulson
Fix tell_thm_deps to match changse in PureThy.
2007-01-31, by aspinall
Expose hard-wired string which was changed and broke Proof General.
2007-01-31, by aspinall
clarified error message
2007-01-31, by haftmann
clarified command annotation
2007-01-31, by haftmann
changed cong alist - now using AList operations instead of overwrite_warn
2007-01-31, by haftmann
dropped Output.update_warn
2007-01-31, by haftmann
print translation for record types with empty-sorted type variables raise Match instead of producing an error
2007-01-31, by haftmann
dropped lemma duplicates in HOL.thy
2007-01-31, by haftmann
Tidying; more debugging information. New reference unwanted_types.
2007-01-31, by paulson
Tweak preferences for PGIP interfaces. Make <askids> return theory successors instead of parents (ideally should be content elements).
2007-01-30, by aspinall
Add get_succs
2007-01-30, by aspinall
Add operations on preference tables (remove, set_default).
2007-01-30, by aspinall
adjusted to new codegen_funcgr interface
2007-01-30, by haftmann
added interface for plugging in preprocessors
2007-01-30, by haftmann
additional auxiliary here
2007-01-30, by haftmann
whitespace tuning
2007-01-30, by haftmann
dropped dead code
2007-01-30, by haftmann
shifted import order
2007-01-30, by haftmann
dropped whitespace
2007-01-30, by haftmann
changed name of interpretation linorder to order
2007-01-30, by haftmann
proper simproc_setup;
2007-01-29, by wenzelm
added get_simproc, @{simproc};
2007-01-29, by wenzelm
added interface for target_naming;
2007-01-28, by wenzelm
added simproc_setup;
2007-01-28, by wenzelm
added def_simproc(_i) -- define named simprocs;
2007-01-28, by wenzelm
updated;
2007-01-28, by wenzelm
Now deals with simples cases where the input equations contain type variables
2007-01-28, by chaieb
refined algorithm
2007-01-26, by haftmann
clarified code
2007-01-26, by haftmann
exported interface for explicit error messages
2007-01-26, by haftmann
added NestedEnvironment
2007-01-26, by haftmann
Improved debugging
2007-01-26, by paulson
Streamlined and improved debugging messages
2007-01-26, by paulson
more fixes of arithmetic for min/max.
2007-01-26, by nipkow
min/max lemmas (actually unused!)
2007-01-26, by paulson
simplification of Suc/numeral combinations with min, max
2007-01-26, by paulson
Fixed long-standing, MAJOR bug in "lt"
2007-01-26, by paulson
adjusted manual to improved treatment of overloaded constants
2007-01-26, by haftmann
Allows evaluation of min/max o numerals.
2007-01-25, by nipkow
fixed bug for OCaml bigints
2007-01-25, by haftmann
tuned
2007-01-25, by haftmann
added explicit maintainance of coregular code theorems for overloaded constants
2007-01-25, by haftmann
dropped useless stuff
2007-01-25, by haftmann
clarified code
2007-01-25, by haftmann
added explicit query function for arities to subalgebra projection
2007-01-25, by haftmann
not importing NestedEnvironment
2007-01-25, by haftmann
adjusted to changes in class package
2007-01-25, by haftmann
made executable
2007-01-25, by haftmann
improved
2007-01-25, by haftmann
fxied bug for OCaml bigints
2007-01-25, by haftmann
adjusted names
2007-01-25, by haftmann
tuned eta_contract;
2007-01-24, by wenzelm
updated timing;
2007-01-24, by wenzelm
some new lemmas
2007-01-24, by paulson
Let <loadfile> execute even while a file is open interactively.
2007-01-24, by aspinall
fixes smlnj-related problem, updated signature
2007-01-23, by krauss
added a fold up and fold down as separate functions and fixed zipto to
2007-01-23, by dixon
simplified proofs
2007-01-22, by nipkow
Included ex/Fundefs.thy in HOL-ex session
2007-01-22, by krauss
* Preliminary implementation of tail recursion
2007-01-22, by krauss
Add location_of_position. Needs work elsewhere.
2007-01-22, by aspinall
Test askref
2007-01-22, by aspinall
Expose currently open file
2007-01-22, by aspinall
Sync location with pgip.rnc, fixing attribute names
2007-01-22, by aspinall
Add askrefs, setrefs, error_with_pos
2007-01-22, by aspinall
Comments
2007-01-22, by aspinall
Comment
2007-01-22, by aspinall
Add line_of, name_of destructors.
2007-01-22, by aspinall
Added lemma nat_size[simp]: "size (n::nat) = n"
2007-01-22, by krauss
tuned;
2007-01-22, by wenzelm
improved fact references: thmref;
2007-01-21, by wenzelm
added atomic, print_int;
2007-01-21, by wenzelm
tuned ML setup;
2007-01-21, by wenzelm
* ML in Isar: improved error reporting;
2007-01-21, by wenzelm
tuned;
2007-01-21, by wenzelm
*** MESSAGE REFERS TO PREVIOUS VERSION ***
2007-01-21, by wenzelm
*** MESSAGE REFERS TO PREVIOUS VERSION ***
2007-01-21, by wenzelm
tuned comments
2007-01-21, by wenzelm
simplified ML setup;
2007-01-21, by wenzelm
use_text: added name argument;
2007-01-21, by wenzelm
moved File.use to ML_Context.use;
2007-01-21, by wenzelm
use_text: added name argument;
2007-01-21, by wenzelm
Added simproc list_neq (prompted by an application)
2007-01-21, by nipkow
Added lists-as-multisets functions
2007-01-21, by nipkow
Simple and efficient binary numerals.
2007-01-20, by wenzelm
added HOL/ex/Binary.thy;
2007-01-20, by wenzelm
tuned ML setup;
2007-01-20, by wenzelm
* ML within Isar: antiquotations;
2007-01-20, by wenzelm
added @{theory};
2007-01-20, by wenzelm
added the_context_finished;
2007-01-20, by wenzelm
Toplevel.debug: coincide with Output.debugging;
2007-01-20, by wenzelm
ML tactic: proper context for compile and runtime;
2007-01-20, by wenzelm
tuned;
2007-01-20, by wenzelm
added @{simpset};
2007-01-20, by wenzelm
added is_finished_thy;
2007-01-20, by wenzelm
Output.debug: non-strict;
2007-01-20, by wenzelm
tuned ML setup;
2007-01-20, by wenzelm
added @{clasimpset};
2007-01-20, by wenzelm
added @{claset};
2007-01-20, by wenzelm
tuned;
2007-01-19, by wenzelm
tuned;
2007-01-19, by wenzelm
renamed Isar/isar_output.ML to Thy/thy_output.ML;
2007-01-19, by wenzelm
moved ML context stuff to from Context to ML_Context;
2007-01-19, by wenzelm
results: proper context;
2007-01-19, by wenzelm
tuned Scan.extend_lexicon;
2007-01-19, by wenzelm
renamed IsarOutput to ThyOutput;
2007-01-19, by wenzelm
moved parts to spec_parse.ML;
2007-01-19, by wenzelm
removed obsolete Method;
2007-01-19, by wenzelm
renamed IsarOutput to ThyOutput;
2007-01-19, by wenzelm
added various ML setup functions (from sign.ML, pure_thy.ML);
2007-01-19, by wenzelm
removed obsolete Attribute;
2007-01-19, by wenzelm
tuned signature;
2007-01-19, by wenzelm
renamed Isar/isar_output.ML to Thy/thy_output.ML;
2007-01-19, by wenzelm
tuned signature of extend_lexicon;
2007-01-19, by wenzelm
moved ML translation interfaces to isar_cmd.ML;
2007-01-19, by wenzelm
moved thm/thms to ml_context.ML;
2007-01-19, by wenzelm
moved inst from drule.ML to old_goals.ML;
2007-01-19, by wenzelm
tuned order;
2007-01-19, by wenzelm
renamed Isar/term_style.ML to Thy/term_style.ML;
2007-01-19, by wenzelm
renamed Isar/thy_header.ML to Thy/thy_header.ML;
2007-01-19, by wenzelm
ML context and antiquotations (material from context.ML);
2007-01-19, by wenzelm
Parsers for complex specifications (material from outer_parse.ML);
2007-01-19, by wenzelm
renamed Isar/isar_output.ML to Thy/thy_output.ML;
2007-01-19, by wenzelm
moved parts of OuterParse to SpecParse;
2007-01-19, by wenzelm
moved parts of OuterParse to SpecParse;
2007-01-19, by wenzelm
HOL-Lambda: usedir -m no_brackets;
2007-01-19, by wenzelm
simplified ML setup;
2007-01-19, by wenzelm
tuned;
2007-01-19, by wenzelm
renamed IsarOutput to ThyOutput;
2007-01-19, by wenzelm
updated;
2007-01-19, by wenzelm
moved ML context stuff to from Context to ML_Context;
2007-01-19, by wenzelm
renamed IsarOutput to ThyOutput;
2007-01-19, by wenzelm
interpreter for Finite_Set.finite added
2007-01-19, by webertj
reformatted to 80 chars/line
2007-01-19, by webertj
Theorem "(x::int) dvd 1 = ( ¦x¦ = 1)" added to default simpset.
2007-01-19, by chaieb
adapted ML context operations;
2007-01-19, by wenzelm
added generic_theory_of;
2007-01-19, by wenzelm
added 'declaration' command;
2007-01-19, by wenzelm
added 'declaration' command;
2007-01-19, by wenzelm
adapted ML context operations;
2007-01-19, by wenzelm
ML context: full generic context, tuned signature;
2007-01-19, by wenzelm
updated
2007-01-19, by wenzelm
Fix pgmlsymbolsoff
2007-01-18, by aspinall
tuned a bit the proofs
2007-01-17, by urbanc
correctled left/right following of another context in zipto.
2007-01-17, by dixon
induction rules for trancl/rtrancl expressed using subsets
2007-01-17, by paulson
Deleted mk_fol_type, since the constructors can be used directly
2007-01-17, by paulson
Streamlining: removing the type argument of CombApp; abbreviating ResClause as RC
2007-01-17, by paulson
fixed typo introduced by me
2007-01-16, by urbanc
changed dictionary representation to explicit classrel witnesses
2007-01-16, by haftmann
reverted order of classrels
2007-01-16, by haftmann
cleanup
2007-01-16, by haftmann
formalisation of Crary's chapter on logical relations
2007-01-16, by urbanc
added capabilities to handle mutual inductions
2007-01-16, by urbanc
refined and added example for ExecutableRat
2007-01-16, by haftmann
introduced binding concept
2007-01-16, by haftmann
slight cleanup
2007-01-16, by haftmann
renamed locale partial_order to order
2007-01-16, by haftmann
refined and added example for ExecutableRat
2007-01-16, by haftmann
updated keywords
2007-01-16, by haftmann
added sections on mutual induction and patterns
2007-01-15, by krauss
optimized translation of HO problems
2007-01-14, by paulson
Reverted to structure representation with records.
2007-01-12, by ballarin
more term inspection
2007-01-12, by haftmann
introduced binding concept
2007-01-12, by haftmann
adjusted manual
2007-01-12, by haftmann
well-founded relations for the integers
2007-01-11, by paulson
updated to mention the automatic unfolding of constants
2007-01-11, by webertj
removed NameSpace.split -- use qualifier/base instead;
2007-01-10, by wenzelm
fixed exit: proper type check of state;
2007-01-10, by wenzelm
tuned
2007-01-10, by webertj
minor comment change
2007-01-10, by webertj
no unfolding necessary anymore (refute does that automatically now)
2007-01-10, by webertj
improved case patterns
2007-01-10, by haftmann
added undefined in cases
2007-01-10, by haftmann
named preprocessorts
2007-01-09, by haftmann
cleanup
2007-01-09, by haftmann
activated new class code
2007-01-09, by haftmann
handling for "undefined" in case expressions
2007-01-09, by haftmann
named preprocessors
2007-01-09, by haftmann
The "of 1, simplified" stopped working some time ago, leaving these simprules
2007-01-09, by paulson
More compact proof reconstruction: lines having fewer than !min_deps dependences are folded
2007-01-09, by paulson
simplified the resoution proofs
2007-01-09, by paulson
Cleanup message model: add info fatality level. Add informfileoutdated and some use of completed flag.
2007-01-09, by aspinall
Add info fatality for error messages.
2007-01-09, by aspinall
Add informfileoutdated and completed flag. This makes the PGIP messages match the Broker states.
2007-01-09, by aspinall
slight cleanups
2007-01-09, by haftmann
improved names
2007-01-09, by haftmann
proper node names
2007-01-09, by haftmann
slight cleanup
2007-01-09, by haftmann
improved variable name handling
2007-01-09, by haftmann
moved variable environments here
2007-01-09, by haftmann
moved a lot to codegen_func.ML
2007-01-09, by haftmann
typo
2007-01-09, by haftmann
added map_abs_vars
2007-01-09, by haftmann
tuned signature;
2007-01-08, by wenzelm
print functions for typs and terms added
2007-01-07, by webertj
Be more chatty in PGIP file operations.
2007-01-07, by aspinall
A few lemmas about relative primes when dividing trough gcd
2007-01-06, by chaieb
A few theorems on integer divisibily.
2007-01-06, by chaieb
Introduction of a bound on DEPTH_ITER, to prevent the meson method from running forever
2007-01-05, by paulson
reverted to v1.60 (PolyML 4.1.3 still has the wrong signature for Array.modifyi)
2007-01-05, by webertj
added codegen_func.ML
2007-01-05, by haftmann
non-layout-sensitive syntax for Haskell
2007-01-05, by haftmann
some cleanup
2007-01-05, by haftmann
primitive definitions are always eta-expanded
2007-01-05, by haftmann
added block_enclose
2007-01-05, by haftmann
added CodeEval
2007-01-05, by haftmann
dealing with ml_string and char instances
2007-01-05, by haftmann
dealing with ml_string combinators
2007-01-05, by haftmann
adaptions
2007-01-05, by haftmann
removed Toplevel.print_exn hook -- existing error_msg_fn does the job;
2007-01-05, by wenzelm
RAW-ProofGeneral: more dependencies;
2007-01-05, by wenzelm
Proof.context now sent to watcher and used in type inference step of proof reconstruction
2007-01-05, by paulson
tuned msg;
2007-01-04, by wenzelm
removed obsolete ProofGeneral/syntax_standalone.ML;
2007-01-04, by wenzelm
approximate Syntax.read_int/nat by Int.fromString -- avoids dependency on Syntax module;
2007-01-04, by wenzelm
added mk_simproc': tuned interface;
2007-01-04, by wenzelm
clarification
2007-01-04, by haftmann
dropped function theorems are considered as deleted
2007-01-04, by haftmann
examples for evaluation oracle
2007-01-04, by haftmann
fixed eval oracle
2007-01-04, by haftmann
Be more chatty in PGIP file operations.proof_general_pgip.ML
2007-01-04, by aspinall
broken error handling for command syntax -- reverted to revision 1.9;
2007-01-04, by wenzelm
Use warning fatality
2007-01-04, by aspinall
Add warning fatality
2007-01-04, by aspinall
improvements to proof reconstruction. Some files loaded in a different order
2007-01-04, by paulson
using Array.modifyi (no functional change)
2007-01-04, by webertj
run as RAW session;
2007-01-04, by wenzelm
removed obsolete option -C;
2007-01-04, by wenzelm
removed obsolete Pure-copied target;
2007-01-04, by wenzelm
updated manual
2007-01-04, by haftmann
updated manual
2007-01-04, by haftmann
obsolete sign_of calls removed
2007-01-04, by webertj
fixed output
2007-01-04, by haftmann
different handling of eta expansion
2007-01-04, by haftmann
eta-expansion now only to common maximum number of arguments
2007-01-04, by haftmann
clarified code
2007-01-04, by haftmann
more term examples
2007-01-04, by haftmann
eliminated Option.app
2007-01-04, by haftmann
constants are unfolded, universal quantifiers are stripped, some minor changes
2007-01-04, by webertj
Fix error reporting in Emacs to also match Isar command failure exactly.
2007-01-03, by aspinall
Use Isar toplevel print_exn_fn for generating error responses instead of Output.error_msg.
2007-01-03, by aspinall
Expose command failure recovery code for top level.
2007-01-03, by aspinall
Selected functions from syntax module
2007-01-03, by aspinall
x-symbol is no longer switched off in the ATP linkup
2007-01-03, by paulson
Improvements to proof reconstruction. Now "fixes" is inserted
2007-01-03, by paulson
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
2007-01-03, by paulson
first version of structured proof reconstruction
2007-01-03, by paulson
Morphism.fact;
2007-01-02, by wenzelm
Term.lambda: abstract over arbitrary closed terms;
2007-01-02, by wenzelm
Add standalone file to help porters
2006-12-31, by aspinall
Quote arguments in PGIP exceptions. Tune comment.
2006-12-31, by aspinall
Initialise parser at startup. Remove some obsolete ProofGeneral.XXX outer syntax, mapping PGIP commands directly to Isar.
2006-12-31, by aspinall
Fix diagnostic kind (*are* spuriouscmd). Add init to get right table for logic at startup. Use theoryitem as default for unrecognised command.
2006-12-31, by aspinall
removed dead code;
2006-12-30, by wenzelm
removed conditional combinator;
2006-12-30, by wenzelm
removed conditional combinator;
2006-12-30, by wenzelm
refrain from setting ml_prompts again;
2006-12-30, by wenzelm
removed misleading OuterLex.eq_token;
2006-12-30, by wenzelm
pretty_statement: more careful handling of name_hint;
2006-12-30, by wenzelm
added has_name_hint;
2006-12-30, by wenzelm
removed obsolete name_hint handling;
2006-12-30, by wenzelm
removed conditional combinator;
2006-12-30, by wenzelm
removed obsolete support for polyml-4.9.1;
2006-12-30, by wenzelm
* Proof General: proper undo of final 'end'; discontinued Isabelle/classic;
2006-12-30, by wenzelm
inform_file_processed: Toplevel.init_empty;
2006-12-30, by wenzelm
refined notion of empty toplevel, admits undo of 'end';
2006-12-30, by wenzelm
Toplevel.init_state;
2006-12-30, by wenzelm
removed obsolete 'clear_undos';
2006-12-30, by wenzelm
removed obsolete clear_undos_theory;
2006-12-30, by wenzelm
major restructurings
2006-12-29, by haftmann
cleanup
2006-12-29, by haftmann
improved print of constructors in OCaml
2006-12-29, by haftmann
changed syntax for axclass attach
2006-12-29, by haftmann
removed obsolete cond_add_path;
2006-12-29, by wenzelm
removed obsolete context_thy etc.;
2006-12-29, by wenzelm
removed obsolete init_pgip;
2006-12-29, by wenzelm
removed obsolete init_context;
2006-12-29, by wenzelm
obsolete (cf. ProofGeneral/proof_general_emacs.ML);
2006-12-29, by wenzelm
tuned;
2006-12-29, by wenzelm
signed_string_of_int;
2006-12-29, by wenzelm
added proper header;
2006-12-29, by wenzelm
added signed_string_of_int (pruduces proper - instead of SML's ~);
2006-12-29, by wenzelm
removed obsolete proof_general.ML;
2006-12-29, by wenzelm
minor tuning;
2006-12-29, by wenzelm
tuned specifications/proofs;
2006-12-29, by wenzelm
replaced Sign.classes by Sign.all_classes (topologically sorted);
2006-12-29, by wenzelm
renamed Graph.project to Graph.subgraph;
2006-12-29, by wenzelm
replaced Sign.classes by Sign.all_classes (topologically sorted);
2006-12-29, by wenzelm
renamed project to subgraph, improved presentation, avoided unnecessary evaluation of predicate;
2006-12-29, by wenzelm
Sorts.minimal_classes;
2006-12-29, by wenzelm
classes: more direct way to achieve topological sorting;
2006-12-29, by wenzelm
replaced classes by all_classes (topologically sorted);
2006-12-29, by wenzelm
replaced Sign.classes by Sign.all_classes (topologically sorted);
2006-12-29, by wenzelm
Enable new Proof General code again after SML/NJ compatibility fixes by Florian.
2006-12-29, by aspinall
Typo in last commit
2006-12-29, by aspinall
explicit construction of operational classes
2006-12-29, by haftmann
less
more
|
(0)
-10000
-1792
+1792
+10000
+30000
tip