Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-10000
-3000
-1000
-224
+224
+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.
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
*** empty log message ***
2000-11-03, by nipkow
*** empty log message ***
2000-11-03, by nipkow
the section command will belong to the new file
2000-11-03, by paulson
advanced induction examples
2000-11-03, by paulson
auto update?
2000-11-03, by paulson
replaced Acc.thy by Advanced.thy
2000-11-03, by paulson
no longer needed: too complicated an example
2000-11-02, by paulson
*** empty log message ***
2000-11-02, by nipkow
auto generated
2000-11-02, by paulson
tuned goal output;
2000-10-31, by wenzelm
*** empty log message ***
2000-10-31, by nipkow
*** empty log message ***
2000-10-31, by nipkow
updated;
2000-10-30, by wenzelm
tuned goals output;
2000-10-30, by wenzelm
improved statement bindings for props;
2000-10-30, by wenzelm
converse: syntax \<inverse>;
2000-10-30, by wenzelm
tuned;
2000-10-30, by wenzelm
added ex/PER.thy;
2000-10-30, by wenzelm
improved doc of "subgoals" antiquotation;
2000-10-30, by wenzelm
replaced \isasymmacron by \isasyminverse;
2000-10-30, by wenzelm
tuned tex template;
2000-10-30, by wenzelm
Partial equivalence relations (leftover from HOL/Quot);
2000-10-30, by wenzelm
added antiq. subgoals
2000-10-30, by nipkow
Added antiquotation "subgoals".
2000-10-30, by nipkow
Mod because of additional parameters to pretty_goals.
2000-10-30, by nipkow
back to 1.167, due to Emacs/CVS casualty!!;
2000-10-27, by wenzelm
added instantiate_tac
2000-10-27, by oheimb
*** empty log message ***
2000-10-27, by wenzelm
removed isabelle resources: are available from main pages
2000-10-27, by kleing
cleanup, looks ok now with konqueror, too
2000-10-27, by kleing
*** empty log message ***
2000-10-26, by nipkow
*** empty log message ***
2000-10-26, by nipkow
added the $Id:$ line
2000-10-26, by paulson
*** empty log message ***
2000-10-26, by nipkow
*** empty log message ***
2000-10-26, by nipkow
use Library/List_Prefix;
2000-10-25, by wenzelm
added HOL/Library/List_Prefix;
2000-10-25, by wenzelm
improved antiquotations;
2000-10-25, by wenzelm
added \isarantiq;
2000-10-25, by wenzelm
add \<le> to list of "good" symbols;
2000-10-25, by wenzelm
tuned names;
2000-10-25, by wenzelm
added List_Prefix;
2000-10-25, by wenzelm
more "xsymbols" syntax;
2000-10-25, by wenzelm
"List prefixes" library theory (replaces old Lex/Prefix);
2000-10-25, by wenzelm
*** empty log message ***
2000-10-25, by nipkow
*** empty log message ***
2000-10-25, by nipkow
inputs Even.tex
2000-10-25, by paulson
minor tinkering
2000-10-25, by paulson
Even numbers section of Inductive chapter
2000-10-25, by paulson
tuned msg;
2000-10-25, by wenzelm
antiquotation "goals": error message;
2000-10-25, by wenzelm
* support sub/super scripts (for single symbols only), input syntax is
2000-10-24, by wenzelm
let commands access Toplevel.state;
2000-10-24, by wenzelm
added pretty_goals;
2000-10-24, by wenzelm
added antiquotation "goals" and option "goals_limit";
2000-10-24, by wenzelm
tuned;
2000-10-24, by wenzelm
added clasimpset: unit -> clasimpset;
2000-10-24, by wenzelm
tuned;
2000-10-24, by wenzelm
Acc example
2000-10-24, by paulson
even numbers example
2000-10-24, by paulson
intro_classes by default;
2000-10-23, by wenzelm
declare trancl rules;
2000-10-23, by wenzelm
tuned;
2000-10-23, by wenzelm
updated;
2000-10-23, by wenzelm
intro_classes by default;
2000-10-23, by wenzelm
make sure default document works;
2000-10-23, by wenzelm
comment out Pure-copied target;
2000-10-23, by wenzelm
* HOL: default proof step now includes 'intro_classes';
2000-10-23, by wenzelm
*** empty log message ***
2000-10-23, by nipkow
part of set-up
2000-10-23, by paulson
sets chapter
2000-10-23, by paulson
fixed crossref
2000-10-23, by paulson
tidied
2000-10-23, by paulson
X-symbol
2000-10-23, by paulson
auto gen
2000-10-23, by paulson
addition of Rules, Sets and some macros of lcp
2000-10-23, by paulson
goodbye to this dummy file
2000-10-23, by paulson
now includes Rules, Sets (?)
2000-10-23, by paulson
the Rules chapter and theories
2000-10-23, by paulson
the Sets chapter and theories
2000-10-23, by paulson
quantifiers now allowed in inductive defs
2000-10-23, by paulson
tidied
2000-10-23, by paulson
isatool unsymbolize;
2000-10-23, by wenzelm
added type_definitionI;
2000-10-23, by wenzelm
tuned deps;
2000-10-23, by wenzelm
contrapos
2000-10-23, by paulson
two spelling fixes
2000-10-23, by paulson
tuned;
2000-10-22, by wenzelm
simplified quotients (only plain total equivs);
2000-10-22, by wenzelm
tuned;
2000-10-20, by wenzelm
*** empty log message ***
2000-10-20, by nipkow
tuned;
2000-10-20, by wenzelm
*** empty log message ***
2000-10-20, by nipkow
provide more theorems (see subset.thy);
2000-10-19, by wenzelm
less
more
|
(0)
-10000
-3000
-1000
-224
+224
+1000
+3000
+10000
+30000
tip