Mercurial
Mercurial
>
repos
>
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
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.
prefer first constant component on merge
2007-10-15, by haftmann
explicit parameter for class finite
2007-10-15, by haftmann
tuned comment;
2007-10-15, by wenzelm
more on authentic syntax;
2007-10-15, by wenzelm
updated method "ferrack";
2007-10-15, by wenzelm
interpreter for List.append added again
2007-10-15, by webertj
quick_and_dirty (again) not touched anymore
2007-10-15, by webertj
require_thy: read_text *after* checking parents
2007-10-14, by wenzelm
gen_add_inductive_i: treat abbrevs as local defs, expand by export;
2007-10-14, by wenzelm
tuned various Class interfaces;
2007-10-14, by wenzelm
removed obsolete Class.class_of_locale/locale_of_class;
2007-10-14, by wenzelm
tuned;
2007-10-14, by wenzelm
added add_def;
2007-10-14, by wenzelm
added is_class;
2007-10-14, by wenzelm
PolyML.Compiler.maxInlineSize := 80;
2007-10-13, by wenzelm
abbrev: return hypothetical def;
2007-10-13, by wenzelm
renamed def to define;
2007-10-13, by wenzelm
(un)overload: full rewrite;
2007-10-13, by wenzelm
add_abbrevs: unvarify result;
2007-10-13, by wenzelm
replaced obsolete Theory.add_finals_i by Theory.add_deps;
2007-10-13, by wenzelm
Theory.specify_const: added deps argument;
2007-10-13, by wenzelm
renamed LocalTheory.def to LocalTheory.define;
2007-10-13, by wenzelm
typo in comment fixed
2007-10-12, by webertj
significant code overhaul, bugfix for inductive data types
2007-10-12, by webertj
added generic provide_file;
2007-10-12, by wenzelm
pass explicit target record -- more informative peek operation;
2007-10-12, by wenzelm
more informative TheoryTarget.peek operation;
2007-10-12, by wenzelm
fork_mixfix: explicit bool argument;
2007-10-12, by wenzelm
eval_term: moved actual evaluation out of CRITICAL section;
2007-10-12, by wenzelm
preventing eta-redexes in theorems from causing failure
2007-10-12, by paulson
trying to make it run faster
2007-10-12, by paulson
calling the correct interface
2007-10-12, by paulson
replaced syntax/translations by abbreviation;
2007-10-12, by wenzelm
updated
2007-10-12, by haftmann
dropped local_syntax
2007-10-12, by haftmann
tuned
2007-10-12, by haftmann
(intermediate quickfix)
2007-10-12, by haftmann
removed
2007-10-12, by haftmann
added
2007-10-12, by haftmann
metis calls
2007-10-12, by paulson
updated
2007-10-12, by haftmann
moved class power to theory Power
2007-10-12, by haftmann
refined; moved class power to theory Power
2007-10-12, by haftmann
consolidated naming conventions for code generator theories
2007-10-12, by haftmann
class div inherits from class times
2007-10-12, by haftmann
code_include replaces code_moduleprolog
2007-10-12, by haftmann
added subclass command
2007-10-12, by haftmann
enabled Refute_Examples again;
2007-10-11, by wenzelm
local_axioms: impose hyps stemming from local consts as well
2007-10-11, by wenzelm
disabled Refute_Examples temporarily;
2007-10-11, by wenzelm
local_theory: incorporated consts into axioms;
2007-10-11, by wenzelm
removed unused/impure quiet_mode;
2007-10-11, by wenzelm
added export_cterm;
2007-10-11, by wenzelm
local_theory: incorporated consts into axioms;
2007-10-11, by wenzelm
replaced Term.equiv_types by Type.similar_types;
2007-10-11, by wenzelm
replaced Term.equiv_types by Type.similar_types;
2007-10-11, by wenzelm
dest/cert_def: replaced Pretty.pp by explicit Proof.context;
2007-10-11, by wenzelm
added elim_implies (more convenient argument order);
2007-10-11, by wenzelm
removed obsolete flip;
2007-10-11, by wenzelm
moved Drule.unvarify to Thm.unvarify (cf. more_thm.ML);
2007-10-11, by wenzelm
replaced (flip Thm.implies_elim) by Thm.elim_implies;
2007-10-11, by wenzelm
moved Drule.unvarify to Thm.unvarify (cf. more_thm.ML);
2007-10-11, by wenzelm
usedir: added HOL_USEDIR_OPTIONS;
2007-10-11, by wenzelm
reconstruction bug fix
2007-10-11, by paulson
tuned;
2007-10-11, by wenzelm
replaced Sign.add_consts_i by Sign.declare_const;
2007-10-11, by wenzelm
replaced Sign.add_consts_authentic by Sign.declare_const;
2007-10-11, by wenzelm
renamed Syntax.XXX_mode to Syntax.mode_XXX;
2007-10-11, by wenzelm
removed obsolete AxClass.params_of_class;
2007-10-11, by wenzelm
replaced Sign.add_consts_authentic by Sign.declare_const;
2007-10-11, by wenzelm
load axclass.ML before Isar;
2007-10-11, by wenzelm
added specify_const;
2007-10-11, by wenzelm
removed obsolete simple_def;
2007-10-11, by wenzelm
moved define_class_params to Isar/class.ML;
2007-10-11, by wenzelm
load axclass.ML before Isar;
2007-10-11, by wenzelm
Theory.specify_const;
2007-10-11, by wenzelm
moved ProofContext.pp to Syntax.pp;
2007-10-11, by wenzelm
renamed Syntax.XXX_mode to Syntax.mode_XXX;
2007-10-11, by wenzelm
replaced Sign.add_consts_authentic by Sign.declare_const;
2007-10-11, by wenzelm
rationalized redundant code
2007-10-11, by paulson
usage: HOL_USEDIR_OPTIONS;
2007-10-11, by wenzelm
failure messages
2007-10-11, by paulson
'notation': allow structmixfix;
2007-10-11, by wenzelm
update_modesyntax: may delete 'structure' notation as well;
2007-10-11, by wenzelm
'notation': allow 'structure' as well;
2007-10-11, by wenzelm
removed redundant strip_vars/abs_eqn, use improved Drule.abs_def instead;
2007-10-10, by wenzelm
replaced add_modesyntax by general update_modesyntax (add or del);
2007-10-10, by wenzelm
added 'no_notation';
2007-10-10, by wenzelm
generalized notation interface (add or del);
2007-10-10, by wenzelm
tuned;
2007-10-10, by wenzelm
improved abs_def: only abstract over outermost (unique) Vars;
2007-10-10, by wenzelm
proper latex antiquotations instead of adhoc escapes;
2007-10-10, by wenzelm
updated;
2007-10-10, by wenzelm
added no_notation;
2007-10-10, by wenzelm
removed dead code
2007-10-10, by paulson
more metis proofs
2007-10-10, by paulson
Prepare proper interface of interpretation_i, interpret_i.
2007-10-10, by ballarin
getting rid of type typ_var
2007-10-10, by paulson
tuned;
2007-10-09, by wenzelm
class: print result is for locale;
2007-10-09, by wenzelm
context-based treatment of generalization; also handling TFrees in axiom clauses
2007-10-09, by paulson
TheoryTarget.init_cmd;
2007-10-09, by wenzelm
removed LocalTheory.defs/target_morphism operations;
2007-10-09, by wenzelm
renamed AxClass.get_definition to AxClass.get_info (again);
2007-10-09, by wenzelm
removed LocalTheory.defs/target_morphism operations;
2007-10-09, by wenzelm
AxClass.axiomatize and Specification: renamed XXX_i to XXX, and XXX to XXX_cmd;
2007-10-09, by wenzelm
removed LocalTheory.defs/target_morphism operations;
2007-10-09, by wenzelm
renamed AxClass.get_definition to AxClass.get_info (again);
2007-10-09, by wenzelm
renamed AxClass.get_definition to AxClass.get_info (again);
2007-10-09, by wenzelm
renamed AxClass.get_definition to AxClass.get_info (again);
2007-10-09, by wenzelm
Specification: renamed XXX_i to XXX, and XXX to XXX_cmd;
2007-10-09, by wenzelm
AxClass.axiomatize: renamed XXX_i to XXX, and XXX to XXX_cmd;
2007-10-09, by wenzelm
removed LocalTheory.defs, use plain LocalTheory.def;
2007-10-09, by wenzelm
tuned;
2007-10-09, by wenzelm
generic Syntax.pretty/string_of operations;
2007-10-09, by wenzelm
generic Syntax.pretty/string_of operations;
2007-10-09, by wenzelm
generic Syntax.pretty/string_of operations;
2007-10-09, by wenzelm
generic Syntax.pretty/string_of operations;
2007-10-09, by wenzelm
updated keywords
2007-10-08, by haftmann
moved translation kernel to CodeThingol
2007-10-08, by haftmann
less
more
|
(0)
-10000
-3000
-1000
-120
+120
+1000
+3000
+10000
+30000
tip