isabelle: Graph

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

@{binding} is not a constructor term and should not be inlined, otherwise we loose value polymorphism;
2009-03-25, by wenzelm
tuned;
2009-03-25, by wenzelm
use more informative Thm.proof_body_of for oracle demo;
2009-03-25, by wenzelm
Proofterm.approximate_proof_body;
2009-03-25, by wenzelm
fulfill_proof/thm_proof: pass whole proof_body, not just the projection to proof (which might be incomplete);
2009-03-25, by wenzelm
removed misleading make_proof_body, make_oracles, make_thms, which essentially assume a *full* proof;
2009-03-25, by wenzelm
avoid mixing of left/right associative infixes, to make it work with experimental Poly/ML 5.3 branch;
2009-03-25, by wenzelm
simplified addPrettyPrinter setup: may pass (fn ...) directly if type constraints are omitted -- addPrettyPrinter treated as a special case internally;
2009-03-24, by wenzelm
status_of: need to include local promises as well!
2009-03-24, by wenzelm
status_of: simultaneous list;
2009-03-24, by wenzelm
display derivation status of thms;
2009-03-24, by wenzelm
recover old ids;
2009-03-24, by wenzelm
report ML typing;
2009-03-24, by wenzelm
merged
2009-03-24, by wenzelm
merged
2009-03-24, by nipkow
NEWS: [arith]
2009-03-24, by nipkow
get_index: produce index of next pending token, not the last one;
2009-03-24, by wenzelm
register token positions persistently with context;
2009-03-24, by wenzelm
tuned;
2009-03-24, by wenzelm
more markup elements for ML programs;
2009-03-24, by wenzelm
merged
2009-03-24, by wenzelm
process at-sml-dev last -- takes very long (why?);
2009-03-24, by wenzelm
fix
2009-03-24, by nipkow
merged
2009-03-24, by nipkow
presburger uses [arith] now
2009-03-24, by nipkow
merged
2009-03-24, by wenzelm
merged
2009-03-24, by haftmann
added Imperative_HOL_ex
2009-03-24, by haftmann
Use assms rather than prems in find_theorems solves.
2009-03-24, by Timothy Bourke
clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
2009-03-23, by huffman
lemmas add_sign_intros
2009-03-23, by huffman
merged
2009-03-23, by haftmann
moved Imperative_HOL examples to Imperative_HOL/ex
2009-03-23, by haftmann
corrected variable renaming
2009-03-23, by haftmann
tuned error messages
2009-03-23, by haftmann
moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
2009-03-23, by haftmann
structure LinArith now named Lin_Arith
2009-03-23, by haftmann
suddenly infix identifier oo occurs in generated code
2009-03-23, by haftmann
datatype antiquote: maintain original Position.range, which is eventually attached to the resulting ML tokens;
2009-03-24, by wenzelm
eliminated non-canonical alias structure T = ML_Lex;
2009-03-24, by wenzelm
error "Static Errors";
2009-03-24, by wenzelm
more systematic type use_context;
2009-03-24, by wenzelm
tuned;
2009-03-23, by wenzelm
more systematic type use_context;
2009-03-23, by wenzelm
eliminated Output.ml_output;
2009-03-23, by wenzelm
pretty_ml/ml_pretty: proper handling of markup and string length;
2009-03-23, by wenzelm
more systematic type use_context;
2009-03-23, by wenzelm
removed obsolete ml_output;
2009-03-23, by wenzelm
more systematic type use_context;
2009-03-23, by wenzelm
more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;
2009-03-23, by wenzelm
de-camelized ML_Name_Space;
2009-03-23, by wenzelm
suppress status output for traditional tty modes (including Proof General);
2009-03-23, by wenzelm
added report_text -- status messages with text body;
2009-03-23, by wenzelm
maintain parse trees cumulatively;
2009-03-23, by wenzelm
Block markup: maintain output version within tree values (in accordance with String) -- changes operational behaviour wrt. print_mode;
2009-03-23, by wenzelm
future scheduler: reduced wait timeout if tasks need to be canceled -- to improve reactivity of interrupts;
2009-03-23, by wenzelm
merged
2009-03-23, by haftmann
Main is (Complex_Main) base entry point in library theories
2009-03-23, by haftmann
Main is (Complex_Main) base entry point in library theories
2009-03-23, by haftmann
added instances for bot, top, wellorder
2009-03-23, by haftmann
tuned header
2009-03-23, by haftmann
more canonical import, syntax fix
2009-03-23, by haftmann
merged
2009-03-23, by haftmann
merged
2009-03-22, by haftmann
more antiquotations
2009-03-22, by haftmann
moved import of module qelim to theory Presburger
2009-03-22, by haftmann
tuned header
2009-03-22, by haftmann
dropped theory Arith_Tools
2009-03-22, by haftmann
lemma nat_dvd_not_less moved here from Arith_Tools
2009-03-22, by haftmann
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
2009-03-22, by haftmann
merged
2009-03-22, by wenzelm
merged
2009-03-22, by nipkow
1. New cancellation simprocs for common factors in inequations
2009-03-22, by nipkow
clarified relationship of modules Code_Name and Code_Printer
2009-03-22, by haftmann
added Symreltab (binary relations of symbols) instance of TableFun
2009-03-22, by haftmann
proper signature;
2009-03-22, by wenzelm
added read_antiq, with improved error reporting;
2009-03-22, by wenzelm
ML_Lex.read_antiq;
2009-03-22, by wenzelm
ML_Lex.read_antiq;
2009-03-22, by wenzelm
simplified Antiquote.read (again);
2009-03-22, by wenzelm
export report -- version that actually covers all cases;
2009-03-22, by wenzelm
Test of advanced ML compiler invocation in Poly/ML 5.3.
2009-03-22, by wenzelm
ML/ml_test.ML: test of advanced ML compiler invocation in Poly/ML 5.3;
2009-03-22, by wenzelm
added pretty_ml;
2009-03-22, by wenzelm
export eval_antiquotes: refined version that operates on ML tokens;
2009-03-22, by wenzelm
ML_Lex.pos_of: regular position;
2009-03-22, by wenzelm
replaced Antiquote.is_antiq by Antiquote.is_text;
2009-03-22, by wenzelm
merged
2009-03-21, by wenzelm
extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3;
2009-03-21, by wenzelm
merged
2009-03-21, by wenzelm
merged
2009-03-21, by huffman
move field lemmas into class locale context
2009-03-21, by huffman
move diff_eq_0_iff_eq into class locale context
2009-03-21, by huffman
removed obsolete pprint operations;
2009-03-21, by wenzelm
added polyml_pp.ML: toplevel pretty printing for Poly/ML 4.x and 5.x before 5.3;
2009-03-21, by wenzelm
adapted toplevel_pp to ML_Pretty.pretty;
2009-03-21, by wenzelm
replaced install_pp/make_pp by more general toplevel_pp based on use_text;
2009-03-21, by wenzelm
simplified datatype ML_Pretty.pretty: model Isabelle not Poly/ML;
2009-03-21, by wenzelm
simplified datatype ML_Pretty.pretty: model Isabelle not Poly/ML;
2009-03-21, by wenzelm
Datatype for ML pretty printing (cf. mlsource/MLCompiler/Pretty.sml in Poly/ML 5.3).
2009-03-21, by wenzelm
Pretty.position;
2009-03-21, by wenzelm
added position;
2009-03-21, by wenzelm
added generic ML_Pretty interface;
2009-03-21, by wenzelm
restricted interrupts for tasks running as future worker thread -- attempt to prevent interrupt race conditions;
2009-03-21, by wenzelm
more ambitious ML_OPTIONS;
2009-03-21, by wenzelm
more stats;
2009-03-21, by wenzelm
added ML syntax markup;
2009-03-20, by wenzelm
report markup for ML tokens;
2009-03-20, by wenzelm
Antiquote.read: argument for reporting text;
2009-03-20, by wenzelm
future_job: do not inherit attributes, but enforce restricted interrupts -- attempt to prevent interrupt race conditions;
2009-03-20, by wenzelm
uniform ml_prompts for RAW and Pure;
2009-03-20, by wenzelm
eliminated old Addsimps;
2009-03-20, by wenzelm
Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
2009-03-20, by wenzelm
fixed possibility_tac;
2009-03-20, by wenzelm
eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
2009-03-20, by wenzelm
merged
2009-03-20, by wenzelm
merged
2009-03-20, by berghofe
split_codegen now eta-expands terms on-the-fly.
2009-03-20, by berghofe
proper context for prove_cont/adm_tac;
2009-03-20, by wenzelm
with_attributes: canonical capture/release scheme (potentially iron out race condition);
2009-03-20, by wenzelm