Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-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.
use Attrib.add_del_args;
2000-03-31, by wenzelm
added add_del_args;
2000-03-31, by wenzelm
fixed goal syntax;
2000-03-31, by wenzelm
comments modified
2000-03-31, by nipkow
tuned
2000-03-31, by kleing
included new stanford mirror, mirror links now point to source directly
2000-03-31, by kleing
updated recdef
2000-03-31, by nipkow
tuned;
2000-03-30, by wenzelm
recdef
2000-03-30, by nipkow
If all termination conditions are proved automatically,
2000-03-30, by nipkow
recdef.rules -> recdef.simps
2000-03-30, by nipkow
mod in recdef allows to access the correct simpset via simpset().
2000-03-30, by nipkow
the simplification rules returned from TFL are now paired with the row they
2000-03-30, by nipkow
* Isar/Pure: local results and corresponding term bindings are now
2000-03-30, by wenzelm
support Hindley-Milner polymorphisms in results and bindings;
2000-03-30, by wenzelm
added 'moreover' and 'ultimately';
2000-03-30, by wenzelm
added \MOREOVER, \ULTIMATELY;
2000-03-30, by wenzelm
support Hindley-Milner polymorphisms in binds and facts;
2000-03-30, by wenzelm
support Hindley-Milner polymorphisms in binds and facts;
2000-03-30, by wenzelm
let_bind(_i): polymorphic version;
2000-03-30, by wenzelm
ProofContext.find_free;
2000-03-30, by wenzelm
'tactic': refer to PureIsar structure;
2000-03-30, by wenzelm
?this: support params;
2000-03-30, by wenzelm
support polymorphic Vars;
2000-03-30, by wenzelm
tuned;
2000-03-30, by wenzelm
foldl_term_types: depend on term as well;
2000-03-30, by wenzelm
read_def_cterms: use Sign.read_def_terms;
2000-03-30, by wenzelm
read_def_terms (no certify yet);
2000-03-30, by wenzelm
export update_multi;
2000-03-30, by wenzelm
added tvars_intr_list;
2000-03-30, by wenzelm
*** empty log message ***
2000-03-29, by nipkow
*** empty log message ***
2000-03-29, by nipkow
mods because of weak_case_cong -> removed Action.ML twice
2000-03-28, by nipkow
added weak_case_cong feature
2000-03-28, by nipkow
mods because of weak_case_cong
2000-03-28, by nipkow
fixed railqtoken;
2000-03-28, by wenzelm
-I option;
2000-03-28, by wenzelm
renamed 'hoare_vcg' to 'hoare';
2000-03-27, by wenzelm
tuned;
2000-03-27, by wenzelm
fixed dddot_tr;
2000-03-27, by wenzelm
rail token vs. terminal;
2000-03-27, by wenzelm
fixed term syntax;
2000-03-27, by wenzelm
tail token vs. terminal;
2000-03-27, by wenzelm
fixed \rail@tokenfont (ever used?);
2000-03-27, by wenzelm
added an order-sorted version of quickSort
2000-03-27, by paulson
simplified constant "colored"
2000-03-27, by paulson
added 'ultimately';
2000-03-26, by wenzelm
added WhileRule';
2000-03-26, by wenzelm
made SML/NJ happy;
2000-03-26, by wenzelm
tuned presentation;
2000-03-26, by wenzelm
tuned;
2000-03-26, by wenzelm
ignore_stuff;
2000-03-26, by wenzelm
tuned output;
2000-03-26, by wenzelm
!!!! = cut "Corrupted outer syntax in presentation";
2000-03-26, by wenzelm
added is_begin/end_ignore;
2000-03-26, by wenzelm
tuned targets;
2000-03-26, by wenzelm
tuned;
2000-03-25, by wenzelm
improved (anti)quote_tr(');
2000-03-25, by wenzelm
addsimprocs [record_simproc];
2000-03-25, by wenzelm
tuned antiquote_tr';
2000-03-25, by wenzelm
export updateN;
2000-03-25, by wenzelm
use abstract syntax;
2000-03-24, by wenzelm
plain ASCII;
2000-03-24, by wenzelm
arith method: HEADGOAL;
2000-03-24, by wenzelm
HOL/ex/Multiquote;
2000-03-24, by wenzelm
added HOL/ex/Multiquote.thy;
2000-03-24, by wenzelm
tuned;
2000-03-24, by wenzelm
usedir -D: update styles as well;
2000-03-24, by wenzelm
usedir -D: update styles;
2000-03-24, by wenzelm
improved dump of styles;
2000-03-24, by wenzelm
-o sty;
2000-03-24, by wenzelm
comments
2000-03-24, by nipkow
added 'moreover' command;
2000-03-23, by wenzelm
tuned output;
2000-03-23, by wenzelm
tuned spacing;
2000-03-23, by wenzelm
ex/Antiquote.thy made new-style theory;
2000-03-23, by wenzelm
now exclusively uses rtac/dtac/etac rather than the long forms
2000-03-23, by paulson
restored the MESON examples file HOL/ex/mesontest2.ML
2000-03-23, by paulson
made a proof more robust (did not like Suc_less_eq)
2000-03-22, by paulson
Suc_less_eq now with AddIffs. How could this have been overlooked?
2000-03-22, by paulson
combined finite_Int1/2 as finite_Int. Deleted the awful "lemma" from the
2000-03-22, by paulson
made more robust
2000-03-22, by paulson
tidied using new "inst" rule
2000-03-22, by paulson
tidied using new "inst" rule
2000-03-22, by paulson
new meta-rule "inst", a shorthand for read_instantiate_sg
2000-03-22, by paulson
goal_spec: [!];
2000-03-21, by wenzelm
tuned;
2000-03-21, by wenzelm
tuned;
2000-03-21, by wenzelm
tuned;
2000-03-21, by wenzelm
tuned comment;
2000-03-21, by wenzelm
help message;
2000-03-21, by wenzelm
handle general case: params and hyps of thesis;
2000-03-21, by wenzelm
soft_asm_tac: hack to norm goal;
2000-03-21, by wenzelm
proof methods: 'case_tac' / 'induct_tac';
2000-03-20, by wenzelm
tuned degenerate cases / induct;
2000-03-20, by wenzelm
added prove_goalw_cterm;
2000-03-20, by wenzelm
quick_and_dirty moved to Isar/skip_proof.ML;
2000-03-20, by wenzelm
use Args.goal_spec;
2000-03-20, by wenzelm
goal_spec;
2000-03-20, by wenzelm
ALLGOALS_RANGE superceded by Seq.INTERVAL;
2000-03-20, by wenzelm
improved support for emulating tactic scripts;
2000-03-20, by wenzelm
res_inst_tac etc.;
2000-03-20, by wenzelm
goalspec;
2000-03-20, by wenzelm
case_tac, induct_tac;
2000-03-20, by wenzelm
tactic emulation;
2000-03-20, by wenzelm
tidied
2000-03-20, by paulson
the perm_rules variable is no longer needed
2000-03-20, by paulson
tidied
2000-03-20, by paulson
replaced best_tac by force_tac, allowing some arithmetic reasoning
2000-03-20, by paulson
renamed a variable to avoid possible free/bound confusion
2000-03-20, by paulson
a possibly (?) more perspicous simprule in the "simpset" part
2000-03-20, by paulson
now based on "Main", as it should be
2000-03-20, by paulson
deleted unnecessary "simpset" part from recdef
2000-03-20, by paulson
'oops' made proper;
2000-03-18, by wenzelm
intro_classes_tac: REPEAT_ALL_NEW;
2000-03-18, by wenzelm
tuned comments;
2000-03-18, by wenzelm
tuned;
2000-03-18, by wenzelm
obtain;
2000-03-18, by wenzelm
simplified setup;
2000-03-18, by wenzelm
pure methods / atts moved here;
2000-03-18, by wenzelm
tuned;
2000-03-18, by wenzelm
obtain;
2000-03-18, by wenzelm
parskip 0pt;
2000-03-17, by wenzelm
tuned;
2000-03-17, by wenzelm
fixed theory, context typing;
2000-03-17, by wenzelm
tuned;
2000-03-17, by wenzelm
simplified Proof General setup;
2000-03-17, by wenzelm
untag: only name arg;
2000-03-17, by wenzelm
arith: "!" arg;
2000-03-17, by wenzelm
x-symbol;
2000-03-17, by wenzelm
fixed \OBTAIN;
2000-03-17, by wenzelm
fixed dep;
2000-03-17, by wenzelm
arith method: bang arg;
2000-03-17, by wenzelm
\isamarkupheader: \section;
2000-03-17, by wenzelm
generic "kill" command;
2000-03-17, by wenzelm
old_symbol_source: include header;
2000-03-17, by wenzelm
kill: include kill_proof;
2000-03-17, by wenzelm
fixed untag;
2000-03-17, by wenzelm
untag: remove all tags of given name;
2000-03-17, by wenzelm
no begin_goal marker (interferes with "latex" etc. output; useless anyway?)
2000-03-17, by wenzelm
next_block: allow in non-goal blocks as well (experimental);
2000-03-17, by wenzelm
re-ordered the theorems
2000-03-17, by paulson
better error messages, especially for multiple types
2000-03-17, by paulson
Splitter support;
2000-03-16, by wenzelm
added HOL/PreLIst.thy;
2000-03-16, by wenzelm
tuned;
2000-03-16, by wenzelm
do not change parindent/parskip;
2000-03-16, by wenzelm
Isar: splitter support; improved diagnostics;
2000-03-16, by wenzelm
Splitter support;
2000-03-16, by wenzelm
moved "cases" to generic.tex;
2000-03-16, by wenzelm
tuned;
2000-03-16, by wenzelm
Named local contexts (cases);
2000-03-16, by wenzelm
Added setup for primrec theory data.
2000-03-15, by berghofe
get_recdef now returns None instead of raising ERROR.
2000-03-15, by berghofe
Added new theory data slot for primrec equations.
2000-03-15, by berghofe
Now returns theorems with correct names in derivations.
2000-03-15, by berghofe
Eliminated store_clasimp.
2000-03-15, by berghofe
- Fixed bug in prove_casedist_thms (proof failed because of
2000-03-15, by berghofe
made SML/XL happy;
2000-03-15, by wenzelm
## -D document;
2000-03-15, by wenzelm
renamed isabelle env;
2000-03-15, by wenzelm
splitter setup;
2000-03-15, by wenzelm
clasimp: include Splitter;
2000-03-15, by wenzelm
splitter setup;
2000-03-15, by wenzelm
tuned comments;
2000-03-15, by wenzelm
include Splitter.split_modifiers;
2000-03-15, by wenzelm
added attributes, method modifiers, theory setup;
2000-03-15, by wenzelm
export change_global_ss, change_local_ss;
2000-03-15, by wenzelm
removed export_chain;
2000-03-15, by wenzelm
eliminated toplevel stack;
2000-03-15, by wenzelm
'pr': modes, optional limit;
2000-03-15, by wenzelm
pr: modes, optional limit;
2000-03-15, by wenzelm
pretty chunks;
2000-03-15, by wenzelm
tuned comment;
2000-03-15, by wenzelm
tuned comments;
2000-03-15, by wenzelm
added pretty_goals(_marker);
2000-03-15, by wenzelm
removed Pretty.spc;
2000-03-15, by wenzelm
use Pretty.str / Pretty.raw_str;
2000-03-15, by wenzelm
removed lst, strlen, strlen_real, spc, sym;
2000-03-15, by wenzelm
made links to homepages absolute, avoids trouble with relative links on the
2000-03-15, by kleing
'undo' prints state (again);
2000-03-14, by wenzelm
pr, disable_pr, enable_pr;
2000-03-14, by wenzelm
silence undo command;
2000-03-14, by wenzelm
tuned comments;
2000-03-14, by wenzelm
invoke_case: include attributes;
2000-03-14, by wenzelm
'cases' and 'induct' methods;
2000-03-14, by wenzelm
tuned 'case';
2000-03-14, by wenzelm
added 'case' command;
2000-03-14, by wenzelm
added \NEXT;
2000-03-14, by wenzelm
proper symbol_output for "xsymbols" mode;
2000-03-13, by wenzelm
replaced exhaust_tac by case_tac;
2000-03-13, by wenzelm
renamed cases_tac to case_tac;
2000-03-13, by wenzelm
case_tac now subsumes both boolean and datatype cases;
2000-03-13, by wenzelm
use cases;
2000-03-13, by wenzelm
* HOL: exhaust_tac on datatypes superceded by new case_tac;
2000-03-13, by wenzelm
renamed cases_tac to case_tac;
2000-03-13, by wenzelm
adapted to new PureThy.add_thms etc.;
2000-03-13, by wenzelm
removed cases_of;
2000-03-13, by wenzelm
adapted to new PureThy.add_thms etc.;
2000-03-13, by wenzelm
adapted to new PureThy.add_thms etc.;
2000-03-13, by wenzelm
use HOLogic.Not;
2000-03-13, by wenzelm
adapted to new PureThy.add_thms etc.;
2000-03-13, by wenzelm
adapted to new PureThy.add_thms etc.;
2000-03-13, by wenzelm
export vars_of;
2000-03-13, by wenzelm
adapted to new PureThy.add_thms etc.;
2000-03-13, by wenzelm
added Not;
2000-03-13, by wenzelm
adapted to new PureThy.add_thms etc.;
2000-03-13, by wenzelm
tuned;
2000-03-13, by wenzelm
cases: preserve order;
2000-03-13, by wenzelm
*** empty log message ***
2000-03-13, by nipkow
exhaust -> cases
2000-03-13, by nipkow
exhaust_tac -> cases_tac
2000-03-13, by nipkow
renamed "f" to "le" and "mset" to "multiset"
2000-03-13, by paulson
fixed the goal statement of sorted_qsort
2000-03-13, by paulson
adapted to new PureThy.add_thms etc.;
2000-03-13, by wenzelm
add_thms, add_axioms, add_defs: return theorems as well;
2000-03-13, by wenzelm
added |>> and |>>>;
2000-03-13, by wenzelm
exhaust->cases
2000-03-13, by nipkow
Type.typ_match now uses Vartab instead of association lists.
2000-03-10, by berghofe
tidied
2000-03-10, by paulson
now uses recdef instead of "rules"
2000-03-10, by paulson
tidied, and new thm perm_append2_eq
2000-03-10, by paulson
cases_tac
2000-03-10, by nipkow
Type.typ_match now uses Vartab instead of association lists.
2000-03-10, by berghofe
Type.unify now uses Vartab instead of association lists.
2000-03-10, by berghofe
Added function min_key.
2000-03-10, by berghofe
Added functions subst_TVars_Vartab and typ_subst_TVars_Vartab.
2000-03-10, by berghofe
Envir now uses Vartab instead of association lists.
2000-03-10, by berghofe
Type.unify and Type.typ_match now use Vartab instead of association lists.
2000-03-10, by berghofe
add_cases_induct: produce proper case names;
2000-03-10, by wenzelm
type descr;
2000-03-10, by wenzelm
check_case: disallow (T)Vars in invoked case;
2000-03-09, by wenzelm
quote tag arguments;
2000-03-09, by wenzelm
more robust case names of induct;
2000-03-09, by wenzelm
cleaned comment;
2000-03-09, by wenzelm
nicely tarted up Mutil
2000-03-09, by paulson
renamed to rsync-isabelle;
2000-03-09, by wenzelm
tuned;
2000-03-09, by wenzelm
made rsync "official"
2000-03-09, by kleing
mod_less, div_less are now default simprules
2000-03-09, by paulson
less
more
|
(0)
-3000
-1000
-240
+240
+1000
+3000
+10000
+30000
tip