Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-10000
-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.
*** empty log message ***
2000-11-21, by nipkow
BCV integration (type system is semilattice)
2000-11-20, by kleing
BCV integration (first step)
2000-11-20, by kleing
export freeze_thaw_type;
2000-11-18, by wenzelm
improved messages;
2000-11-18, by wenzelm
default_intro_classes_tac: Tactic.distinct_subgoals_tac;
2000-11-18, by wenzelm
axclass ordered_ring;
2000-11-18, by wenzelm
quot_cond_function: simplified, support conditional definition;
2000-11-18, by wenzelm
abs_eq_0: #0 instead of 0;
2000-11-18, by wenzelm
symbol syntax for "abs";
2000-11-18, by wenzelm
added axclass ordered_field;
2000-11-18, by wenzelm
check result: Envir.beta_norm;
2000-11-17, by wenzelm
Envir.beta_norm;
2000-11-17, by wenzelm
added beta_norm;
2000-11-17, by wenzelm
tuned;
2000-11-17, by wenzelm
removed quot_cond_function1, quot_function1;
2000-11-17, by wenzelm
UNIV_witness;
2000-11-17, by wenzelm
Ring_and_Field;
2000-11-17, by wenzelm
Library/Ring_and_Field.thy;
2000-11-17, by wenzelm
rings and fields;
2000-11-16, by bauerg
Proof.assert_forward;
2000-11-16, by wenzelm
added not_equiv_sym, not_equiv_trans1/2;
2000-11-16, by wenzelm
added abs_mult, abs_eq_0, square_nonzero;
2000-11-16, by wenzelm
ground terms section: new intro
2000-11-16, by paulson
CTT
2000-11-16, by paulson
separate rules for function/operation definitions;
2000-11-15, by wenzelm
renamed integ_le_less to int_le_less;
2000-11-15, by wenzelm
updated;
2000-11-15, by wenzelm
isabellebody: \par at begin/end;
2000-11-15, by wenzelm
auto update
2000-11-14, by paulson
first version of Advanced Inductive Defs section
2000-11-14, by paulson
x-symbol support for Pi, Sigma, -->, : (membership)
2000-11-14, by paulson
new Main.thy as in HOL, ZF
2000-11-14, by paulson
added read_terms, read_props (simulataneous type-inference);
2000-11-13, by wenzelm
tuned statement args;
2000-11-13, by wenzelm
tuned IsarThy.theorem_i;
2000-11-13, by wenzelm
added students
2000-11-13, by kleing
Removed > and >=
2000-11-13, by nipkow
Removed > and >= again.
2000-11-13, by nipkow
quot_cond_definition;
2000-11-12, by wenzelm
simplified induction;
2000-11-12, by wenzelm
updated;
2000-11-12, by wenzelm
"induct" method: handle proper rules;
2000-11-12, by wenzelm
removed warning for "stripped" option;
2000-11-12, by wenzelm
removed junk;
2000-11-12, by wenzelm
Syntax.pure_appl_syntax declared as output syntax for theory ProtoPure;
2000-11-12, by wenzelm
* added overloaded operations "inverse" and "divide" (infix "/");
2000-11-10, by wenzelm
int_distrib;
2000-11-10, by wenzelm
nat_distrib;
2000-11-10, by wenzelm
hide_space(_i): use Sign.certify_tycon, Sign.certify_tyabbr, Sign.certify_const;
2000-11-10, by wenzelm
tuned;
2000-11-10, by wenzelm
use inverse, divide from basic HOL;
2000-11-10, by wenzelm
norm_hhf_tac;
2000-11-10, by wenzelm
rewrite_goal_tac moved to tactic.ML;
2000-11-10, by wenzelm
added rewrite_goal_tac;
2000-11-10, by wenzelm
added certify_tycon, certify_tyabbr, certify_const;
2000-11-10, by wenzelm
has_meta_prems: include "==";
2000-11-10, by wenzelm
store_standard_thm "norm_hhf_eq";
2000-11-10, by wenzelm
proper theory context for mesontest2;
2000-11-10, by wenzelm
inductive_rulify2 accomodates malformed induction rules;
2000-11-10, by wenzelm
Sign.certify_tycon, Sign.certify_const;
2000-11-10, by wenzelm
improved cong_definition theorems;
2000-11-10, by wenzelm
simplified induction;
2000-11-10, by wenzelm
added axclass power (from HOL.thy);
2000-11-10, by wenzelm
simplified atomize;
2000-11-10, by wenzelm
axclass power moved to Nat.thy;
2000-11-10, by wenzelm
added axclass inverse and consts inverse, divide (infix "/");
2000-11-10, by wenzelm
FOL_basic_ss: simprocs moved to FOL_ss;
2000-11-10, by wenzelm
added atomize_eq;
2000-11-10, by wenzelm
val atomize = thms "atomize'";
2000-11-10, by wenzelm
> etc
2000-11-10, by nipkow
new: > and >=
2000-11-10, by nipkow
rule inversion
2000-11-10, by nipkow
JMB -> JMPB. Email von Johannes Pfeifroth.
2000-11-10, by nipkow
updated;
2000-11-09, by wenzelm
fixed \title: convert "_" to "-";
2000-11-09, by wenzelm
tuned isabelle environment;
2000-11-08, by wenzelm
subgoals
2000-11-08, by nipkow
*** empty log message ***
2000-11-08, by nipkow
better discussion of rule induction
2000-11-07, by paulson
Thm.dest_abs now takes an additional argument.
2000-11-07, by berghofe
Moved rewriting functions from Thm to MetaSimplifier.
2000-11-07, by berghofe
- Moved rewriting functions to meta_simplifier.ML
2000-11-07, by berghofe
moved rewriting functions from Drule to MetaSimplifier
2000-11-07, by berghofe
- new theorems imp_cong and swap_prems_eq
2000-11-07, by berghofe
Added new file meta_simplifier.ML
2000-11-07, by berghofe
Moved meta simplification stuff from Thm to MetaSimplifier.
2000-11-07, by berghofe
Added type constraint in theorem "lift".
2000-11-07, by berghofe
*** empty log message ***
2000-11-07, by nipkow
method 'induct' now handles non-atomic goals;
2000-11-06, by wenzelm
improved: 'induct' handle non-atomic goals;
2000-11-06, by wenzelm
make: open_parms argument;
2000-11-06, by wenzelm
RuleCases.make true;
2000-11-06, by wenzelm
added rewrite_goal_tac;
2000-11-06, by wenzelm
added typ_instance;
2000-11-06, by wenzelm
Sign.typ_instance;
2000-11-06, by wenzelm
inductive_atomize, inductive_rulify;
2000-11-06, by wenzelm
* Isar/HOL: method 'induct' now handles non-atomic goals; as a
2000-11-06, by wenzelm
tuned atomize_goal;
2000-11-06, by wenzelm
minor modifications for new Springer style
2000-11-06, by paulson
minor changes
2000-11-06, by paulson
auto update
2000-11-06, by paulson
*** empty log message ***
2000-11-06, by nipkow
updated;
2000-11-04, by wenzelm
tuned method "rule" and "default";
2000-11-04, by wenzelm
isamarkup: handle % in input;
2000-11-04, by wenzelm
tuned;
2000-11-04, by wenzelm
misc stuff;
2000-11-04, by wenzelm
tuned;
2000-11-03, by wenzelm
proper setup of "parallel";
2000-11-03, by wenzelm
tuned notation;
2000-11-03, by wenzelm
adapted "obtain" proofs;
2000-11-03, by wenzelm
provide case names for rev_induct, rev_cases;
2000-11-03, by wenzelm
rev_exhaust: rulify;
2000-11-03, by wenzelm
removed atomic_Trueprop (now in Pure/Isar/auto_bind.ML);
2000-11-03, by wenzelm
"atomize" for classical tactics;
2000-11-03, by wenzelm
atomize: all automated tactics that "solve" goals;
2000-11-03, by wenzelm
fixed two obscurities of "fix": predeclare_terms;
2000-11-03, by wenzelm
tuned names;
2000-11-03, by wenzelm
improved handling of "that": insert into goal, only declare as Pure "intro";
2000-11-03, by wenzelm
less
more
|
(0)
-10000
-3000
-1000
-120
+120
+1000
+3000
+10000
+30000
tip