Old_HOL: Graph

Mercurial Mercurial > repos > Old_HOL / graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -100 -60 tip

Simplified proof.
1995-02-01, by nipkow
The thm if(P,Q,R) now yields the two conditional rewrite rules P ==> Q and
1995-02-01, by nipkow
Added Un_empty (also to set_ss)
1995-01-30, by nipkow
Added some simplifications for ? x.
1995-01-29, by nipkow
Added "nth" and some lemmas.
1995-01-26, by nipkow
added bind_thm for theorems made by "standard ..." Isabelle94-2
1994-12-14, by clasohm
improved primrec: now calls store_thm;
1994-12-14, by wenzelm
removed HOL_Lemmas structure and added qed_goal
1994-12-09, by clasohm
replaced store_thm by bind_thm
1994-12-08, by clasohm
Added (? x. x=t & P) = P to the simpset.
1994-12-07, by nipkow
Removed a local lemma which is now part of HOL_ss.
1994-12-07, by nipkow
Moved the old List to ex and replaced it by one defined via
1994-12-02, by nipkow
Moved HOL/List to HOL/ex/SList (strict list).
1994-12-02, by nipkow
small updates because datatype list is now used. In particular Nil -> []
1994-12-02, by nipkow
list_ind_tac -> list.induct_tac
1994-12-02, by nipkow
Added dependency on thy_syntax.ML
1994-12-01, by nipkow
Fixed small bug in print-translation for set comprehension.
1994-11-28, by nipkow
adapted to 'subtype' section;
1994-11-28, by wenzelm
added IMP/Properties
1994-11-25, by nipkow
Proved determinism.
1994-11-25, by nipkow
minor changes according to new hologic;
1994-11-25, by wenzelm
replaced ["term"] by termS;
1994-11-25, by wenzelm
adapted to 'subtype' section;
1994-11-25, by wenzelm
added id_in_pair_conv
1994-11-25, by nipkow
Removed obsolete induction package
1994-11-25, by nipkow
removed Sum-rules
1994-11-25, by nipkow
checks that the recursive sets are Consts before taking
1994-11-25, by lcp
renamed term_induct/2 -> Term_induct/2
1994-11-25, by nipkow
replaced prove_goal by qed_goal
1994-11-25, by clasohm
rules -> defs
1994-11-24, by nipkow
The collection of theories required for inductive definitions.
1994-11-24, by nipkow
Trancl.{thy,ML} was missing
1994-11-24, by nipkow
moved parser stuff to thy_syntax.ML;
1994-11-23, by wenzelm
add_subtype now adds constant definition for the representing set;
1994-11-23, by wenzelm
moved remaining thy syntax stuff to thy_syntax.ML;
1994-11-23, by wenzelm
added 'datatype' and 'primrec';
1994-11-23, by wenzelm
replaced 'val ... = result()' by 'qed "..."'
1994-11-21, by clasohm
HOL,ZF/Makefile: enclosed multiple "use" calls in parentheses. This
1994-11-11, by lcp
Initial revision
1994-11-10, by nipkow
Added headers and made various small mods.
1994-11-09, by nipkow
Added header.
1994-11-09, by nipkow
HOL/ROOT/HOL_dup_cs: removed as obsolete
1994-11-08, by lcp
changed loadpath
1994-11-06, by clasohm
changed command for making 'test'
1994-11-06, by clasohm
rearranged theory section stuff;
1994-11-04, by wenzelm
moved section parser to thy_syntax.ML;
1994-11-04, by wenzelm
lnternal interface for HOL subtype definitions;
1994-11-04, by wenzelm
additional theory file sections for HOL;
1994-11-04, by wenzelm
abstract syntax operations for HOL;
1994-11-04, by wenzelm
Replaced fast_tac by simp_tac in a number of places.
1994-11-03, by nipkow
added IOA files
1994-11-02, by clasohm
added IOA to isabelle/HOL
1994-11-02, by clasohm
HOL/HOL/swap: deleted
1994-11-01, by lcp
HOL/ex/cla: proofs now use deepen_tac instead of best_tac HOL_dup_cs
1994-10-31, by lcp
HOL/HOL.ML/selectI2: new rule for descriptions
1994-10-13, by lcp
{HOL,ZF}/indrule/ind_tac: now calls DEPTH_SOLVE_1 instead of REPEAT, to
1994-10-12, by lcp
{HOL,ZF}/indrule/ind_tac: now calls DEPTH_SOLVE_1 instead of REPEAT, to
1994-10-12, by lcp
replaced some "rules" by "defs"
1994-10-06, by nipkow
changed precedences to eliminate some ambiguities Isabelle94-1
1994-10-04, by clasohm
moved LList* to ex
1994-09-28, by nipkow

less more | (0) -100 -60 tip

Old_HOL