Mon, 26 Sep 1994 17:55:45 +0100 exported pretty_sort;
wenzelm [Mon, 26 Sep 1994 17:55:45 +0100] rev 620
exported pretty_sort; various minor internal changes;
Mon, 26 Sep 1994 17:36:10 +0100 added init_pps;
wenzelm [Mon, 26 Sep 1994 17:36:10 +0100] rev 619
added init_pps;
Mon, 26 Sep 1994 17:35:45 +0100 added init_database (somewhat experimental);
wenzelm [Mon, 26 Sep 1994 17:35:45 +0100] rev 618
added init_database (somewhat experimental);
Mon, 26 Sep 1994 17:35:23 +0100 added flag show_no_free_types: bool ref;
wenzelm [Mon, 26 Sep 1994 17:35:23 +0100] rev 617
added flag show_no_free_types: bool ref;
Mon, 26 Sep 1994 17:34:59 +0100 explode_tr now produces leadings 0s;
wenzelm [Mon, 26 Sep 1994 17:34:59 +0100] rev 616
explode_tr now produces leadings 0s; implode_ast_tr' now quotes result;
Wed, 21 Sep 1994 15:39:02 +0200 minor cleanup, added 'syntax' section;
wenzelm [Wed, 21 Sep 1994 15:39:02 +0200] rev 615
minor cleanup, added 'syntax' section;
Thu, 15 Sep 1994 13:13:54 +0200 now mentions that the sections are available as
lcp [Thu, 15 Sep 1994 13:13:54 +0200] rev 614
now mentions that the sections are available as Datatypes and (Co)Inductive Definitions in Isabelle/HOL
Wed, 14 Sep 1994 16:11:19 +0200 removed lookup_const (use Sign.const_type instead); Isabelle94
wenzelm [Wed, 14 Sep 1994 16:11:19 +0200] rev 613
removed lookup_const (use Sign.const_type instead);
Wed, 14 Sep 1994 16:05:39 +0200 replaced lookup_const by Sign.const_type;
wenzelm [Wed, 14 Sep 1994 16:05:39 +0200] rev 612
replaced lookup_const by Sign.const_type;
Wed, 14 Sep 1994 16:02:06 +0200 now uses Sign.const_type;
wenzelm [Wed, 14 Sep 1994 16:02:06 +0200] rev 611
now uses Sign.const_type;
Wed, 14 Sep 1994 14:49:56 +0200 letrec syntax: replaced "id" by "idt";
wenzelm [Wed, 14 Sep 1994 14:49:56 +0200] rev 610
letrec syntax: replaced "id" by "idt";
Tue, 13 Sep 1994 11:39:49 +0200 updated for Isabelle94
lcp [Tue, 13 Sep 1994 11:39:49 +0200] rev 609
updated for Isabelle94
Tue, 13 Sep 1994 11:19:38 +0200 now uses find to locate .thy.ML files everywhere
lcp [Tue, 13 Sep 1994 11:19:38 +0200] rev 608
now uses find to locate .thy.ML files everywhere
Tue, 13 Sep 1994 10:42:34 +0200 updated the identifier "version"
lcp [Tue, 13 Sep 1994 10:42:34 +0200] rev 607
updated the identifier "version"
Tue, 13 Sep 1994 10:26:24 +0200 minor updates
lcp [Tue, 13 Sep 1994 10:26:24 +0200] rev 606
minor updates
Mon, 12 Sep 1994 13:20:07 +0200 New Makefile for Logics Manual
lcp [Mon, 12 Sep 1994 13:20:07 +0200] rev 605
New Makefile for Logics Manual
Mon, 12 Sep 1994 13:06:07 +0200 New Makefile for Reference Manual
lcp [Mon, 12 Sep 1994 13:06:07 +0200] rev 604
New Makefile for Reference Manual
Mon, 12 Sep 1994 13:01:38 +0200 New Makefile for Introduction
lcp [Mon, 12 Sep 1994 13:01:38 +0200] rev 603
New Makefile for Introduction
Mon, 12 Sep 1994 12:45:10 +0200 New Makefile for ind-defs
lcp [Mon, 12 Sep 1994 12:45:10 +0200] rev 602
New Makefile for ind-defs
Sun, 11 Sep 1994 12:52:00 +0200 Added primrec section
nipkow [Sun, 11 Sep 1994 12:52:00 +0200] rev 601
Added primrec section
Sun, 11 Sep 1994 10:59:09 +0200 Added primrec section.
nipkow [Sun, 11 Sep 1994 10:59:09 +0200] rev 600
Added primrec section.
Fri, 09 Sep 1994 13:10:09 +0200 now in a format that could be published
lcp [Fri, 09 Sep 1994 13:10:09 +0200] rev 599
now in a format that could be published
Fri, 09 Sep 1994 12:34:54 +0200 added Abrial and Laffitte; Kunen; Winskel, etc.
lcp [Fri, 09 Sep 1994 12:34:54 +0200] rev 598
added Abrial and Laffitte; Kunen; Winskel, etc.
Fri, 09 Sep 1994 12:25:56 +0200 Updated for existence of HOL version and infinitely
lcp [Fri, 09 Sep 1994 12:25:56 +0200] rev 597
Updated for existence of HOL version and infinitely branching datatypes
Fri, 09 Sep 1994 11:57:49 +0200 Per cent (%) now functions as comment character in tt
lcp [Fri, 09 Sep 1994 11:57:49 +0200] rev 596
Per cent (%) now functions as comment character in tt box environment
Fri, 09 Sep 1994 11:52:38 +0200 Added mention of directory IMP; tidied the section on examples.
lcp [Fri, 09 Sep 1994 11:52:38 +0200] rev 595
Added mention of directory IMP; tidied the section on examples.
Fri, 09 Sep 1994 11:45:44 +0200 Logics/HOL: Section 3, added Pow and its rule. New sections 6 on the
lcp [Fri, 09 Sep 1994 11:45:44 +0200] rev 594
Logics/HOL: Section 3, added Pow and its rule. New sections 6 on the datatype declaration and 7 on (co)inductive definitions. Added mention of directory IMP.
Fri, 09 Sep 1994 11:40:40 +0200 ZF/Zorn/next_bounded: deleted this proof, which was already in comments
lcp [Fri, 09 Sep 1994 11:40:40 +0200] rev 593
ZF/Zorn/next_bounded: deleted this proof, which was already in comments
Thu, 08 Sep 1994 13:17:57 +0200 documentation on theories
lcp [Thu, 08 Sep 1994 13:17:57 +0200] rev 592
documentation on theories
Thu, 08 Sep 1994 12:55:50 +0200 ZF/add_ind_def/add_fp_def_i: now prints the fixedpoint defs at the terminal
lcp [Thu, 08 Sep 1994 12:55:50 +0200] rev 591
ZF/add_ind_def/add_fp_def_i: now prints the fixedpoint defs at the terminal
Thu, 08 Sep 1994 11:05:06 +0200 {HOL,ZF}/indrule/quant_induct: replaced ssubst in eresolve_tac by
lcp [Thu, 08 Sep 1994 11:05:06 +0200] rev 590
{HOL,ZF}/indrule/quant_induct: replaced ssubst in eresolve_tac by separate call to hyp_subst_tac. This avoids substituting in x=f(x) {HOL,ZF}/indrule/ind_tac: now tries resolve_tac [refl]. This handles trivial equalities such as x=a. {HOL,ZF}/intr_elim/intro_tacsf_tac: now calls assume_tac last, to try refl before any equality assumptions
Wed, 07 Sep 1994 17:28:53 +0200 addition of ZF/ex/twos_compl.thy
lcp [Wed, 07 Sep 1994 17:28:53 +0200] rev 589
addition of ZF/ex/twos_compl.thy
Wed, 07 Sep 1994 13:04:28 +0200 moved from Contrib
clasohm [Wed, 07 Sep 1994 13:04:28 +0200] rev 588
moved from Contrib
Wed, 07 Sep 1994 10:43:30 +0200 renamed temporary variable 'base' to 'thy' in mk_structure
clasohm [Wed, 07 Sep 1994 10:43:30 +0200] rev 587
renamed temporary variable 'base' to 'thy' in mk_structure
Tue, 06 Sep 1994 14:44:10 +0200 renamed base_on into mk_base and moved it to the beginning of the generated
clasohm [Tue, 06 Sep 1994 14:44:10 +0200] rev 586
renamed base_on into mk_base and moved it to the beginning of the generated .thy.ML file to make sure that all base theories are present when ML executes the rest of this file
Tue, 06 Sep 1994 13:46:53 +0200 Pure/type/unvarifyT: moved there from logic.ML
lcp [Tue, 06 Sep 1994 13:46:53 +0200] rev 585
Pure/type/unvarifyT: moved there from logic.ML
Tue, 06 Sep 1994 13:28:56 +0200 documentation of theory sections (co)inductive and (co)datatype
lcp [Tue, 06 Sep 1994 13:28:56 +0200] rev 584
documentation of theory sections (co)inductive and (co)datatype
Tue, 06 Sep 1994 13:10:38 +0200 minor internal changes;
wenzelm [Tue, 06 Sep 1994 13:10:38 +0200] rev 583
minor internal changes;
Tue, 06 Sep 1994 13:09:58 +0200 added ext_tsig_types;
wenzelm [Tue, 06 Sep 1994 13:09:58 +0200] rev 582
added ext_tsig_types; various minor changes;
Tue, 06 Sep 1994 11:02:16 +0200 removal of needless quotes
lcp [Tue, 06 Sep 1994 11:02:16 +0200] rev 581
removal of needless quotes
Wed, 31 Aug 1994 17:34:12 +0200 Updated datatype documentation with a few hints
nipkow [Wed, 31 Aug 1994 17:34:12 +0200] rev 580
Updated datatype documentation with a few hints
Thu, 25 Aug 1994 12:21:00 +0200 new file of useful things for writing theory sections
lcp [Thu, 25 Aug 1994 12:21:00 +0200] rev 579
new file of useful things for writing theory sections
Thu, 25 Aug 1994 12:09:21 +0200 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp [Thu, 25 Aug 1994 12:09:21 +0200] rev 578
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without the keyword "inductive" making the theory file fail ZF/Makefile: now has Inductive.thy,.ML ZF/Datatype,Finite,Zorn: depend upon Inductive ZF/intr_elim: now checks that the inductive name does not clash with existing theory names ZF/ind_section: deleted things replicated in Pure/section_utils.ML ZF/ROOT: now loads Pure/section_utils
Thu, 25 Aug 1994 10:41:17 +0200 print_sign_exn: now exported, with a polymorphic type
lcp [Thu, 25 Aug 1994 10:41:17 +0200] rev 577
print_sign_exn: now exported, with a polymorphic type
Wed, 24 Aug 1994 15:48:47 +0200 ZF/ex/LList/lconst_type: streamlined proof
lcp [Wed, 24 Aug 1994 15:48:47 +0200] rev 576
ZF/ex/LList/lconst_type: streamlined proof
Tue, 23 Aug 1994 19:34:01 +0200 added print_syntax: theory -> unit;
wenzelm [Tue, 23 Aug 1994 19:34:01 +0200] rev 575
added print_syntax: theory -> unit;
Tue, 23 Aug 1994 19:33:33 +0200 read_def_cterm: minor changes;
wenzelm [Tue, 23 Aug 1994 19:33:33 +0200] rev 574
read_def_cterm: minor changes; merge_thm_sgs: improved error msg;
Tue, 23 Aug 1994 19:31:05 +0200 removed constant _constrain from Pure sig;
wenzelm [Tue, 23 Aug 1994 19:31:05 +0200] rev 573
removed constant _constrain from Pure sig;
Mon, 22 Aug 1994 11:27:23 +0200 ZF/upair/consE', UnE': new
lcp [Mon, 22 Aug 1994 11:27:23 +0200] rev 572
ZF/upair/consE', UnE': new
Mon, 22 Aug 1994 11:11:17 +0200 ZF/Cardinal: some results moved here from CardinalArith
lcp [Mon, 22 Aug 1994 11:11:17 +0200] rev 571
ZF/Cardinal: some results moved here from CardinalArith ZF/CardinalArith/nat_succ_lepoll: removed obsolete proof ZF/CardinalArith/nat_cons_eqpoll: new
Mon, 22 Aug 1994 11:07:40 +0200 Pure/Thy/thy_parse/THY_PARSE: deleted duplicate specifications of parens,
lcp [Mon, 22 Aug 1994 11:07:40 +0200] rev 570
Pure/Thy/thy_parse/THY_PARSE: deleted duplicate specifications of parens, brackets, ..., mk_triple
Mon, 22 Aug 1994 11:03:52 +0200 HOLCF/Lift1.thy: now imports Sum
lcp [Mon, 22 Aug 1994 11:03:52 +0200] rev 569
HOLCF/Lift1.thy: now imports Sum
Fri, 19 Aug 1994 16:13:53 +0200 replaced Lexicon.scan_id by Scanner.scan_id;
wenzelm [Fri, 19 Aug 1994 16:13:53 +0200] rev 568
replaced Lexicon.scan_id by Scanner.scan_id; replaced const_name by Syntax.const_name;
Fri, 19 Aug 1994 16:12:23 +0200 replaced add_defns_i by add_defs_i;
wenzelm [Fri, 19 Aug 1994 16:12:23 +0200] rev 567
replaced add_defns_i by add_defs_i;
Fri, 19 Aug 1994 16:09:27 +0200 replaced sextension.ML by syn_trans.ML;
wenzelm [Fri, 19 Aug 1994 16:09:27 +0200] rev 566
replaced sextension.ML by syn_trans.ML;
Fri, 19 Aug 1994 15:42:13 +0200 slightly changed args of infer_types;
wenzelm [Fri, 19 Aug 1994 15:42:13 +0200] rev 565
slightly changed args of infer_types; replaced parents by enclose; renamed 2nd add_types to attach_types and fixed the typevar-sort-constraint BUG; various minor internal changes;
Fri, 19 Aug 1994 15:41:39 +0200 added inferT_axm;
wenzelm [Fri, 19 Aug 1994 15:41:39 +0200] rev 564
added inferT_axm; removed extend_theory; changed read_def_cterm: now uses Sign.infer_types;
Fri, 19 Aug 1994 15:41:00 +0200 replaced mapst by map;
wenzelm [Fri, 19 Aug 1994 15:41:00 +0200] rev 563
replaced mapst by map; added find_first;
Fri, 19 Aug 1994 15:40:44 +0200 added pretty_sg;
wenzelm [Fri, 19 Aug 1994 15:40:44 +0200] rev 562
added pretty_sg; added infer_types; removed subclasses arg of add_classes; removed old 'extend' and related stuff; various minor internal changes;
Fri, 19 Aug 1994 15:40:10 +0200 added add_defs, add_defs_i;
wenzelm [Fri, 19 Aug 1994 15:40:10 +0200] rev 561
added add_defs, add_defs_i;
Fri, 19 Aug 1994 15:39:52 +0200 cleaned sig;
wenzelm [Fri, 19 Aug 1994 15:39:52 +0200] rev 560
cleaned sig; removed add_defns (now in drule.ML as add_defs); removed add_sigclass; minor internal changes;
Fri, 19 Aug 1994 15:39:19 +0200 added theory_of_sign, theory_of_thm;
wenzelm [Fri, 19 Aug 1994 15:39:19 +0200] rev 559
added theory_of_sign, theory_of_thm; renamed get_thms to thms_of; improved store_thms etc.;
Fri, 19 Aug 1994 15:38:50 +0200 renamed 'defns' to 'defs';
wenzelm [Fri, 19 Aug 1994 15:38:50 +0200] rev 558
renamed 'defns' to 'defs'; removed 'sigclass'; replaced parents by enclose; exported parens, brackets, mk_list, mk_big_list, mk_pair, mk_triple; various minor internal changes;
Fri, 19 Aug 1994 15:38:18 +0200 added raw_term_sorts and changed typ_of_term accordingly (part of fix
wenzelm [Fri, 19 Aug 1994 15:38:18 +0200] rev 557
added raw_term_sorts and changed typ_of_term accordingly (part of fix of the typevar-sort-constraint BUG); various minor internal changes;
Fri, 19 Aug 1994 15:37:46 +0200 added type xrule (from sextension.ML);
wenzelm [Fri, 19 Aug 1994 15:37:46 +0200] rev 556
added type xrule (from sextension.ML); removed old 'extend'; removed added syn_ext_const_names, syn_ext_trfuns (now in syn_ext.ML); various minor changes;
Fri, 19 Aug 1994 15:37:24 +0200 removed idT, varT, tidT, tvarT (now in lexicon.ML);
wenzelm [Fri, 19 Aug 1994 15:37:24 +0200] rev 555
removed idT, varT, tidT, tvarT (now in lexicon.ML); added syn_ext_const_names, syn_ext_trfuns;
Fri, 19 Aug 1994 15:37:05 +0200 various minor internal changes;
wenzelm [Fri, 19 Aug 1994 15:37:05 +0200] rev 554
various minor internal changes;
Fri, 19 Aug 1994 15:36:45 +0200 added map_strs: (string -> string) -> T -> T;
wenzelm [Fri, 19 Aug 1994 15:36:45 +0200] rev 553
added map_strs: (string -> string) -> T -> T;
Fri, 19 Aug 1994 15:36:23 +0200 removed roots arg of extend_gram;
wenzelm [Fri, 19 Aug 1994 15:36:23 +0200] rev 552
removed roots arg of extend_gram; added functor sig constraint (: PARSER);
Fri, 19 Aug 1994 15:35:56 +0200 minor cleanings;
wenzelm [Fri, 19 Aug 1994 15:35:56 +0200] rev 551
minor cleanings;
Fri, 19 Aug 1994 15:35:38 +0200 replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm [Fri, 19 Aug 1994 15:35:38 +0200] rev 550
replaced id, var, tid, tvar by idT, varT, tidT, tvarT; added const, free, var: build atomic terms of dummyT; added 'xnum' (signed numerals) and 'xstr' (strings) token kinds; various minor internal changes;
Fri, 19 Aug 1994 15:34:58 +0200 replaced SExtension by SynTrans (mixfix stuff in Mixfix);
wenzelm [Fri, 19 Aug 1994 15:34:58 +0200] rev 549
replaced SExtension by SynTrans (mixfix stuff in Mixfix); private structs now hidden within PrivateSyntax;
Fri, 19 Aug 1994 15:34:28 +0200 added this file;
wenzelm [Fri, 19 Aug 1994 15:34:28 +0200] rev 548
added this file;
Fri, 19 Aug 1994 10:57:40 +0200 deleted obsolete references to ISABELLEMAKE
lcp [Fri, 19 Aug 1994 10:57:40 +0200] rev 547
deleted obsolete references to ISABELLEMAKE
Thu, 18 Aug 1994 17:56:07 +0200 /unvarifyT, unvarify: moved to Pure/logic.ML
lcp [Thu, 18 Aug 1994 17:56:07 +0200] rev 546
/unvarifyT, unvarify: moved to Pure/logic.ML
Thu, 18 Aug 1994 17:53:28 +0200 Pure/goals.ML: prove_goalw_cterm now does its own exception-handling, moved
lcp [Thu, 18 Aug 1994 17:53:28 +0200] rev 545
Pure/goals.ML: prove_goalw_cterm now does its own exception-handling, moved from prove_goalw
Thu, 18 Aug 1994 17:50:22 +0200 Pure/library/assert_all: new, moved from ZF/ind_syntax.ML
lcp [Thu, 18 Aug 1994 17:50:22 +0200] rev 544
Pure/library/assert_all: new, moved from ZF/ind_syntax.ML
Thu, 18 Aug 1994 17:41:40 +0200 ZF/ind_syntax/unvarifyT, unvarify: moved to Pure/logic.ML
lcp [Thu, 18 Aug 1994 17:41:40 +0200] rev 543
ZF/ind_syntax/unvarifyT, unvarify: moved to Pure/logic.ML ZF/ind_syntax/prove_term: deleted ZF/constructor, indrule, intr_elim: now call prove_goalw_cterm and Logic.unvarify
Thu, 18 Aug 1994 12:56:57 +0200 HOLCF/Lift1.thy: updated for new sum_case by using "case" syntax
lcp [Thu, 18 Aug 1994 12:56:57 +0200] rev 542
HOLCF/Lift1.thy: updated for new sum_case by using "case" syntax
Wed, 17 Aug 1994 10:42:41 +0200 overheads for inductive definitions, originally for CADE-12
lcp [Wed, 17 Aug 1994 10:42:41 +0200] rev 541
overheads for inductive definitions, originally for CADE-12
Wed, 17 Aug 1994 10:38:37 +0200 ZF/ex/ROOT: added .ML to use command use "ex/twos_compl"
lcp [Wed, 17 Aug 1994 10:38:37 +0200] rev 540
ZF/ex/ROOT: added .ML to use command use "ex/twos_compl" Should be able to delete this after fixing the treatment of orphans.
Wed, 17 Aug 1994 10:34:44 +0200 ZF/ex/Ntree: two new examples, maptree and maptree2
lcp [Wed, 17 Aug 1994 10:34:44 +0200] rev 539
ZF/ex/Ntree: two new examples, maptree and maptree2
Wed, 17 Aug 1994 10:33:23 +0200 ZF/func/fun_extend3: new
lcp [Wed, 17 Aug 1994 10:33:23 +0200] rev 538
ZF/func/fun_extend3: new ZF/func/cons_fun_eq: simplified proof
Wed, 17 Aug 1994 10:31:35 +0200 ZF/Univ/Sigma_subset_univ, Transset_Pair_subset_univ: deleted
lcp [Wed, 17 Aug 1994 10:31:35 +0200] rev 537
ZF/Univ/Sigma_subset_univ, Transset_Pair_subset_univ: deleted
Tue, 16 Aug 1994 19:09:43 +0200 ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
lcp [Tue, 16 Aug 1994 19:09:43 +0200] rev 536
ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where they can be proved trivially using eq_cs ZF/domrange/XXX_empty: renamed XXX_0
Tue, 16 Aug 1994 19:06:14 +0200 ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
lcp [Tue, 16 Aug 1994 19:06:14 +0200] rev 535
ZF/ex/Equiv.thy,.ML: moved to main directory as EquivClass.thy,.ML
Tue, 16 Aug 1994 19:03:45 +0200 ZF/Finite: added the finite function space, A-||>B
lcp [Tue, 16 Aug 1994 19:03:45 +0200] rev 534
ZF/Finite: added the finite function space, A-||>B ZF/InfDatatype: added rules for the above
Tue, 16 Aug 1994 19:01:26 +0200 ZF/pair.ML: moved some definitions here from simpdata.ML
lcp [Tue, 16 Aug 1994 19:01:26 +0200] rev 533
ZF/pair.ML: moved some definitions here from simpdata.ML
Tue, 16 Aug 1994 18:58:42 +0200 ZF/Makefile,ROOT.ML, ZF/ex/Integ.thy: updated for EquivClass
lcp [Tue, 16 Aug 1994 18:58:42 +0200] rev 532
ZF/Makefile,ROOT.ML, ZF/ex/Integ.thy: updated for EquivClass
Tue, 16 Aug 1994 18:53:29 +0200 ZF/Makefile,ROOT.ML, ZF/ex/Integ.thy: updated for EquivClass
lcp [Tue, 16 Aug 1994 18:53:29 +0200] rev 531
ZF/Makefile,ROOT.ML, ZF/ex/Integ.thy: updated for EquivClass
Mon, 15 Aug 1994 19:01:51 +0200 ZF/Makefile/FILES: added many missing .thy files
lcp [Mon, 15 Aug 1994 19:01:51 +0200] rev 530
ZF/Makefile/FILES: added many missing .thy files
Mon, 15 Aug 1994 18:38:38 +0200 ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
lcp [Mon, 15 Aug 1994 18:38:38 +0200] rev 529
ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
Mon, 15 Aug 1994 18:37:25 +0200 ZF/ex/Brouwer.thy,.ML: new example of wellordering types
lcp [Mon, 15 Aug 1994 18:37:25 +0200] rev 528
ZF/ex/Brouwer.thy,.ML: new example of wellordering types
Mon, 15 Aug 1994 18:31:29 +0200 ZF/ex/CoUnit/lleq_cs: copied from LList.ML
lcp [Mon, 15 Aug 1994 18:31:29 +0200] rev 527
ZF/ex/CoUnit/lleq_cs: copied from LList.ML
Mon, 15 Aug 1994 18:27:50 +0200 ZF/ex/ROOT: changed "time_use" to "time_use_thy" to load CoUnit;
lcp [Mon, 15 Aug 1994 18:27:50 +0200] rev 526
ZF/ex/ROOT: changed "time_use" to "time_use_thy" to load CoUnit; removed some explicit loads by exploiting theory dependencies
Mon, 15 Aug 1994 18:25:27 +0200 ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
lcp [Mon, 15 Aug 1994 18:25:27 +0200] rev 525
ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
Mon, 15 Aug 1994 18:15:09 +0200 ZF/InfDatatype: simplified, extended results for infinite branching
lcp [Mon, 15 Aug 1994 18:15:09 +0200] rev 524
ZF/InfDatatype: simplified, extended results for infinite branching
Mon, 15 Aug 1994 18:12:56 +0200 ZF/CardinalArith/InfCard_Un: new
lcp [Mon, 15 Aug 1994 18:12:56 +0200] rev 523
ZF/CardinalArith/InfCard_Un: new
Mon, 15 Aug 1994 18:11:00 +0200 ZF/Cardinal/Card_Un: new
lcp [Mon, 15 Aug 1994 18:11:00 +0200] rev 522
ZF/Cardinal/Card_Un: new
Mon, 15 Aug 1994 18:09:37 +0200 ZF/Sum/Sigma_bool: new
lcp [Mon, 15 Aug 1994 18:09:37 +0200] rev 521
ZF/Sum/Sigma_bool: new
Mon, 15 Aug 1994 18:07:03 +0200 ZF/equalities/Sigma_cons: new
lcp [Mon, 15 Aug 1994 18:07:03 +0200] rev 520
ZF/equalities/Sigma_cons: new ZF/equalities/cons_eq: new ZF/equalities.thy: added final newline
Mon, 15 Aug 1994 18:04:10 +0200 ZF/func/empty_fun: renamed from fun_empty
lcp [Mon, 15 Aug 1994 18:04:10 +0200] rev 519
ZF/func/empty_fun: renamed from fun_empty ZF/func/single_fun: replaces the weaker fun_single ZF/func/fun_single_lemma: deleted ZF/func.thy: now depends upon equalities.thy
Mon, 15 Aug 1994 16:12:35 +0200 Proof beautification
nipkow [Mon, 15 Aug 1994 16:12:35 +0200] rev 518
Proof beautification
Fri, 12 Aug 1994 18:45:33 +0200 for infinite datatypes with arbitrary index sets
lcp [Fri, 12 Aug 1994 18:45:33 +0200] rev 517
for infinite datatypes with arbitrary index sets
Fri, 12 Aug 1994 12:51:34 +0200 installation of new inductive/datatype sections
lcp [Fri, 12 Aug 1994 12:51:34 +0200] rev 516
installation of new inductive/datatype sections
Fri, 12 Aug 1994 12:28:46 +0200 installation of new inductive/datatype sections
lcp [Fri, 12 Aug 1994 12:28:46 +0200] rev 515
installation of new inductive/datatype sections
Fri, 12 Aug 1994 11:13:23 +0200 addition of string escapes
lcp [Fri, 12 Aug 1994 11:13:23 +0200] rev 514
addition of string escapes
Fri, 12 Aug 1994 11:01:18 +0200 updated reference to parents
lcp [Fri, 12 Aug 1994 11:01:18 +0200] rev 513
updated reference to parents
Fri, 12 Aug 1994 10:57:55 +0200 Pure/library/enclose, Pure/Syntax/pretty/enclose: renamed from parents
lcp [Fri, 12 Aug 1994 10:57:55 +0200] rev 512
Pure/library/enclose, Pure/Syntax/pretty/enclose: renamed from parents Pure/library/is_blank: now handles form feeds () too, in accordance with ML definition
Fri, 12 Aug 1994 10:20:07 +0200 re-organized using new theory sections
lcp [Fri, 12 Aug 1994 10:20:07 +0200] rev 511
re-organized using new theory sections
Mon, 08 Aug 1994 16:45:08 +0200 Simplified some proofs. Added some type assumptions to the introduction rules.
nipkow [Mon, 08 Aug 1994 16:45:08 +0200] rev 510
Simplified some proofs. Added some type assumptions to the introduction rules.
Thu, 04 Aug 1994 12:39:28 +0200 fixed spelling
lcp [Thu, 04 Aug 1994 12:39:28 +0200] rev 509
fixed spelling
Thu, 04 Aug 1994 11:51:30 +0200 addition of show_brackets
lcp [Thu, 04 Aug 1994 11:51:30 +0200] rev 508
addition of show_brackets
Thu, 04 Aug 1994 11:45:59 +0200 addition of show_brackets
lcp [Thu, 04 Aug 1994 11:45:59 +0200] rev 507
addition of show_brackets
Wed, 03 Aug 1994 09:45:42 +0200 improved show_brackets again - Trueprop does not create () any more.
nipkow [Wed, 03 Aug 1994 09:45:42 +0200] rev 506
improved show_brackets again - Trueprop does not create () any more.
Tue, 02 Aug 1994 20:08:57 +0200 minimized () in forced printing of barckets (show_brackets)
nipkow [Tue, 02 Aug 1994 20:08:57 +0200] rev 505
minimized () in forced printing of barckets (show_brackets)
Tue, 02 Aug 1994 09:07:10 +0200 added flag show_brackets for printinmg fully bracketed terms.
nipkow [Tue, 02 Aug 1994 09:07:10 +0200] rev 504
added flag show_brackets for printinmg fully bracketed terms.
Mon, 01 Aug 1994 17:34:57 +0200 trivial whitespace change
lcp [Mon, 01 Aug 1994 17:34:57 +0200] rev 503
trivial whitespace change
Mon, 01 Aug 1994 17:24:46 +0200 ZF/Perm.ML/inj_converse_inj, comp_inj: simpler proofs using f_imp_injective
lcp [Mon, 01 Aug 1994 17:24:46 +0200] rev 502
ZF/Perm.ML/inj_converse_inj, comp_inj: simpler proofs using f_imp_injective many other tidies
Fri, 29 Jul 1994 16:07:22 +0200 ZF/ex/PropLog/sat_XXX: renamed logcon_XXX, since the relation is logical
lcp [Fri, 29 Jul 1994 16:07:22 +0200] rev 501
ZF/ex/PropLog/sat_XXX: renamed logcon_XXX, since the relation is logical consequence rather than satisfaction
(0) -120 +120 +1000 +3000 +10000 +30000 tip