Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-10000
-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.
improved superclass entry for classes and definition status of is_class, class
2000-12-06, by oheimb
improved superclass entry for classes and definition status of is_class, class
2000-12-06, by oheimb
simplified interactive handling
2000-12-06, by oheimb
some derived properties;
2000-12-06, by bauerg
HOL/Real: "rinv" and "hrinv" replaced by overloaded "inverse" function;
2000-12-06, by bauerg
*** empty log message ***
2000-12-06, by nipkow
converted rinv and hrinv to inverse;
2000-12-06, by bauerg
converted rinv to inverse;
2000-12-06, by bauerg
added \<a> ... \<z>;
2000-12-06, by wenzelm
tuned;
2000-12-06, by wenzelm
theory file for Numbers section
2000-12-06, by paulson
auto generated
2000-12-06, by paulson
auto update
2000-12-06, by paulson
deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
2000-12-06, by paulson
miniscoping of nat_diff_split
2000-12-06, by paulson
new theory Numbers.thy
2000-12-05, by paulson
new package amsfonts
2000-12-05, by paulson
tidying
2000-12-05, by paulson
partial numerics section
2000-12-05, by paulson
nat and int sections but no real
2000-12-05, by paulson
fixed document preparation
2000-12-05, by kleing
BCV Integration
2000-12-05, by kleing
jvm_progs now also store maximum op_stack depth
2000-12-05, by kleing
*** empty log message ***
2000-12-05, by nipkow
*** empty log message ***
2000-12-04, by wenzelm
updated;
2000-12-04, by wenzelm
proper order of symbols for genarated table in system manual;
2000-12-04, by wenzelm
added \isabeginpar, \isaendpar;
2000-12-04, by wenzelm
proper order of modes;
2000-12-04, by wenzelm
diagnostic commands: comment;
2000-12-04, by wenzelm
export get_skolem;
2000-12-04, by wenzelm
fixed binding of parameters;
2000-12-04, by wenzelm
dignostic commands: comment;
2000-12-04, by wenzelm
include table of Isabelle standard symbols;
2000-12-04, by wenzelm
loads the new theory Numbers.thy
2000-12-04, by paulson
fixed formatting in section heading
2000-12-04, by paulson
auto update
2000-12-04, by paulson
tuned;
2000-12-01, by wenzelm
Now adjusted to mixed terms involving coercions.
2000-12-01, by nipkow
Linear arithmetic now copes with mixed nat/int formulae.
2000-12-01, by nipkow
append print modes;
2000-12-01, by wenzelm
no_brackets mode;
2000-12-01, by wenzelm
use_dir: modes;
2000-12-01, by wenzelm
append print_modes;
2000-12-01, by wenzelm
ignore quick_and_dirty for coind;
2000-12-01, by wenzelm
FreeUltrafilterNat ("\\<U>");
2000-12-01, by wenzelm
schematic goals;
2000-12-01, by wenzelm
removed quick_and_dirty;
2000-12-01, by wenzelm
superscripts: syntax (latex);
2000-12-01, by wenzelm
usedir: -m option;
2000-12-01, by wenzelm
added \mathcal A-Z;
2000-12-01, by wenzelm
option -m;
2000-12-01, by wenzelm
*** empty log message ***
2000-12-01, by nipkow
*** empty log message ***
2000-12-01, by nipkow
many new div and mod properties (borrowed from Integ/IntDiv)
2000-12-01, by paulson
renamed less_eq_Suc_add to less_imp_Suc_add
2000-12-01, by paulson
tuned;
2000-11-30, by wenzelm
removed "./configure";
2000-11-30, by wenzelm
/usr/bin/env bash;
2000-11-30, by wenzelm
schematic props;
2000-11-30, by wenzelm
removed get_goal;
2000-11-30, by wenzelm
added is_replaced_dummy_pattern;
2000-11-30, by wenzelm
renamed "equivalence_class" to "class";
2000-11-30, by wenzelm
schematic goals;
2000-11-30, by wenzelm
cases/induct: tuned handling of facts ('consumes');
2000-11-30, by wenzelm
'consumes' att;
2000-11-30, by wenzelm
misc;
2000-11-30, by wenzelm
replaced Eps by SOME
2000-11-30, by paulson
*** empty log message ***
2000-11-30, by nipkow
some properties;
2000-11-30, by bauerg
*** empty log message ***
2000-11-30, by nipkow
resolveq_cases_tac moved here from Pure/Isar/method.ML;
2000-11-29, by wenzelm
resolveq(_cases)_tac moved to HOL/Tools/induct_method.ML;
2000-11-29, by wenzelm
expand_split_asm -> split_split_asm
2000-11-29, by nipkow
*** empty log message ***
2000-11-29, by nipkow
*** empty log message ***
2000-11-29, by nipkow
simproc for cancelling common factors around = < <= div /
2000-11-29, by paulson
invoking CancelNumeralFactorFun
2000-11-29, by paulson
new simproc file cancel_numeral_factor.ML
2000-11-29, by paulson
added a reference to {sec:products} for ordered pair reasoning
2000-11-28, by paulson
fixed hostname;
2000-11-28, by wenzelm
detect CVSROOT;
2000-11-28, by wenzelm
tuned;
2000-11-28, by wenzelm
added consumes, consumes_default;
2000-11-28, by wenzelm
resolveq_cases_tac: insert facts;
2000-11-28, by wenzelm
added "consumes" attribute;
2000-11-28, by wenzelm
consume facts;
2000-11-28, by wenzelm
consumes0/1;
2000-11-28, by wenzelm
RuleCases.save;
2000-11-28, by wenzelm
*** empty log message ***
2000-11-27, by nipkow
deleted unused result intrel_refl
2000-11-27, by paulson
*** empty log message ***
2000-11-27, by nipkow
*** empty log message ***
2000-11-26, by nipkow
*** empty log message ***
2000-11-26, by nipkow
hide many names from Datatype_Universe.
2000-11-24, by nipkow
exception Interrupt = SML90.Interrupt;
2000-11-24, by wenzelm
added exception Interrupt for use in function Library/try
2000-11-24, by paulson
arith_tac: atomize;
2000-11-23, by wenzelm
standard: close_derivation;
2000-11-23, by wenzelm
* HOL: syntax or "abs";
2000-11-23, by wenzelm
*** empty log message ***
2000-11-23, by nipkow
tuned;
2000-11-22, by wenzelm
tuned;
2000-11-22, by wenzelm
*** empty log message ***
2000-11-22, by wenzelm
*** empty log message ***
2000-11-22, by nipkow
tag result with name reference to final binding (basically just a comment);
2000-11-21, by wenzelm
Tactic.distinct_subgoals_tac moved to internal intro_classes_tac;
2000-11-21, by wenzelm
replace \<dots>;
2000-11-21, by wenzelm
unsymbolize;
2000-11-21, by wenzelm
quote executable;
2000-11-21, by wenzelm
tuned;
2000-11-21, by wenzelm
;
2000-11-21, by bauerg
adjusted for BV changes (Ok -> OK)
2000-11-21, by kleing
thebibliography environment: replaced the Springer version by the standard one
2000-11-21, by paulson
alternative function definition;
2000-11-21, by bauerg
*** 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
assumption / finish: handle non-atomic assumptions from context as well;
2000-11-03, by wenzelm
added atomic_judgment;
2000-11-03, by wenzelm
structure Obtain = Obtain;
2000-11-03, by wenzelm
new lemma card_Diff2_less for mulilated chess board
2000-11-03, by paulson
*** empty log message ***
2000-11-03, by nipkow
less
more
|
(0)
-10000
-3000
-1000
-240
+240
+1000
+3000
+10000
+30000
tip