isabelle: Graph

replaced apply_copy by apply';
2006-11-04, by wenzelm
removed is_Trueprop (use can dest_Trueprop'' instead);
2006-11-04, by wenzelm
removed is_Trueprop (use can dest_Trueprop'' instead);
2006-11-04, by wenzelm
updated;
2006-11-04, by wenzelm
HOL_USEDIR_OPTIONS: -p 1 by default;
2006-11-04, by wenzelm
tuned;
2006-11-04, by wenzelm
* October 2006: Stefan Hohe, TUM;
2006-11-04, by wenzelm
replaced Toplevel.proof_to_theory by Toplevel.end_proof;
2006-11-04, by wenzelm
optional argument for timespan (default 100);
2006-11-04, by wenzelm
added at-mac-poly-e, at64-poly-e;
2006-11-04, by wenzelm
moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
2006-11-04, by huffman
new Deriv.thy contains stuff from Lim.thy
2006-11-04, by huffman
re-added simpdata.ML
2006-11-03, by haftmann
new ML serializer
2006-11-03, by haftmann
fixed problem with eta-expansion
2006-11-03, by haftmann
tuned
2006-11-03, by haftmann
fixed problem with variable names
2006-11-03, by haftmann
tightened notion of function equations
2006-11-03, by haftmann
dropped name_mangler.ML
2006-11-03, by haftmann
some example tweaking
2006-11-03, by haftmann
added particular test for partially applied case constants
2006-11-03, by haftmann
improved evaluation setup
2006-11-03, by haftmann
adapted to changes in codegen_data.ML
2006-11-03, by haftmann
added code gen II
2006-11-03, by haftmann
simplified reasoning tools setup
2006-11-03, by haftmann
dropped prop_cs
2006-11-03, by haftmann
dropped equals_conv for nbe
2006-11-03, by haftmann
first version of style guide
2006-11-03, by haftmann
continued tutorial
2006-11-03, by haftmann
added serialization keywords
2006-11-03, by haftmann
bugfix to zipto: left and right were wrong way around.
2006-11-02, by dixon
added sum_squared
2006-11-02, by nipkow
changed a misplaced "also" to a "moreover" (caused a loop somehow)
2006-11-01, by urbanc
changed to not compile Iteration and Recursion, but Lam_Funs instead
2006-11-01, by urbanc
move DERIV_sumr from Series.thy to Lim.thy
2006-11-01, by huffman
generalize type of lemma isCont_Id
2006-11-01, by huffman
new proof of Bseq_NSbseq using transfer
2006-11-01, by huffman
changed to use Lam_Funs
2006-11-01, by urbanc
clauses for iff-introduction, unfortunately useless
2006-11-01, by paulson
tuned
2006-11-01, by urbanc
Numerous cosmetic changes.
2006-11-01, by paulson
not needed anymore
2006-11-01, by urbanc
these files are superseded by the internal recursion combinator and the file Lam_Funs.thy
2006-11-01, by urbanc
More blacklisting
2006-11-01, by paulson
added lexicographic_order tactic
2006-11-01, by bulwahn
new SML serializer
2006-10-31, by haftmann
clarified make_term interface
2006-10-31, by haftmann
introduced CodegenData.add_func_legacy
2006-10-31, by haftmann
cleaned up
2006-10-31, by haftmann
adapted seralizer syntax
2006-10-31, by haftmann
adapted to new serializer syntax
2006-10-31, by haftmann
constructing proof
2006-10-31, by haftmann
dropped constructiv `->
2006-10-31, by haftmann
new serialization syntax; experimental extensions
2006-10-31, by haftmann
refined
2006-10-31, by haftmann
refined algorithm
2006-10-31, by haftmann
simplified preprocessor framework
2006-10-31, by haftmann
cleanup
2006-10-31, by haftmann
*** empty log message ***
2006-10-31, by haftmann
fixed type signature of Type.varify
2006-10-31, by haftmann
dropped junk
2006-10-31, by haftmann
disabled some code generation (an intermeidate solution)
2006-10-31, by haftmann
adapted to new serializer syntax
2006-10-31, by haftmann
added Equals_conv
2006-10-31, by haftmann
cleaned up
2006-10-31, by haftmann
adaptions to changes in preprocessor
2006-10-31, by haftmann
dropped nth_update
2006-10-31, by haftmann
Purely cosmetic
2006-10-30, by paulson
new file for defining functions in the lambda-calculus
2006-10-30, by urbanc
Added "recdef_wf" and "simp" attribute to "wf_measures"
2006-10-26, by krauss
Removed debugging output
2006-10-26, by krauss
removed free "x" from termination goal...
2006-10-26, by krauss
Added "measures" combinator for lexicographic combinations of multiple measures.
2006-10-26, by krauss
Conversion to clause form now tolerates Boolean variables without looping.
2006-10-26, by paulson
adapted to Stefan's new inductive package
2006-10-24, by urbanc
Fixed bug in the handling of congruence rules
2006-10-23, by krauss
(added entry)
2006-10-23, by haftmann
switched merge_alists'' to AList.merge'' whenever appropriate
2006-10-23, by haftmann
new single-step proofs
2006-10-23, by paulson
meson method MUST NOT use all safe rules, only basic ones for the logical connectives.
2006-10-23, by paulson
Improved tracing
2006-10-23, by paulson
fixed two bugs
2006-10-23, by haftmann
bugfixes
2006-10-23, by haftmann
added example with split
2006-10-23, by haftmann
cleanup in ML setup code
2006-10-23, by haftmann
added option of Haskell serializer
2006-10-23, by haftmann
continued
2006-10-23, by haftmann
Added freshness context to FCBs.
2006-10-23, by berghofe
Adapted to changes in FCBs.
2006-10-23, by berghofe
Added Compile and Height examples.
2006-10-23, by berghofe
Added Compile and Height examples to Nominal directory.
2006-10-23, by berghofe
removed antisym_setup.ML
2006-10-20, by haftmann
cleaned up
2006-10-20, by haftmann
final Haskell serializer
2006-10-20, by haftmann
dropped classop shallow namespace
2006-10-20, by haftmann
added Haskell
2006-10-20, by haftmann
added reserved words for Haskell
2006-10-20, by haftmann
slight cleanup
2006-10-20, by haftmann
extended section on code generator
2006-10-20, by haftmann
small refinements
2006-10-20, by haftmann
continued
2006-10-20, by haftmann
added entries for tutorials
2006-10-20, by haftmann
Proof of "bs # fK bs us vs" no longer depends on FCBs.
2006-10-20, by berghofe
example of a single-step proof reconstruction
2006-10-20, by paulson
Fixed the "exception Empty" bug in elim2Fol
2006-10-20, by paulson
Added more debugging info
2006-10-20, by paulson
nclauses no longer requires its input to be in NNF
2006-10-20, by paulson
cleanup
2006-10-20, by haftmann
explicit change of code width possible
2006-10-20, by haftmann
code nofunc now permits theorems violating typing discipline
2006-10-20, by haftmann
abandoned foldl
2006-10-20, by haftmann
fold cleanup
2006-10-20, by haftmann
slight cleanup
2006-10-20, by haftmann
slight adaption
2006-10-20, by haftmann
added normal post setup; cleaned up "execution" constants
2006-10-20, by haftmann
added normal post setup
2006-10-20, by haftmann
added if_delayed
2006-10-20, by haftmann
started tutorial
2006-10-20, by haftmann
code_constsubst -> code_axioms
2006-10-20, by haftmann
Symtab.foldl replaced by Symtab.fold
2006-10-20, by haftmann
Induction rule for graph of recursion combinator
2006-10-19, by berghofe
Split up FCBs into separate formulae for each binder.
2006-10-19, by berghofe
cleaning up
2006-10-18, by urbanc
adapted to Stefan's new inductive package and cleaning up
2006-10-18, by urbanc
Switched function package to use the new package for inductive predicates.
2006-10-18, by krauss
More robust error handling in make_nnf and forward_res
2006-10-18, by paulson
Stylistic improvements.
2006-10-18, by ballarin
Restructured and repaired code dealing with case names
2006-10-17, by berghofe
macbroy6 still has non-standard setup
2006-10-17, by kleing
moved HOL code generator setup to Code_Generator
2006-10-16, by haftmann
slight cleanup
2006-10-16, by haftmann
fixed print translations for bounded quantification
2006-10-16, by haftmann
added explicit print translation for nat_case
2006-10-16, by haftmann
added isactrlconst
2006-10-16, by haftmann
Order and lattice structures no longer based on records.
2006-10-16, by ballarin
add experimental macbroy6 (intel-darwin)
2006-10-15, by isatest
add experimental at64 poly-4.9.1 test on atbroy101
2006-10-15, by isatest
generate devel snapshot even if experimental builds fail.
2006-10-15, by kleing
added peek;
2006-10-14, by wenzelm
added theorem(_i);
2006-10-14, by wenzelm
export map_elem;
2006-10-14, by wenzelm
added assert;
2006-10-14, by wenzelm
theorem: added local_theory version;
2006-10-14, by wenzelm
Attrib.pretty_attrib;
2006-10-14, by wenzelm
added pretty_attribs (from attrib.ML);
2006-10-14, by wenzelm
moved pretty_attribs to attrib.ML;
2006-10-14, by wenzelm
locale begin/end;
2006-10-14, by wenzelm
updated;
2006-10-13, by wenzelm
Added keywords for new inductive definition package.
2006-10-13, by berghofe
Adapted to changes in FixedPoint theory.
2006-10-13, by berghofe
Moved old inductive package to old_inductive_package.ML
2006-10-13, by berghofe
Completely rewrote inductive definition package. Now allows to
2006-10-13, by berghofe
Old version of inductive definition package (for sets).
2006-10-13, by berghofe
Moved old inductive package to old_inductive_package.ML
2006-10-13, by berghofe
Adapted to new inductive definition package.
2006-10-13, by berghofe
Adapted to changes in FixedPoint theory.
2006-10-13, by berghofe
Legacy ML bindings now refer to old inductive definition package.
2006-10-13, by berghofe
Added new package for inductive definitions, moved old package
2006-10-13, by berghofe
Generalized gfp and lfp to arbitrary complete lattices.
2006-10-13, by berghofe
Repaired strip_assums_hyp (now also works for goals not
2006-10-13, by berghofe
improved framework
2006-10-13, by haftmann
refined
2006-10-13, by haftmann
fixed bug
2006-10-13, by haftmann
tuned
2006-10-13, by haftmann
added codegen2 example
2006-10-13, by haftmann
added the missing freshness-lemmas for nat, int, char and string and
2006-10-13, by urbanc
lifted claset setup from ML to Isar level
2006-10-13, by haftmann
explicit nonfix for union and inter
2006-10-13, by haftmann
renamed enter_forward_proof to enter_proof_body;
2006-10-12, by wenzelm
added peek;
2006-10-12, by wenzelm
interpretation_in_locale: standalone goal setup;
2006-10-12, by wenzelm
tuned;
2006-10-12, by wenzelm
renamed print_lthms to print_facts, do not insist on proof state;
2006-10-12, by wenzelm
print_evaluated_term: Toplevel.context_of;
2006-10-12, by wenzelm
replaced attributes_update by map_attributes;
2006-10-12, by wenzelm
Toplevel.local_theory_to_proof: proper target;
2006-10-12, by wenzelm
Toplevel.local_theory: proper target;
2006-10-12, by wenzelm
To be consistent with "induct", I renamed "fixing" to "arbitrary".
2006-10-12, by urbanc
Extended combinators now disabled
2006-10-12, by paulson
abstraction is now turned OFF...
2006-10-12, by paulson
Logging of theorem names to the /tmp directory now works
2006-10-12, by paulson
cc: avoid space after options;
2006-10-12, by wenzelm
set DYLD_LIBRARY_PATH (for Darwin);
2006-10-12, by wenzelm
added execute/system;
2006-10-12, by wenzelm
added x86-darwin;
2006-10-12, by wenzelm
now allowing subdirectories in Doc/
2006-10-12, by haftmann
added makefile layer
2006-10-12, by haftmann
* isabelle-process: option -S (secure mode) disables some critical operations;
2006-10-11, by wenzelm
increased heap size for polyml-4.9.1;
2006-10-11, by wenzelm
tuned Toplevel.begin_local_theory;
2006-10-11, by wenzelm
exit_local_theory: pass interactive flag;
2006-10-11, by wenzelm
exit: pass interactive flag;
2006-10-11, by wenzelm
added begin parser;
2006-10-11, by wenzelm
is_sid: disallow 'begin' keyword as identifier;
2006-10-11, by wenzelm
exit: pass interactive flag, toplevel result convention;
2006-10-11, by wenzelm
add_defs: declare terms;
2006-10-11, by wenzelm
'context': demand 'begin', support local theory;
2006-10-11, by wenzelm
removed 'undo_end', recovered 'cannot_undo';
2006-10-11, by wenzelm
tuned signature;
2006-10-11, by wenzelm
minor refinements in serialization
2006-10-11, by haftmann
adapted to signature change
2006-10-11, by haftmann
slight type signature changes
2006-10-11, by haftmann
cleaned up HOL bootstrap
2006-10-11, by haftmann
abandoned findrep
2006-10-11, by haftmann
added code generator setup
2006-10-11, by haftmann
added code lemma
2006-10-11, by haftmann
Abstraction re-use code now checks that the abstraction function can be used in the current
2006-10-11, by paulson
added examples for nested let
2006-10-11, by haftmann
added tex files to CVS
2006-10-11, by haftmann
renamed body_context_node to presentation_context;
2006-10-11, by wenzelm
add_locale(_i): return actual result context;
2006-10-11, by wenzelm
class(_i): mimic Locale.add_locale(_i);
2006-10-11, by wenzelm
added type global_theory -- theory or local_theory;
2006-10-11, by wenzelm
added begin;
2006-10-11, by wenzelm
added opt_begin;
2006-10-11, by wenzelm
added raw_theory(_result);
2006-10-11, by wenzelm
Toplevel.end_proof;
2006-10-11, by wenzelm
'end': handle local theory;
2006-10-11, by wenzelm
undo_end/kill: handle local theory;
2006-10-11, by wenzelm
Toplevel: generic_theory;
2006-10-11, by wenzelm
made some proof look more like the ones in Barendregt
2006-10-10, by urbanc
A way to call the ATP linkup from ML scripts
2006-10-10, by paulson
Combinators require the theory name; added settings for SPASS
2006-10-10, by paulson
stripped pointless head
2006-10-10, by haftmann
gen_rem(s) abandoned in favour of remove / subtract
2006-10-10, by haftmann
added IsarAdvanced material
2006-10-10, by haftmann
Induction rules have schematic variables again.
2006-10-10, by krauss
initial draft
2006-10-10, by haftmann
*** empty log message ***
2006-10-10, by haftmann
initial draft
2006-10-10, by haftmann
fixed intendation
2006-10-10, by haftmann
cleanup basic HOL bootstrap
2006-10-10, by haftmann
added legacy tactic
2006-10-10, by haftmann
purged some ML legacy
2006-10-10, by haftmann
added eq_True eq_False True_implies_equals to extraction_expand
2006-10-10, by haftmann
no breaks for Haskell
2006-10-10, by haftmann
removed experimental codegen_simtype
2006-10-10, by haftmann
added keeping of funcgr
2006-10-10, by haftmann
generalized purge
2006-10-10, by haftmann
changed order
2006-10-10, by haftmann
removed quote in serialization
2006-10-10, by haftmann
added code_abstype
2006-10-10, by haftmann
added code_constsubst
2006-10-10, by haftmann
fixed typo
2006-10-10, by haftmann
added code_abstype and code_constsubst
2006-10-10, by haftmann
isabelle-process: options -S, -X;
2006-10-09, by wenzelm
tuned;
2006-10-09, by wenzelm
loop: disallow exit in secure mode;
2006-10-09, by wenzelm
Secure.commit;
2006-10-09, by wenzelm
moved Context.ml_output to Output.ml_output;
2006-10-09, by wenzelm
Secure critical operations.
2006-10-09, by wenzelm
added General/secure.ML;
2006-10-09, by wenzelm
added option -S (secure mode);
2006-10-09, by wenzelm
added nbe_post for delayed_if
2006-10-09, by nipkow
added delayed_if
2006-10-09, by nipkow
added pre/post-processor equations
2006-10-09, by nipkow
attribute "symmetric": standardized schematic variables;
2006-10-09, by wenzelm
sequential lemmas;
2006-10-09, by wenzelm
reorderd ML/lemmas (Why!?);
2006-10-09, by wenzelm
PureThy.note_thmss_i;
2006-10-09, by wenzelm
added exit;
2006-10-09, by wenzelm
added theorems(_i) -- with present_results;
2006-10-09, by wenzelm
def(_i): LocalDefs.add_defs;
2006-10-09, by wenzelm
attribute: Context.mapping;
2006-10-09, by wenzelm
removed obsolete note_thmss(_i);
2006-10-09, by wenzelm
added exit;
2006-10-09, by wenzelm
simplified derived_def;
2006-10-09, by wenzelm
removed theorems, smart_theorems etc. (cf. Specification.theorems);
2006-10-09, by wenzelm
lemmas/theorems/declare: Specification.theorems;
2006-10-09, by wenzelm
added kind attributes;
2006-10-09, by wenzelm
Drule.lhs/rhs_of;
2006-10-09, by wenzelm
added dest_equals_lhs;
2006-10-09, by wenzelm
attribute: Context.mapping;
2006-10-09, by wenzelm
replaced Drule.clhs/crhs_of by Drule.lhs/rhs_of;
2006-10-09, by wenzelm
attribute: Context.mapping;
2006-10-09, by wenzelm
standardized facts;
2006-10-09, by wenzelm
attribute symmetric: zero_var_indexes;
2006-10-09, by wenzelm
attribute symmetric: zero_var_indexes;
2006-10-09, by wenzelm
attribute: Context.mapping;
2006-10-09, by wenzelm
cleaned up interfaces
2006-10-07, by haftmann
Removed unused res_atp_setup.ML, since its functions have been put in res_atp.ML.
2006-10-07, by mengj
Common theory targets.
2006-10-07, by wenzelm
Element.export_facts;
2006-10-07, by wenzelm
refined unlocalize_mixfix;
2006-10-07, by wenzelm
TheoryTarget;
2006-10-07, by wenzelm
moved pretty_consts to proof_display.ML;
2006-10-07, by wenzelm
added pretty_consts (from specification.ML);
2006-10-07, by wenzelm
turned into abstract wrapper module, cf. theory_target.ML;
2006-10-07, by wenzelm
replaced add_def by more elaborate add_defs;
2006-10-07, by wenzelm
replaced generalize_facts by full export_(standard_)facts;
2006-10-07, by wenzelm
Thm.def_name_optional;
2006-10-07, by wenzelm
added def_name_optional;
2006-10-07, by wenzelm
removed is_equals, is_implies;
2006-10-07, by wenzelm
added the_single;
2006-10-07, by wenzelm
added term_rule;
2006-10-07, by wenzelm
added Isar/theory_target.ML;
2006-10-07, by wenzelm
improved LocalDefs.add_def;
2006-10-07, by wenzelm
mk_partial_rules_mutual: expand result terms/thms;
2006-10-07, by wenzelm
removed with_local_path -- LocalTheory.note admits qualified names;
2006-10-07, by wenzelm
moved the_single to Pure/library.ML;
2006-10-07, by wenzelm
TheoryTarget.init;
2006-10-07, by wenzelm
tuned comments;
2006-10-07, by wenzelm
tuned method syntax: polymorhic term argument;
2006-10-07, by wenzelm
tuned;
2006-10-07, by wenzelm
Fixed the printing of the used theorems by maintaining separate lists for each subgoal.
2006-10-06, by paulson
Tidied code to delete tmp files.
2006-10-06, by paulson
renamed the combinator laws
2006-10-06, by paulson
Improved detection of identical clauses, also in the conjecture
2006-10-06, by paulson
Refinements to abstraction. Seeding with combinators K, I and B.
2006-10-06, by paulson
examples for hex and bin numerals
2006-10-06, by kleing
Changed and removed some functions related to combinators, since they are Isabelle constants now.
2006-10-05, by mengj
Now the DFG output includes correct declarations of c_fequal, but not hEXTENT
2006-10-05, by paulson
improvements to abstraction, ensuring more re-use of abstraction functions
2006-10-05, by paulson
facts about combinators
2006-10-05, by paulson
a few new functions on thms and cterms
2006-10-05, by paulson
reorganize and speed up termdiffs proofs
2006-10-05, by huffman
fixed bug in linear arith
2006-10-04, by nipkow
improvements for Haskell serialization
2006-10-04, by haftmann
insert replacing ins ins_int ins_string
2006-10-04, by haftmann
cleaned up some mess
2006-10-04, by haftmann
clarified header comments
2006-10-04, by haftmann
insert replacing ins ins_int ins_string
2006-10-04, by haftmann
*** empty log message ***
2006-10-04, by haftmann
tuned
2006-10-04, by webertj
Improved error reporting
2006-10-04, by krauss
nnf_simpset built statically
2006-10-04, by webertj
rewrite proofs of powser_insidea and termdiffs_aux
2006-10-03, by huffman
generalize summability lemmas using class banach
2006-10-02, by huffman
clarified setup name
2006-10-02, by haftmann
various code refinements
2006-10-02, by haftmann
fixed some Haskell issues
2006-10-02, by haftmann
changed preprocessing framework
2006-10-02, by haftmann
clarified some things
2006-10-02, by haftmann
cleaned and extended
2006-10-02, by haftmann
added gen_primrec
2006-10-02, by haftmann
added code for insert
2006-10-02, by haftmann
improvements for code_gen
2006-10-02, by haftmann
cleaned mess
2006-10-02, by haftmann
added example for code_gen
2006-10-02, by haftmann
dropped obsolete Theory.sign_of
2006-10-02, by haftmann
tuned
2006-10-02, by haftmann
added code generator names for nat_rec and nat_case
2006-10-02, by haftmann
improved serialization for arbitrary
2006-10-02, by haftmann
normal_form now a diagnostic command
2006-10-02, by haftmann
restructured contents
2006-10-02, by haftmann
add axclass banach for complete normed vector spaces
2006-10-02, by huffman
remove unused Cauchy_Bseq lemmas
2006-10-02, by huffman
add lemmas norm_not_less_zero, norm_le_zero_iff
2006-10-02, by huffman
added is_Trueprop
2006-10-02, by paulson
tidying and simplifying
2006-10-02, by paulson
Changing the default for theory_const
2006-10-02, by paulson
extensions for Susanto
2006-10-02, by paulson
restored the "length of name > 2" check for package definitions
2006-10-02, by paulson
Now checks explicitly for Trueprop, thereby ignoring junk theorems involving OF_CLASS, etc.
2006-10-02, by paulson
exists_name: include this theory name;
2006-10-01, by wenzelm
removed obsolete Datatype_Universe.thy (cf. Datatype.thy);
2006-10-01, by wenzelm
merged with theory Datatype_Universe;
2006-10-01, by wenzelm
obsolete;
2006-10-01, by wenzelm
renamed ex/SVC_Oracle.ML to ex/svc_oracle.ML;
2006-10-01, by wenzelm
removed share_data;
2006-10-01, by wenzelm
cterm_match: avoid recalculation of maxidx;
2006-10-01, by wenzelm
reverted to revision 1.28;
2006-10-01, by wenzelm
proper use of svc_oracle.ML;
2006-10-01, by wenzelm
reactivated theory PER;
2006-10-01, by wenzelm
tuned proofs;
2006-10-01, by wenzelm
moved theory Infinite_Set to Library;
2006-10-01, by wenzelm
moved theory Infinite_Set to Library;
2006-10-01, by wenzelm
moved Infinite_Set.thy to Library;
2006-10-01, by wenzelm
tuned;
2006-10-01, by wenzelm
Removed the helper files (combinator rewrite rules, function extensionality and fequal rules).
2006-10-01, by mengj
generalize more DERIV proofs
2006-10-01, by huffman
statement: Variable.fix_frees;
2006-09-30, by wenzelm
added undo_end;
2006-09-30, by wenzelm
tuned proofs;
2006-09-30, by wenzelm
proper import of Main HOL;
2006-09-30, by wenzelm
tuned specifications and proofs;
2006-09-30, by wenzelm
hides popular names (from Datatype.thy);
2006-09-30, by wenzelm
removed obsolete sum_case_Inl/Inr;
2006-09-30, by wenzelm
renamed Variable.invent_fixes to Variable.variant_fixes;
2006-09-30, by wenzelm
generalize proofs of DERIV_isCont and DERIV_mult
2006-09-30, by huffman
generalized some DERIV proofs
2006-09-30, by huffman
add scaleR lemmas
2006-09-30, by huffman
generalize type of DERIV
2006-09-30, by huffman
add type annotations for DERIV
2006-09-30, by huffman
Combinator axioms are now from Isabelle theorems, no need to use helper files.
2006-09-30, by mengj
Added the combinator constants to the constants table.
2006-09-30, by mengj
Removed ResHolClause.LAM2COMB exception.
2006-09-30, by mengj
Reordered how files are loaded.
2006-09-30, by mengj
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
2006-09-29, by wenzelm
removed mixfix_content;
2006-09-29, by wenzelm
Syntax.mode;
2006-09-29, by wenzelm
Syntax.mode;
2006-09-29, by wenzelm
Sign.add_consts_authentic;
2006-09-29, by wenzelm
proper use of matrixlp.ML;
2006-09-29, by wenzelm
simplified is_package_def -- be less ambitious about B library operations;
2006-09-29, by wenzelm
obsolete;
2006-09-28, by wenzelm
added share_data;
2006-09-28, by wenzelm
Sign.add_consts_authentic;
2006-09-28, by wenzelm
consts: syntax consts only for actual syntax;
2006-09-28, by wenzelm
added share_data (dummy);
2006-09-28, by wenzelm
removed obsolete HOLCF.ML;
2006-09-28, by wenzelm
ResAtpset.get_atpset;
2006-09-28, by wenzelm
removed legacy code;
2006-09-28, by wenzelm
tuned definitions/proofs;
2006-09-28, by wenzelm
proper use of float.ML;
2006-09-28, by wenzelm
fixed translations: CONST;
2006-09-28, by wenzelm
replaced syntax/translations by abbreviation;
2006-09-28, by wenzelm
replaced syntax/translations by abbreviation;
2006-09-28, by wenzelm
removed obsolete Real/document/root.tex;
2006-09-28, by wenzelm
tuned;
2006-09-28, by wenzelm
rearranged axioms and simp rules for scaleR
2006-09-28, by huffman
added Poly/ML 4.9.1 (experimental!);
2006-09-28, by wenzelm
rearranged axioms and simp rules for scaleR
2006-09-28, by huffman
clearout of obsolete code
2006-09-28, by paulson
addition of combinators
2006-09-28, by paulson
tuned messages;
2006-09-28, by wenzelm
tuned;
2006-09-28, by wenzelm
LD_LIBRARY_PATH;
2006-09-28, by wenzelm
Definitions produced by packages are now blacklisted.
2006-09-28, by paulson
more reorganizing sections
2006-09-28, by huffman
reorganize sections
2006-09-28, by huffman
add intro/dest rules for NSLIM; rewrite equivalence proofs using transfer
2006-09-28, by huffman
add lemma hypreal_epsilon_gt_zero
2006-09-28, by huffman
generalize type of is(NS)UCont
2006-09-28, by huffman
add intro/dest rules for (NS)LIMSEQ and (NS)Cauchy; rewrite equivalence proofs using transfer
2006-09-28, by huffman
proper use of PolyML.shareCommonData;
2006-09-28, by wenzelm
add lemmas InfinitesimalI2, InfinitesimalD2
2006-09-27, by huffman
adapted to pre-5.0 versions;
2006-09-27, by wenzelm
Poly/ML startup script (for 4.9.1);
2006-09-27, by wenzelm
added ML-Systems/polyml-4.9.1.ML;
2006-09-27, by wenzelm
Compatibility wrapper for Poly/ML 4.9.1.
2006-09-27, by wenzelm
removed all references to star_n and FreeUltrafilterNat
2006-09-27, by huffman
add lemmas about hnorm, Infinitesimal
2006-09-27, by huffman
reverted to 1.58;
2006-09-27, by wenzelm
proper const_syntax for uminus, abs;
2006-09-27, by wenzelm
reorganized HNatInfinite proofs; simplified and renamed some lemmas
2006-09-27, by huffman
removed obsolete of_instream_slurp -- now already included in tty;
2006-09-27, by wenzelm
Source.tty now slurps by default;
2006-09-27, by wenzelm
of_stream/tty: slurp input eagerly;
2006-09-27, by wenzelm
tuned all_paths;
2006-09-27, by wenzelm
internal params: Vartab instead of AList;
2006-09-27, by wenzelm
removed unused serial_of, name_of;
2006-09-27, by wenzelm
removed redundant lemmas;
2006-09-27, by wenzelm
remove redundant lemmas
2006-09-27, by huffman
replaced constant 0 by HOL.zero
2006-09-27, by haftmann
hypreal_of_nat abbreviates of_nat
2006-09-27, by huffman
add lemmas of_real_eq_star_of, Reals_eq_Standard
2006-09-27, by huffman
move star_of_norm from SEQ.thy to NSA.thy
2006-09-27, by huffman
convert more proofs to transfer principle
2006-09-27, by huffman
add lemmas about Standard, real_of, scaleR
2006-09-27, by huffman
instance complex :: real_normed_field; cleaned up
2006-09-27, by huffman
add lemma stc_unique; shorten stc proofs
2006-09-27, by huffman
add lemmas approx_diff and st_unique, shorten st proofs
2006-09-27, by huffman
add lemmas about of_real and power
2006-09-27, by huffman
reorganize section headings
2006-09-27, by huffman
more lemmas about Standard and star_of
2006-09-27, by huffman
define new constant Standard = range star_of
2006-09-27, by huffman
add lemmas of_int_in_Reals, of_nat_in_Reals
2006-09-27, by huffman
add header
2006-09-26, by huffman
Changed precedence of "op O" (relation composition) from 60 to 75.
2006-09-26, by krauss
handling of \<^const> syntax for case; explicit case names for induction rules for rep_datatype
2006-09-26, by haftmann
tuned syntax for <= <
2006-09-26, by haftmann
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
2006-09-26, by haftmann
renamed 0 and 1 to HOL.zero and HOL.one respectivly
2006-09-26, by haftmann
fixed the definition of "depth"
2006-09-26, by paulson
Abstraction now handles equations where the RHS is a lambda-expression; also, strings of lambdas
2006-09-26, by paulson
some cleanup
2006-09-25, by haftmann
changed order
2006-09-25, by haftmann
inserted headings
2006-09-25, by haftmann
changed interface in codegen_package.ML
2006-09-25, by haftmann
fixed some mess
2006-09-25, by haftmann
cleaned up
2006-09-25, by haftmann
adding constants the modern way
2006-09-25, by haftmann
added examples for variable name handling
2006-09-25, by haftmann
better handling for div by zero
2006-09-25, by haftmann
updated theory description
2006-09-25, by haftmann
refinements in codegen serializer
2006-09-25, by haftmann
added 'undefined' serializer
2006-09-25, by haftmann
added code_instname
2006-09-25, by haftmann
reorganized subsection headings
2006-09-24, by huffman