isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -3000 -1000 -300 -100 -50 -30 +30 +50 +100 +300 +1000 +3000 +10000 +30000 tip

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

less more | (0) -3000 -1000 -300 -100 -50 -30 +30 +50 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle