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.
type local_theory;
2006-02-06, by wenzelm
norm_term: Sign.const_expansion, Envir.expand_atom;
2006-02-06, by wenzelm
TableFun: renamed xxx_multi to xxx_list;
2006-02-06, by wenzelm
type local_theory = Proof.context;
2006-02-06, by wenzelm
cert_def: use Logic.dest_def;
2006-02-06, by wenzelm
Toplevel.local_theory;
2006-02-06, by wenzelm
LocalDefs.cert_def;
2006-02-06, by wenzelm
eq_prop: Envir.beta_eta_contract;
2006-02-06, by wenzelm
renamed xxx_multi to xxx_list;
2006-02-06, by wenzelm
moved combound, rlist_abs to logic.ML;
2006-02-06, by wenzelm
union_tpairs: Library.merge;
2006-02-06, by wenzelm
moved no_vars to sign.ML;
2006-02-06, by wenzelm
lambda: abstract over any const;
2006-02-06, by wenzelm
added add_abbrevs(_i);
2006-02-06, by wenzelm
moved (beta_)eta_contract to envir.ML;
2006-02-06, by wenzelm
tuned;
2006-02-06, by wenzelm
added generic dest_def (mostly from theory.ML);
2006-02-06, by wenzelm
added (beta_)eta_contract (from pattern.ML);
2006-02-06, by wenzelm
print_theory: const abbreviations;
2006-02-06, by wenzelm
added abbreviations;
2006-02-06, by wenzelm
load envir.ML and logic.ML early;
2006-02-06, by wenzelm
Logic.rlist_abs;
2006-02-06, by wenzelm
Logic.const_of_class/class_of_const;
2006-02-06, by wenzelm
TableFun: renamed xxx_multi to xxx_list;
2006-02-06, by wenzelm
replaced Symtab.merge_multi by local merge_rules;
2006-02-06, by wenzelm
Envir.(beta_)eta_contract;
2006-02-06, by wenzelm
subsituted gen_duplicates / has_duplicates for duplicates whenever appropriate
2006-02-06, by haftmann
added strip_abs
2006-02-06, by haftmann
clarified semantics of merge
2006-02-06, by haftmann
speedup: use simproc for AC rules
2006-02-04, by huffman
UU_reorient_simproc no longer rewrites UU = numeral
2006-02-04, by huffman
removed obsolete gen_ins/mem;
2006-02-03, by wenzelm
removed add/del_rules;
2006-02-03, by wenzelm
canonical member/insert/merge;
2006-02-03, by wenzelm
removal of case analysis clauses
2006-02-03, by paulson
fix
2006-02-03, by haftmann
minor improvements
2006-02-03, by haftmann
refined signature of locale module
2006-02-03, by haftmann
no toplevel 'thy' anymore
2006-02-03, by haftmann
fix in codegen
2006-02-03, by haftmann
do not open structure;
2006-02-02, by wenzelm
reimplemented using Equiv_Relations.thy
2006-02-02, by huffman
improvement in devarifications
2006-02-02, by haftmann
alternative syntax for instances
2006-02-02, by haftmann
tuned;
2006-02-02, by wenzelm
consumes: negative argument relative to total number of prems;
2006-02-02, by wenzelm
added refine_insert;
2006-02-02, by wenzelm
Proof.refine_insert;
2006-02-02, by wenzelm
always use Attrib.src;
2006-02-02, by wenzelm
more generic type for map_specs/facts;
2006-02-02, by wenzelm
'obtains' element;
2006-02-02, by wenzelm
'obtain': optional case name;
2006-02-02, by wenzelm
index elements;
2006-02-02, by wenzelm
* Isar: 'obtains' element;
2006-02-02, by wenzelm
tuned msg;
2006-02-02, by wenzelm
theorem(_in_locale): Element.statement, Obtain.statement;
2006-02-02, by wenzelm
added parname;
2006-02-02, by wenzelm
obtain(_i): optional name for 'that';
2006-02-02, by wenzelm
tuned comments;
2006-02-02, by wenzelm
moved (general_)statement to outer_parse.ML;
2006-02-02, by wenzelm
added concluding statements: Shows/Obtains;
2006-02-02, by wenzelm
moved specific map_typ/term to sign.ML;
2006-02-02, by wenzelm
added specific map_typ/term (from term.ML);
2006-02-02, by wenzelm
Exporting recdef's hints for use by new recdef package
2006-02-02, by krauss
*_asms_of fixed.
2006-02-02, by ballarin
add 64bit atbroy98 platform
2006-02-02, by kleing
updated;
2006-02-01, by wenzelm
Added "evaluation" method and oracle.
2006-02-01, by berghofe
new and updated protocol proofs by Giamp Bella
2006-02-01, by paulson
substantial cleanup and simplifications
2006-02-01, by haftmann
name clarifications
2006-02-01, by haftmann
added map_entry_yield
2006-02-01, by haftmann
- renamed some lemmas (some had names coming from ancient
2006-02-01, by urbanc
added all constructors from PhD
2006-02-01, by urbanc
axiomatization: retrict parameters to occurrences in specs;
2006-01-31, by wenzelm
improved comments;
2006-01-31, by wenzelm
tuned LocalDefs.unfold;
2006-01-31, by wenzelm
(un)fold: removed '(raw)' option;
2006-01-31, by wenzelm
added consts_retricted;
2006-01-31, by wenzelm
(un)fold: no raw flag;
2006-01-31, by wenzelm
tuned;
2006-01-31, by wenzelm
tuned LocalTheory.pretty_consts;
2006-01-31, by wenzelm
(un)folded: removed '(raw)' option;
2006-01-31, by wenzelm
lambda: abstract over TYPE argument, too;
2006-01-31, by wenzelm
tuned comments;
2006-01-31, by wenzelm
removal of ResClause.num_of_clauses and other simplifications
2006-01-31, by paulson
working SPASS support; much tidying
2006-01-31, by paulson
added serialization for arbitrary
2006-01-31, by haftmann
minor change to CodegenPackage interface
2006-01-31, by haftmann
minor cleanups
2006-01-31, by haftmann
more coherent lookup extraction functions
2006-01-31, by haftmann
reorganization of code to support DFG otuput
2006-01-31, by paulson
* Pure: 'advanced' translation functions use Context.generic instead of just theory;
2006-01-31, by wenzelm
declare defn rules;
2006-01-31, by wenzelm
all styles now reset to defaults first, i.e. the document may switch styles back and forth;
2006-01-31, by wenzelm
export meta_rewrite_rule;
2006-01-31, by wenzelm
advanced translations: Context.generic;
2006-01-31, by wenzelm
advanced translations: Context.generic;
2006-01-31, by wenzelm
tidy-up of res_clause.ML, removing the "predicates" field
2006-01-30, by paulson
'setup': no list type, support implicit setup;
2006-01-30, by wenzelm
'fixes': support plain vars;
2006-01-30, by wenzelm
fixed a syntax error!
2006-01-30, by paulson
replaced gen_list by enum
2006-01-30, by haftmann
adaptions to codegen_package
2006-01-30, by haftmann
various improvements
2006-01-30, by haftmann
added three times overloaded Isar instance command
2006-01-30, by haftmann
moved instance Isar command to class_package.ML
2006-01-30, by haftmann
added map_atype, map_aterms
2006-01-30, by haftmann
tuned proof;
2006-01-29, by wenzelm
declare atomize/defn for Ball;
2006-01-29, by wenzelm
invent_fixes: merely enter body temporarily;
2006-01-29, by wenzelm
'unfolding': LocalDefs.unfold;
2006-01-29, by wenzelm
moved treatment of object-logic equalities to local_defs.ML;
2006-01-29, by wenzelm
method (un)folded: option '(raw)';
2006-01-29, by wenzelm
added attributes defn_add/del;
2006-01-29, by wenzelm
added 'defn' attribute;
2006-01-29, by wenzelm
proper order of trfuns;
2006-01-29, by wenzelm
CPure: Context.add_setup;
2006-01-29, by wenzelm
tuned proofs;
2006-01-29, by wenzelm
implicit setup;
2006-01-29, by wenzelm
default rule step: norm_hhf_tac;
2006-01-29, by wenzelm
tuned comment;
2006-01-29, by wenzelm
declare 'defn' rules;
2006-01-29, by wenzelm
LocalDefs;
2006-01-28, by wenzelm
Basic operations on local definitions.
2006-01-28, by wenzelm
removed unnecessary Syntax.fix_mixfix;
2006-01-28, by wenzelm
added axiomatization_loc, definition_loc;
2006-01-28, by wenzelm
moved local defs to local_defs.ML;
2006-01-28, by wenzelm
LocalDefs;
2006-01-28, by wenzelm
removed unatomize;
2006-01-28, by wenzelm
(un)fold: support object-level rewrites;
2006-01-28, by wenzelm
added print_consts;
2006-01-28, by wenzelm
removed obsolete keyword 'files';
2006-01-28, by wenzelm
(un)folded: support object-level rewrites;
2006-01-28, by wenzelm
added equals_cong;
2006-01-28, by wenzelm
added Isar/local_defs.ML;
2006-01-28, by wenzelm
LocalDefs.add_def;
2006-01-28, by wenzelm
LocalDefs.def_export;
2006-01-28, by wenzelm
tuned proofs;
2006-01-28, by wenzelm
Pure/Isar: (un)folded, (un)fold, unfolding support
2006-01-28, by wenzelm
interrupt_timeout for Poly replaced by stub
2006-01-27, by webertj
added atomize_iff;
2006-01-27, by wenzelm
renamed Pretty.gen_list to Pretty.enum;
2006-01-27, by wenzelm
swapped theory_context;
2006-01-27, by wenzelm
swapped Toplevel.theory_context;
2006-01-27, by wenzelm
added invent_fixes;
2006-01-27, by wenzelm
swapped Toplevel.theory_context;
2006-01-27, by wenzelm
renamed reverse_atomize to unatomize;
2006-01-27, by wenzelm
init: include view;
2006-01-27, by wenzelm
improved 'notes', including proper treatment of locale results;
2006-01-27, by wenzelm
swapped Toplevel.theory_context;
2006-01-27, by wenzelm
Locale.init;
2006-01-27, by wenzelm
renamed gen_list to enum;
2006-01-27, by wenzelm
moved theorem tags from Drule to PureThy;
2006-01-27, by wenzelm
added ProofContext.pprint_context (depends on ProofContext.debug);
2006-01-27, by wenzelm
moved theorem tags from Drule to PureThy;
2006-01-27, by wenzelm
tidying up SPASS output
2006-01-27, by paulson
tidying
2006-01-27, by paulson
better reporting
2006-01-27, by paulson
Interface to access the specification of a named locale.
2006-01-27, by ballarin
Added new file Tools/ATP/reduce_axiomsN.ML
2006-01-27, by mengj
Added in new file Tools/ATP/reduce_axiomsN.ML
2006-01-27, by mengj
Changed codes that call relevance filter.
2006-01-27, by mengj
Relevance filtering. Has replaced the previous version.
2006-01-27, by mengj
interrupt_timeout now raises Interrupt instead of SML90.Interrupt
2006-01-26, by webertj
smaller example to prevent timeout
2006-01-26, by webertj
Fixed bug in code generator for primitive definitions that
2006-01-26, by berghofe
Inductive sets with no introduction rules are now allowed as well.
2006-01-26, by berghofe
added definition(_i);
2006-01-25, by wenzelm
renamed export to export_standard (again!), because it includes Drule.local_standard';
2006-01-25, by wenzelm
ProofContext.export_standard;
2006-01-25, by wenzelm
tuned atomize_cterm;
2006-01-25, by wenzelm
turned abstract_term into ProofContext.abs_def;
2006-01-25, by wenzelm
added constant definition;
2006-01-25, by wenzelm
added 'definition';
2006-01-25, by wenzelm
tuned comment;
2006-01-25, by wenzelm
export name_multi;
2006-01-25, by wenzelm
abs_def: improved error;
2006-01-25, by wenzelm
ObjectLogic.atomize_cterm;
2006-01-25, by wenzelm
updated;
2006-01-25, by wenzelm
works with DPLL solver now
2006-01-24, by webertj
the additional freshness-condition in the one-induction
2006-01-24, by urbanc
fixed code_generate syntax;
2006-01-24, by wenzelm
renamed axiomatize(_i) to axiomatization(_i);
2006-01-24, by wenzelm
renamed inferred_type to inferred_param;
2006-01-24, by wenzelm
ProofContext.inferred_param;
2006-01-24, by wenzelm
removed the_params;
2006-01-24, by wenzelm
added actual operations;
2006-01-24, by wenzelm
axiomatization: optional vars;
2006-01-24, by wenzelm
LocalTheory.pretty_consts;
2006-01-24, by wenzelm
tuned;
2006-01-24, by wenzelm
add_finals: prep_consts, i.e. varify type;
2006-01-24, by wenzelm
added dest_all;
2006-01-24, by wenzelm
TimeLimit replaced by interrupt_timeout
2006-01-23, by webertj
TimeLimit replaced by interrupt_timeout
2006-01-23, by webertj
Updated to Isabelle 2006-01-23
2006-01-23, by krauss
made change for ex1
2006-01-23, by urbanc
removed problematic keyword 'atom'
2006-01-23, by haftmann
more general serializer
2006-01-23, by haftmann
slight steps forward
2006-01-23, by haftmann
exported after_qed for axclass instance
2006-01-23, by haftmann
ResClasimp.get_clasimp_lemmas now takes all subgoals rather than only the first
2006-01-23, by paulson
Clausification now handles some IFs in rewrite rules (if-split did not work)
2006-01-23, by paulson
bugfix: induct_tac no longer raises THM "dest_state"
2006-01-23, by paulson
fixed the <<= notation
2006-01-23, by paulson
replacement of bool by a datatype (making problems first-order). More lemma names
2006-01-23, by paulson
Fixed a bug.
2006-01-23, by mengj
no essential changes
2006-01-22, by urbanc
made the change for setup-functions not returning functions
2006-01-22, by urbanc
a fixme comments about abs_fun_if, which should be called perm_if
2006-01-22, by urbanc
Local theory operations, with optional target locale.
2006-01-22, by wenzelm
added restore_body;
2006-01-22, by wenzelm
added the_params;
2006-01-22, by wenzelm
tuned order;
2006-01-22, by wenzelm
added Isar/local_theory.ML;
2006-01-22, by wenzelm
Ensure dereference is delayed.
2006-01-21, by mengj
tuned;
2006-01-21, by wenzelm
* ML: simplified type attribute;
2006-01-21, by wenzelm
simplified type attribute;
2006-01-21, by wenzelm
removed duplicate type_solver (cf. Tools/typechk.ML);
2006-01-21, by wenzelm
simplified type attribute;
2006-01-21, by wenzelm
simplified type attribute;
2006-01-21, by wenzelm
simplified type attribute;
2006-01-21, by wenzelm
rename map_theory/proof to theory/proof_map;
2006-01-21, by wenzelm
tuned proofs;
2006-01-21, by wenzelm
simplified type attribute;
2006-01-21, by wenzelm
simplified type attribute;
2006-01-21, by wenzelm
type information is now also printed.
2006-01-20, by mengj
added some debugging code.
2006-01-20, by mengj
fixed a bug
2006-01-20, by mengj
quote "atom";
2006-01-19, by wenzelm
updated;
2006-01-19, by wenzelm
* ML/Isar: theory setup has type (theory -> theory);
2006-01-19, by wenzelm
use/use_thy: Output.toplevel_errors;
2006-01-19, by wenzelm
added basic syntax;
2006-01-19, by wenzelm
moved pure syntax to Syntax/syntax.ML and pure_thy.ML;
2006-01-19, by wenzelm
keep: disable Output.toplevel_errors;
2006-01-19, by wenzelm
run_thy: removed Output.toplevel_errors;
2006-01-19, by wenzelm
added ML_errors;
2006-01-19, by wenzelm
use: Output.ML_errors;
2006-01-19, by wenzelm
less
more
|
(0)
-10000
-3000
-1000
-240
+240
+1000
+3000
+10000
+30000
tip