isabelle: Graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -10000 -3000 -1000 -120 +120 +1000 +3000 +10000 +30000 tip

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