Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-10000
-3000
-1000
-240
+240
+1000
+3000
+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.
Removed an "apply arith" where there are already "No Subgoals"
2006-07-31, by krauss
code reformatted
2006-07-31, by webertj
Additional freshness constraints for FCB.
2006-07-31, by berghofe
proper Element.generalize_facts;
2006-07-30, by wenzelm
add_consts: proper Sign.full_name;
2006-07-30, by wenzelm
added generalize_facts;
2006-07-30, by wenzelm
added maxidx_values;
2006-07-30, by wenzelm
export: refrain from adjusting maxidx;
2006-07-30, by wenzelm
adjust_maxidx: pass explicit lower bound;
2006-07-30, by wenzelm
Thm.adjust_maxidx;
2006-07-30, by wenzelm
removed unused add_in_order/add_once (cf. OrdList.insert);
2006-07-30, by wenzelm
demod_rule: depend on context, proper Variable.import/export;
2006-07-30, by wenzelm
tuned proofs;
2006-07-30, by wenzelm
lin_arith_prover splits certain operators (e.g. min, max, abs)
2006-07-30, by webertj
bugfix related to cancel_div_mod simproc
2006-07-30, by webertj
lin_arith_prover splits certain operators (e.g. min, max, abs)
2006-07-29, by webertj
rename legacy_pretty_thm to pretty_thm_legacy;
2006-07-29, by wenzelm
tuned comment;
2006-07-29, by wenzelm
added add_fixes_direct;
2006-07-29, by wenzelm
prove: proper assumption context, more tactic arguments;
2006-07-29, by wenzelm
added mk_conjunction_list;
2006-07-29, by wenzelm
Goal.prove: more tactic arguments;
2006-07-29, by wenzelm
Checking for unsound proofs. Tidying.
2006-07-28, by paulson
"all theorems" mode forces definition-expansion off.
2006-07-28, by paulson
title fixed
2006-07-28, by webertj
replaced extern_skolem by slightly more simplistic revert_skolems;
2006-07-27, by wenzelm
renamed ProofContext.fix_frees to Variable.fix_frees;
2006-07-27, by wenzelm
replaced ProofContext.extern_skolem by slightly more simplistic ProofContext.revert_skolems;
2006-07-27, by wenzelm
no_vars: based on Variable.import;
2006-07-27, by wenzelm
added fix_frees (from Isar/proof_context.ML);
2006-07-27, by wenzelm
declare_term_names: cover types as well;
2006-07-27, by wenzelm
eliminated obsolete freeze_thaw;
2006-07-27, by wenzelm
type annotation added to make SML/NJ happy
2006-07-27, by webertj
"moved basic assumption operations from structure ProofContext to Assumption;"
2006-07-27, by wenzelm
ProofContext.legacy_pretty_thm;
2006-07-27, by wenzelm
added legacy_pretty_thm (with fall-back on ProtoPure.thy);
2006-07-27, by wenzelm
Assumption.assume;
2006-07-27, by wenzelm
removed obsolete is_fact (cf. Thm.no_prems);
2006-07-27, by wenzelm
tuned interfaces;
2006-07-27, by wenzelm
read_def_cterms (legacy version): Consts.certify;
2006-07-27, by wenzelm
Assumption.assume;
2006-07-27, by wenzelm
moved Goal.norm_hhf(_protect) to meta_simplifier.ML (pervasive);
2006-07-27, by wenzelm
removed obsolete equal_abs_elim(_list);
2006-07-27, by wenzelm
removed obsolete pretty_thm_no_quote;
2006-07-27, by wenzelm
added Pure/assumption.ML;
2006-07-27, by wenzelm
moved basic assumption operations from structure ProofContext to Assumption;
2006-07-27, by wenzelm
tuned proofs;
2006-07-27, by wenzelm
Local assumptions, parameterized by export rules.
2006-07-27, by wenzelm
updated;
2006-07-26, by wenzelm
import(T): result includes fixed types/terms;
2006-07-26, by wenzelm
focus: result record includes (fixed) schematic variables;
2006-07-26, by wenzelm
Variable.import(T): result includes fixed types/terms;
2006-07-26, by wenzelm
linear arithmetic splits certain operators (e.g. min, max, abs)
2006-07-26, by webertj
added eval_term
2006-07-26, by haftmann
updated;
2006-07-26, by wenzelm
fixed LaTeX problem;
2006-07-26, by wenzelm
added eval_term
2006-07-26, by haftmann
Removed wrong sentence (Simon Funke)
2006-07-26, by nipkow
moved pprint functions to Isar/proof_display.ML;
2006-07-26, by wenzelm
Tactical operations depending on local subgoal structure.
2006-07-26, by wenzelm
moved pprint functions to Isar/proof_display.ML;
2006-07-26, by wenzelm
export goal_tac (was internal refine_tac);
2006-07-26, by wenzelm
added Pure/subgoal.ML;
2006-07-26, by wenzelm
updated;
2006-07-25, by wenzelm
raw symbols: disallow dot to avoid confusion in NameSpace.unpack;
2006-07-25, by wenzelm
avoid Term.is_funtype;
2006-07-25, by wenzelm
avoid structure Char;
2006-07-25, by wenzelm
added variant_abs (from term.ML);
2006-07-25, by wenzelm
added find_free (from term.ML);
2006-07-25, by wenzelm
added is/to_ascii_lower/upper;
2006-07-25, by wenzelm
is_funtype: do not export internal operation;
2006-07-25, by wenzelm
tuned;
2006-07-25, by wenzelm
use Term.add_vars instead of obsolete term_varnames;
2006-07-25, by wenzelm
renamed add_term_varnames to Term.add_varnames (cf. Term.add_vars etc.);
2006-07-25, by wenzelm
tuned ML code;
2006-07-25, by wenzelm
renamed Term.variant_abs to Syntax.variant_abs;
2006-07-25, by wenzelm
Drule.merge_rules;
2006-07-25, by wenzelm
renamed Name.give_names to Name.names and moved Name.alphanum to Symbol.alphanum
2006-07-25, by haftmann
improvements for lazy code generation
2006-07-25, by haftmann
fixed typo
2006-07-25, by haftmann
added code generator serialization for Char
2006-07-25, by haftmann
added notes on class_package.ML and codegen_package.ML
2006-07-25, by haftmann
small adjustments
2006-07-23, by haftmann
fixed bug for serialization for uminus on ints
2006-07-23, by haftmann
small improvement in serialization for wfrec
2006-07-23, by haftmann
added structure HOList
2006-07-23, by haftmann
major simplifications for integers
2006-07-23, by haftmann
tactic for prove_instance_arity now gets definition theorems as arguments
2006-07-23, by haftmann
added term_of_string function
2006-07-21, by haftmann
simplification for code generation for Integers
2006-07-21, by haftmann
adaption to argument change in primrec_package
2006-07-21, by haftmann
adaption to changes in class_package
2006-07-21, by haftmann
hooks now take string list as arguments (mutual datatypes); some nice combinators in datatype_codegen
2006-07-21, by haftmann
exported equation transformator
2006-07-21, by haftmann
class package and codegen refinements
2006-07-21, by haftmann
added give_names and alphanum
2006-07-21, by haftmann
Some cases in "case ... of ..." expressions may now
2006-07-21, by berghofe
- Added new "undefined" constant
2006-07-21, by berghofe
removed Variable.monomorphic;
2006-07-20, by wenzelm
comments fixed, member function renamed
2006-07-20, by webertj
Change to algebra method.
2006-07-19, by ballarin
Reimplemented algebra method; now controlled by attribute.
2006-07-19, by ballarin
Strict dfs traversal of imported and registered identifiers.
2006-07-19, by ballarin
added map_default, internal restructuring
2006-07-19, by haftmann
export is_tid;
2006-07-19, by wenzelm
thm_of_proof: improved generation of variables;
2006-07-19, by wenzelm
Sign.infer_types: Name.context;
2006-07-19, by wenzelm
reorganize declarations (more efficient);
2006-07-19, by wenzelm
Name.context for used'';
2006-07-19, by wenzelm
added variant_frees;
2006-07-19, by wenzelm
tuned;
2006-07-19, by wenzelm
export make_context, is_declared;
2006-07-19, by wenzelm
prove: Variable.declare_internal (more efficient);
2006-07-19, by wenzelm
add_local: simplified interface, all frees are known'';
2006-07-19, by wenzelm
Sign.infer_types: Name.context;
2006-07-19, by wenzelm
renamed Variable.rename_wrt to Variable.variant_frees;
2006-07-19, by wenzelm
Fixed the bugs introduced by the last commit! Output is now *identical* to that
2006-07-19, by paulson
MiniSat proof trace format changed; MiniSat is now expected to produce a proof also for "trivial" problems
2006-07-19, by webertj
thm_of_proof: tuned Name operations;
2006-07-18, by wenzelm
print_statement: tuned Variable operations;
2006-07-18, by wenzelm
added newly_fixed, focus;
2006-07-18, by wenzelm
added declare_term_names;
2006-07-18, by wenzelm
fold_proof_terms: canonical arguments;
2006-07-18, by wenzelm
Term.declare_term_names;
2006-07-18, by wenzelm
Started implementing uniqueness proof for recursion
2006-07-18, by berghofe
typo (theorerms) fixed
2006-07-18, by webertj
typo (theorerms) fixed
2006-07-18, by webertj
AList.join now with 'DUP' exception
2006-07-18, by haftmann
added Table.map_default
2006-07-18, by haftmann
removed obsolete ML files;
2006-07-18, by wenzelm
replaced butlast by Library.split_last;
2006-07-17, by wenzelm
replaced butlast by Library.split_last;
2006-07-17, by wenzelm
butlast removed (use fst o split_last instead)
2006-07-17, by webertj
support for MiniSat proof traces added
2006-07-17, by webertj
support for MiniSat proof traces added
2006-07-17, by webertj
has_consts renamed to has_conn, now actually parses the first-order formula
2006-07-16, by paulson
function butlast added
2006-07-15, by webertj
Replaced a-lists by tables to improve efficiency
2006-07-15, by paulson
Pass user lemmas' names to ResHolClause.tptp_write_file and dfg_write_file.
2006-07-15, by mengj
Only include combinators if required by goals and user specified lemmas.
2006-07-15, by mengj
Term.term_lpo takes order on terms rather than strings as argument.
2006-07-14, by ballarin
keep/transaction: unified execution model (with debugging etc.);
2006-07-14, by wenzelm
trivial whitespace changes
2006-07-14, by webertj
simp method: depth_limit;
2006-07-14, by wenzelm
"conjecture" must be lower case
2006-07-13, by paulson
tuned insert_list;
2006-07-13, by wenzelm
Name.context already declares empty names;
2006-07-13, by wenzelm
strip_abs_eta: proper use of Name.context;
2006-07-13, by wenzelm
do not export make_context;
2006-07-13, by wenzelm
removed colon from sym category;
2006-07-13, by wenzelm
fix to refl_clause_aux: added occurs check
2006-07-13, by paulson
* Isar: ":" (colon) is no longer a symbolic identifier character;
2006-07-12, by wenzelm
removed duplicate of Tactic.make_elim_preserve;
2006-07-12, by wenzelm
removed obsolete adhoc_freeze_vars (may use Variable.import_terms instead);
2006-07-12, by wenzelm
exported make_elim_preserve;
2006-07-12, by wenzelm
prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars;
2006-07-12, by wenzelm
simplified prove_conv;
2006-07-12, by wenzelm
removed ':' from category of symbolic identifier chars;
2006-07-12, by wenzelm
query/bang_colon: separate tokens;
2006-07-12, by wenzelm
purged website sources
2006-07-12, by haftmann
added strip_abs_eta
2006-07-12, by haftmann
added chop_prefix
2006-07-12, by haftmann
class_of_param instead of class_of
2006-07-12, by haftmann
adaptions in class_package
2006-07-12, by haftmann
adaptions in codegen
2006-07-12, by haftmann
variants: special treatment of empty name;
2006-07-12, by wenzelm
avoid reference to internal skolem;
2006-07-11, by wenzelm
separate names filed (covers fixes/defaults);
2006-07-11, by wenzelm
adapted Name.defaults_of;
2006-07-11, by wenzelm
removed obsolete xless;
2006-07-11, by wenzelm
clean: no special treatment of empty name;
2006-07-11, by wenzelm
removed obsolete xless;
2006-07-11, by wenzelm
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
2006-07-11, by webertj
uniform treatment of num/xnum;
2006-07-11, by wenzelm
replaced read_radixint by read_intinf;
2006-07-11, by wenzelm
removed str_to_int in favour of general Syntax.read_xnum;
2006-07-11, by wenzelm
num/xnum: bin or hex;
2006-07-11, by wenzelm
Name.internal;
2006-07-11, by wenzelm
tuned;
2006-07-11, by wenzelm
* Pure: structure Name;
2006-07-11, by wenzelm
Names of basic logical entities (variables etc.).
2006-07-11, by wenzelm
replaced Term.variant(list) by Name.variant(_list);
2006-07-11, by wenzelm
Name.internal;
2006-07-11, by wenzelm
adapted to more efficient Name/Variable implementation;
2006-07-11, by wenzelm
replaced Term.variant(list) by Name.variant(_list);
2006-07-11, by wenzelm
maintain Name.context for fixes/defaults;
2006-07-11, by wenzelm
removed obsolete mem_ix;
2006-07-11, by wenzelm
removed obsolete ins_ix, mem_ix, ins_term, mem_term;
2006-07-11, by wenzelm
Name.dest_skolem;
2006-07-11, by wenzelm
Name.bound;
2006-07-11, by wenzelm
replaced Term.variant(list) by Name.variant(_list);
2006-07-11, by wenzelm
replaced Term.variant(list) by Name.variant(_list);
2006-07-11, by wenzelm
replaced Term.variant(list) by Name.variant(_list);
2006-07-11, by wenzelm
Name.invent_list;
2006-07-11, by wenzelm
added name.ML;
2006-07-11, by wenzelm
Name.is_bound;
2006-07-11, by wenzelm
removed obsolete mem_term;
2006-07-11, by wenzelm
Name.internal;
2006-07-11, by wenzelm
replaced Term.variant(list) by Name.variant(_list);
2006-07-11, by wenzelm
let_simproc: activate Variable.import;
2006-07-11, by wenzelm
Witness theorems of interpretations now transfered to current theory.
2006-07-11, by ballarin
New function transfer_witness lifting Thm.transfer to witnesses.
2006-07-11, by ballarin
hex and binary numerals (contributed by Rafal Kolanski)
2006-07-11, by kleing
minor optimization wrt. certifying terms
2006-07-10, by webertj
tuned;
2006-07-08, by wenzelm
tuned;
2006-07-08, by wenzelm
updated;
2006-07-08, by wenzelm
tuned interface;
2006-07-08, by wenzelm
tuned interface;
2006-07-08, by wenzelm
removed dead code;
2006-07-08, by wenzelm
Element.prove_witness: context;
2006-07-08, by wenzelm
prove_witness: context;
2006-07-08, by wenzelm
tuned exception handling;
2006-07-08, by wenzelm
prove/prove_multi: context;
2006-07-08, by wenzelm
simprocs: no theory argument -- use simpset context instead;
2006-07-08, by wenzelm
distinct simproc/simpset: proper context;
2006-07-08, by wenzelm
presburger_ss: proper context;
2006-07-08, by wenzelm
presburger_ss: proper context;
2006-07-08, by wenzelm
tuned;
2006-07-08, by wenzelm
avoid Force_tac, which uses a different context;
2006-07-08, by wenzelm
Goal.prove: context;
2006-07-08, by wenzelm
tactic/method simpset: maintain proper context;
2006-07-08, by wenzelm
Goal.prove_global;
2006-07-08, by wenzelm
Goal.prove_global;
2006-07-08, by wenzelm
simprocs: no theory argument -- use simpset context instead;
2006-07-08, by wenzelm
simprocs: no theory argument -- use simpset context instead;
2006-07-08, by wenzelm
updated;
2006-07-08, by wenzelm
updated Goal.prove, Goal.prove_global;
2006-07-08, by wenzelm
added some bits on variables;
2006-07-08, by wenzelm
* Pure: structure Variable provides operations for proper treatment of fixed/schematic variables;
2006-07-08, by wenzelm
"solver" reference added to make the SAT solver configurable
2006-07-07, by webertj
Some tidying.
2006-07-07, by paulson
Fixed erroneous check-in.
2006-07-07, by ballarin
made evaluation_conv and normalization_conv visible.
2006-07-07, by nipkow
Internal restructuring: identify no longer computes syntax.
2006-07-07, by ballarin
Modified comment.
2006-07-07, by ballarin
added support for MiniSat 1.14
2006-07-07, by webertj
removed obsolete locale view;
2006-07-06, by wenzelm
apply_text: support Method.Source_i;
2006-07-06, by wenzelm
added method_i and Source_i;
2006-07-06, by wenzelm
less
more
|
(0)
-10000
-3000
-1000
-240
+240
+1000
+3000
+10000
+30000
tip