Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary

shortlog

changelog
 graph 
tags

bookmarks

branches

files

gz

help
less
more

(0)
10000
3000
1000
300
100
60
+60
+100
+300
+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 JavaScriptenabled browsers.
first version of Advanced Inductive Defs section
20001114, by paulson
xsymbol support for Pi, Sigma, >, : (membership)
20001114, by paulson
new Main.thy as in HOL, ZF
20001114, by paulson
added read_terms, read_props (simulataneous typeinference);
20001113, by wenzelm
tuned statement args;
20001113, by wenzelm
tuned IsarThy.theorem_i;
20001113, by wenzelm
added students
20001113, by kleing
Removed > and >=
20001113, by nipkow
Removed > and >= again.
20001113, by nipkow
quot_cond_definition;
20001112, by wenzelm
simplified induction;
20001112, by wenzelm
updated;
20001112, by wenzelm
"induct" method: handle proper rules;
20001112, by wenzelm
removed warning for "stripped" option;
20001112, by wenzelm
removed junk;
20001112, by wenzelm
Syntax.pure_appl_syntax declared as output syntax for theory ProtoPure;
20001112, by wenzelm
* added overloaded operations "inverse" and "divide" (infix "/");
20001110, by wenzelm
int_distrib;
20001110, by wenzelm
nat_distrib;
20001110, by wenzelm
hide_space(_i): use Sign.certify_tycon, Sign.certify_tyabbr, Sign.certify_const;
20001110, by wenzelm
tuned;
20001110, by wenzelm
use inverse, divide from basic HOL;
20001110, by wenzelm
norm_hhf_tac;
20001110, by wenzelm
rewrite_goal_tac moved to tactic.ML;
20001110, by wenzelm
added rewrite_goal_tac;
20001110, by wenzelm
added certify_tycon, certify_tyabbr, certify_const;
20001110, by wenzelm
has_meta_prems: include "==";
20001110, by wenzelm
store_standard_thm "norm_hhf_eq";
20001110, by wenzelm
proper theory context for mesontest2;
20001110, by wenzelm
inductive_rulify2 accomodates malformed induction rules;
20001110, by wenzelm
Sign.certify_tycon, Sign.certify_const;
20001110, by wenzelm
improved cong_definition theorems;
20001110, by wenzelm
simplified induction;
20001110, by wenzelm
added axclass power (from HOL.thy);
20001110, by wenzelm
simplified atomize;
20001110, by wenzelm
axclass power moved to Nat.thy;
20001110, by wenzelm
added axclass inverse and consts inverse, divide (infix "/");
20001110, by wenzelm
FOL_basic_ss: simprocs moved to FOL_ss;
20001110, by wenzelm
added atomize_eq;
20001110, by wenzelm
val atomize = thms "atomize'";
20001110, by wenzelm
> etc
20001110, by nipkow
new: > and >=
20001110, by nipkow
rule inversion
20001110, by nipkow
JMB > JMPB. Email von Johannes Pfeifroth.
20001110, by nipkow
updated;
20001109, by wenzelm
fixed \title: convert "_" to "";
20001109, by wenzelm
tuned isabelle environment;
20001108, by wenzelm
subgoals
20001108, by nipkow
*** empty log message ***
20001108, by nipkow
better discussion of rule induction
20001107, by paulson
Thm.dest_abs now takes an additional argument.
20001107, by berghofe
Moved rewriting functions from Thm to MetaSimplifier.
20001107, by berghofe
 Moved rewriting functions to meta_simplifier.ML
20001107, by berghofe
moved rewriting functions from Drule to MetaSimplifier
20001107, by berghofe
 new theorems imp_cong and swap_prems_eq
20001107, by berghofe
Added new file meta_simplifier.ML
20001107, by berghofe
Moved meta simplification stuff from Thm to MetaSimplifier.
20001107, by berghofe
Added type constraint in theorem "lift".
20001107, by berghofe
*** empty log message ***
20001107, by nipkow
method 'induct' now handles nonatomic goals;
20001106, by wenzelm
less
more

(0)
10000
3000
1000
300
100
60
+60
+100
+300
+1000
+3000
+10000
+30000
tip