2007-04-13 haftmann 2007-04-13 canonical merge operations
2007-04-13 berghofe 2007-04-13 Removed erroneous application of rev in get_clauses that caused introduction rules taken from the InductivePackage database to be in the wrong order.
2007-04-13 krauss 2007-04-13 more robust proof
2007-04-13 ballarin 2007-04-13 Experimental code for the interpretation of definitions.
2007-04-13 ballarin 2007-04-13 Experimental interpretation code for definitions.
2007-04-13 ballarin 2007-04-13 New file for locale regression tests.
2007-04-13 narboux 2007-04-13 debug versions of finite_guess and fresh_guess do not fail if they can not solve the goal
2007-04-13 huffman 2007-04-13 minimize imports
2007-04-13 huffman 2007-04-13 new simp rule exp_ln; new standard proof of DERIV_exp_ln_one; changed imports
2007-04-13 huffman 2007-04-13 moved nonstandard derivative stuff from Deriv.thy into new file HDeriv.thy
2007-04-12 wenzelm 2007-04-12 added proj_value_antiq;
2007-04-12 wenzelm 2007-04-12 absdummy: use internal name uu to avoid renaming of popular names;
2007-04-12 urbanc 2007-04-12 tuned the proof of lemma pt_list_set_fresh (as suggested by Randy Pollack) and tuned the syntax for sub_contexts
2007-04-12 wenzelm 2007-04-12 updated;
2007-04-12 wenzelm 2007-04-12 output_basic: added isaantiq markup (only inside verbatim tokens);
2007-04-12 wenzelm 2007-04-12 newenvironment{isaantiq};
2007-04-12 paulson 2007-04-12 Zero variable indexes in clauses
2007-04-12 paulson 2007-04-12 Improved treatment of classrel/arity clauses
2007-04-12 paulson 2007-04-12 Fixed the treatment of TVars in conjecture clauses (they are deleted, not frozen)
2007-04-12 paulson 2007-04-12 Improved and simplified the treatment of classrel/arity clauses
2007-04-12 haftmann 2007-04-12 canonical merge operations
2007-04-12 huffman 2007-04-12 moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
2007-04-12 kleing 2007-04-12 run annomaly from makedist
2007-04-12 isatest 2007-04-12 set special ISABELLE_USER_HOME as in other isatest settings
2007-04-12 kleing 2007-04-12 isatest version of annomaly script. to be run from istatest-makedist.
2007-04-12 huffman 2007-04-12 new standard proof of lemma LIM_inverse
2007-04-11 huffman 2007-04-11 new class syntax for scaleR and norm classes
2007-04-11 krauss 2007-04-11 removed debugging code
2007-04-11 haftmann 2007-04-11 canonical merge operations
2007-04-11 haftmann 2007-04-11 tuned
2007-04-11 haftmann 2007-04-11 dropped legacy ML bindings
2007-04-11 huffman 2007-04-11 moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
2007-04-11 huffman 2007-04-11 move lemma real_of_nat_inverse_le_iff from NSA.thy to NthRoot.thy
2007-04-11 huffman 2007-04-11 new standard proof of convergent = Cauchy
2007-04-10 huffman 2007-04-10 new standard proof of LIMSEQ_realpow_zero
2007-04-10 huffman 2007-04-10 new LIM/isCont lemmas for abs, of_real, and power
2007-04-10 krauss 2007-04-10 some restructuring
2007-04-10 huffman 2007-04-10 interpretation bounded_linear_of_real
2007-04-10 huffman 2007-04-10 removed unnecessary premise from power_le_imp_le_base
2007-04-10 krauss 2007-04-10 proper handling of morphisms
2007-04-10 krauss 2007-04-10 Moving "FunDef" up in the HOL development graph, since it is independent from "Recdef" and "Datatype" now.
2007-04-10 wenzelm 2007-04-10 inline_antiq: no longer forces ML_Syntax.atomic;
2007-04-10 krauss 2007-04-10 removed dead code
2007-04-10 krauss 2007-04-10 tuned
2007-04-10 krauss 2007-04-10 added example for definitions in local contexts
2007-04-10 krauss 2007-04-10 removed obsolete workaround
2007-04-09 huffman 2007-04-09 generalized type of lemma setsum_product
2007-04-09 huffman 2007-04-09 new standard proofs of some LIMSEQ lemmas
2007-04-08 huffman 2007-04-08 rearranged sections
2007-04-08 huffman 2007-04-08 remove redundant lemmas
2007-04-07 krauss 2007-04-07 removed obsolete workarounds
2007-04-07 urbanc 2007-04-07 deleted remaining instances of swap_simp_a and swap_simp_b (obsolete now)
2007-04-07 urbanc 2007-04-07 tuned slightly the previous commit
2007-04-07 narboux 2007-04-07 perm_simp can now simplify using the rules (a,b) o a = b and (a,b) o b = a
2007-04-06 huffman 2007-04-06 add new standard proofs for limits of sequences
2007-04-05 berghofe 2007-04-05 Replaced add_inductive_i by add_inductive_global.
2007-04-05 berghofe 2007-04-05 - Tried to make name_of_thm more robust against changes of the structure of proofs. - Now uses add_inductive_global rather than add_inductive_i for the definition of the realizability predicate.
2007-04-05 berghofe 2007-04-05 - Removed occurrences of ProofContext.export in add_ind_def that caused theorems to end up in the wrong context - Explicit parameters are now generalized in theorems returned by add_inductive(_i)
2007-04-05 wenzelm 2007-04-05 thy_deps: sort Context.thy_ord;
2007-04-05 wenzelm 2007-04-05 added thy_ord -- order of creation; ancestors: back to traditional ad-hoc order (avoid occasional problems with get_thm);