Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-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.
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
less
more
|
(0)
-3000
-1000
-120
+120
+1000
+3000
+10000
+30000
tip