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

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
Small simplification in add_datatype.
1994-09-27, by nipkow
replaced local instantaite_types by inferT_axm
1994-09-26, by nipkow
minor cleanup, added 'axclass', 'instance', 'syntax', 'defs' sections;
1994-09-21, by wenzelm
Definition of C was not truly prim rec because C was called inside Gamma
1994-09-16, by nipkow
improved error reporting for primrec
1994-09-15, by nipkow
replaced lookup_const by Sign.const_type; Isabelle94
1994-09-14, by wenzelm
Allowed string as function name in primrec header
1994-09-11, by nipkow
{HOL,ZF}/indrule/quant_induct: replaced ssubst in eresolve_tac by
1994-09-08, by lcp
HOL/IMP/Equiv/bexp_iff: split proof into separate directions, to be faster
1994-09-07, by lcp

less more | (0) -100 -60 tip

Old_HOL