wenzelm [Wed, 12 Apr 2000 23:51:57 +0200] rev 8695
export concl_of;
induct method: admit "_";
wenzelm [Wed, 12 Apr 2000 23:49:10 +0200] rev 8694
tuned \isasymlbrace;
wenzelm [Wed, 12 Apr 2000 23:47:47 +0200] rev 8693
'insts' syntax;
'insert' method;
wenzelm [Wed, 12 Apr 2000 23:46:06 +0200] rev 8692
improved 'induct(_tac)' syntax;
wenzelm [Wed, 12 Apr 2000 23:45:21 +0200] rev 8691
added 'insert' method;
wenzelm [Wed, 12 Apr 2000 23:45:01 +0200] rev 8690
added inst, insts;
wenzelm [Wed, 12 Apr 2000 18:53:20 +0200] rev 8689
improved induct_tac;
wenzelm [Wed, 12 Apr 2000 18:53:09 +0200] rev 8688
induct stripped: match_tac;
wenzelm [Wed, 12 Apr 2000 18:47:03 +0200] rev 8687
Args.name_dummy;
wenzelm [Wed, 12 Apr 2000 15:40:19 +0200] rev 8686
fixed 'induct_tac' syntax;
wenzelm [Mon, 10 Apr 2000 23:38:02 +0200] rev 8685
handle dir prefix;
wenzelm [Mon, 10 Apr 2000 23:36:19 +0200] rev 8684
improved document preparation;
wenzelm [Sat, 08 Apr 2000 19:38:19 +0200] rev 8683
fixed comment;
wenzelm [Fri, 07 Apr 2000 17:36:56 +0200] rev 8682
added 'ML_command';
'apply' etc.: comments;
wenzelm [Fri, 07 Apr 2000 17:36:25 +0200] rev 8681
apply etc.: comments;
wenzelm [Thu, 06 Apr 2000 19:11:30 +0200] rev 8680
tuned \isasymlbrace;
wenzelm [Thu, 06 Apr 2000 17:05:38 +0200] rev 8679
added \isasymlbrace, \isasymrbrace, \isasymtop;
wenzelm [Thu, 06 Apr 2000 13:39:49 +0200] rev 8678
'welcome' made diagnostic;
wenzelm [Wed, 05 Apr 2000 21:08:24 +0200] rev 8677
added Isar_examples/NestedDatatype.thy;
wenzelm [Wed, 05 Apr 2000 21:07:09 +0200] rev 8676
added NestedDatatype.thy;
wenzelm [Wed, 05 Apr 2000 21:06:52 +0200] rev 8675
added NestedDatatype;
wenzelm [Wed, 05 Apr 2000 21:06:37 +0200] rev 8674
fixed goal selection;
wenzelm [Wed, 05 Apr 2000 21:06:06 +0200] rev 8673
Isar: simplified (more robust) goal selection of proof methods;
Isar: tuned 'let' syntax: replace 'as' keyword by 'and';
wenzelm [Wed, 05 Apr 2000 21:05:20 +0200] rev 8672
induct/case_tac emulation: optional rule;
add_cases_induct: fixed case names;
wenzelm [Wed, 05 Apr 2000 21:02:31 +0200] rev 8671
HEADGOAL;
wenzelm [Wed, 05 Apr 2000 21:02:19 +0200] rev 8670
tuned comment;
wenzelm [Wed, 05 Apr 2000 21:01:59 +0200] rev 8669
removed "as" keyword;
wenzelm [Wed, 05 Apr 2000 21:01:33 +0200] rev 8668
suppress warning;
wenzelm [Tue, 04 Apr 2000 22:16:11 +0200] rev 8667
print_simpset / print_claset command;
wenzelm [Tue, 04 Apr 2000 18:08:08 +0200] rev 8666
case_tac / induct_tac: optional rule;
wenzelm [Tue, 04 Apr 2000 12:32:02 +0200] rev 8665
case_tac, induct_tac;
wenzelm [Tue, 04 Apr 2000 12:31:48 +0200] rev 8664
'let': replaced 'as' by 'and';
wenzelm [Mon, 03 Apr 2000 21:05:07 +0200] rev 8663
tuned recover;
wenzelm [Mon, 03 Apr 2000 14:02:40 +0200] rev 8662
isapar, isamarkuptext, isamarkuptxt turned into environments;
wenzelm [Mon, 03 Apr 2000 14:00:39 +0200] rev 8661
markup_env_command 'text' / 'txt';
wenzelm [Mon, 03 Apr 2000 14:00:16 +0200] rev 8660
support markup environments;
wenzelm [Sat, 01 Apr 2000 20:26:20 +0200] rev 8659
tuned presentation;
wenzelm [Sat, 01 Apr 2000 20:22:46 +0200] rev 8658
proper naming of fib equations;
wenzelm [Sat, 01 Apr 2000 20:21:39 +0200] rev 8657
recdef: admit names/atts;
wenzelm [Sat, 01 Apr 2000 20:18:52 +0200] rev 8656
isatool document: tuned -c option;
wenzelm [Sat, 01 Apr 2000 20:17:51 +0200] rev 8655
recdef: admit name and atts;
wenzelm [Sat, 01 Apr 2000 20:16:56 +0200] rev 8654
tuned -c option;
wenzelm [Sat, 01 Apr 2000 20:15:55 +0200] rev 8653
recover: observe stopper;
wenzelm [Sat, 01 Apr 2000 20:13:33 +0200] rev 8652
presentation ignore stuff: swallow newline;
wenzelm [Sat, 01 Apr 2000 20:12:52 +0200] rev 8651
added is_newline;
wenzelm [Sat, 01 Apr 2000 20:12:15 +0200] rev 8650
'cd': diag;
wenzelm [Sat, 01 Apr 2000 20:11:50 +0200] rev 8649
more robust handling of explicit rules;
wenzelm [Sat, 01 Apr 2000 20:10:57 +0200] rev 8648
tuned mixfix syntax;
wenzelm [Sat, 01 Apr 2000 20:09:52 +0200] rev 8647
added ProofGeneral.undo;
wenzelm [Sat, 01 Apr 2000 20:09:20 +0200] rev 8646
isatool document: check output file (workaround PolyML problem with RC);
wenzelm [Fri, 31 Mar 2000 22:39:39 +0200] rev 8645
use cong_add_global att;
wenzelm [Fri, 31 Mar 2000 22:39:06 +0200] rev 8644
added cong atts;
wenzelm [Fri, 31 Mar 2000 22:22:23 +0200] rev 8643
added cong atts;
wenzelm [Fri, 31 Mar 2000 22:01:01 +0200] rev 8642
made SML/XL happy;
wenzelm [Fri, 31 Mar 2000 22:00:36 +0200] rev 8641
change_global/local_css move to Provers/clasimp.ML;
fixed 'iff' att syntax;
added 'cong' att;
wenzelm [Fri, 31 Mar 2000 21:59:37 +0200] rev 8640
setup cong_attrib_setup;
wenzelm [Fri, 31 Mar 2000 21:58:34 +0200] rev 8639
added change_global/local_css;
wenzelm [Fri, 31 Mar 2000 21:57:14 +0200] rev 8638
added 'cong' att;
fixed 'iff' syntax;
wenzelm [Fri, 31 Mar 2000 21:56:23 +0200] rev 8637
tuned;
wenzelm [Fri, 31 Mar 2000 21:56:13 +0200] rev 8636
params: preserve case names;
wenzelm [Fri, 31 Mar 2000 21:55:51 +0200] rev 8635
fixed indexing of elim rules;
wenzelm [Fri, 31 Mar 2000 21:55:27 +0200] rev 8634
use Attrib.add_del_args;
wenzelm [Fri, 31 Mar 2000 21:54:50 +0200] rev 8633
added add_del_args;
wenzelm [Fri, 31 Mar 2000 18:10:21 +0200] rev 8632
fixed goal syntax;
nipkow [Fri, 31 Mar 2000 10:23:15 +0200] rev 8631
comments modified
kleing [Fri, 31 Mar 2000 10:17:32 +0200] rev 8630
tuned
kleing [Fri, 31 Mar 2000 10:15:33 +0200] rev 8629
included new stanford mirror, mirror links now point to source directly
nipkow [Fri, 31 Mar 2000 10:08:26 +0200] rev 8628
updated recdef
wenzelm [Thu, 30 Mar 2000 21:26:10 +0200] rev 8627
tuned;
nipkow [Thu, 30 Mar 2000 20:06:27 +0200] rev 8626
recdef
nipkow [Thu, 30 Mar 2000 19:47:17 +0200] rev 8625
If all termination conditions are proved automatically,
the recusrion equations are added to the simpset automatically.
recdef.rules -> recdef.simps
nipkow [Thu, 30 Mar 2000 19:45:51 +0200] rev 8624
recdef.rules -> recdef.simps
nipkow [Thu, 30 Mar 2000 19:45:18 +0200] rev 8623
mod in recdef allows to access the correct simpset via simpset().
nipkow [Thu, 30 Mar 2000 19:44:11 +0200] rev 8622
the simplification rules returned from TFL are now paired with the row they
came from.
wenzelm [Thu, 30 Mar 2000 15:13:59 +0200] rev 8621
* Isar/Pure: local results and corresponding term bindings are now
subject to Hindley-Milner polymorphism (similar to ML); this
accommodates incremental type-inference nicely;
* Isar/Pure: new calculational elements 'moreover' and 'ultimately'
support plain accumulation of results, without applying any rules yet;
wenzelm [Thu, 30 Mar 2000 15:13:02 +0200] rev 8620
support Hindley-Milner polymorphisms in results and bindings;
wenzelm [Thu, 30 Mar 2000 15:12:20 +0200] rev 8619
added 'moreover' and 'ultimately';
wenzelm [Thu, 30 Mar 2000 15:11:48 +0200] rev 8618
added \MOREOVER, \ULTIMATELY;
wenzelm [Thu, 30 Mar 2000 14:28:54 +0200] rev 8617
support Hindley-Milner polymorphisms in binds and facts;
let_bind(_i): polymorphic version;
moved find_free, export_wrt to Isar/proof_context.ML;
wenzelm [Thu, 30 Mar 2000 14:28:10 +0200] rev 8616
support Hindley-Milner polymorphisms in binds and facts;
let_bind(_i): polymorphic version;
improved warn_extra_tfrees;
added find_free, export_wrt (from Isar/proof.ML);
wenzelm [Thu, 30 Mar 2000 14:25:35 +0200] rev 8615
let_bind(_i): polymorphic version;
wenzelm [Thu, 30 Mar 2000 14:24:46 +0200] rev 8614
ProofContext.find_free;
wenzelm [Thu, 30 Mar 2000 14:22:15 +0200] rev 8613
'tactic': refer to PureIsar structure;
wenzelm [Thu, 30 Mar 2000 14:21:28 +0200] rev 8612
?this: support params;
wenzelm [Thu, 30 Mar 2000 14:20:42 +0200] rev 8611
support polymorphic Vars;
wenzelm [Thu, 30 Mar 2000 14:20:13 +0200] rev 8610
tuned;
wenzelm [Thu, 30 Mar 2000 14:20:01 +0200] rev 8609
foldl_term_types: depend on term as well;
wenzelm [Thu, 30 Mar 2000 14:19:33 +0200] rev 8608
read_def_cterms: use Sign.read_def_terms;
wenzelm [Thu, 30 Mar 2000 14:19:13 +0200] rev 8607
read_def_terms (no certify yet);
wenzelm [Thu, 30 Mar 2000 14:18:40 +0200] rev 8606
export update_multi;
wenzelm [Thu, 30 Mar 2000 14:15:41 +0200] rev 8605
added tvars_intr_list;
nipkow [Wed, 29 Mar 2000 15:09:51 +0200] rev 8604
*** empty log message ***
nipkow [Wed, 29 Mar 2000 14:23:27 +0200] rev 8603
*** empty log message ***
nipkow [Tue, 28 Mar 2000 17:33:44 +0200] rev 8602
mods because of weak_case_cong -> removed Action.ML twice
nipkow [Tue, 28 Mar 2000 17:32:24 +0200] rev 8601
added weak_case_cong feature
nipkow [Tue, 28 Mar 2000 17:31:36 +0200] rev 8600
mods because of weak_case_cong
wenzelm [Tue, 28 Mar 2000 12:28:24 +0200] rev 8599
fixed railqtoken;
wenzelm [Tue, 28 Mar 2000 11:50:23 +0200] rev 8598
-I option;
wenzelm [Mon, 27 Mar 2000 21:41:19 +0200] rev 8597
renamed 'hoare_vcg' to 'hoare';
wenzelm [Mon, 27 Mar 2000 21:13:23 +0200] rev 8596
tuned;
wenzelm [Mon, 27 Mar 2000 21:13:06 +0200] rev 8595
fixed dddot_tr;
wenzelm [Mon, 27 Mar 2000 18:10:11 +0200] rev 8594
rail token vs. terminal;
wenzelm [Mon, 27 Mar 2000 18:09:49 +0200] rev 8593
fixed term syntax;
wenzelm [Mon, 27 Mar 2000 18:09:24 +0200] rev 8592
tail token vs. terminal;
wenzelm [Mon, 27 Mar 2000 18:08:57 +0200] rev 8591
fixed \rail@tokenfont (ever used?);
paulson [Mon, 27 Mar 2000 17:04:03 +0200] rev 8590
added an order-sorted version of quickSort
paulson [Mon, 27 Mar 2000 16:25:53 +0200] rev 8589
simplified constant "colored"
wenzelm [Sun, 26 Mar 2000 22:31:11 +0200] rev 8588
added 'ultimately';
wenzelm [Sun, 26 Mar 2000 22:29:33 +0200] rev 8587
added WhileRule';
tuned;
wenzelm [Sun, 26 Mar 2000 20:38:23 +0200] rev 8586
made SML/NJ happy;
wenzelm [Sun, 26 Mar 2000 20:17:52 +0200] rev 8585
tuned presentation;
wenzelm [Sun, 26 Mar 2000 20:16:34 +0200] rev 8584
tuned;
wenzelm [Sun, 26 Mar 2000 20:13:53 +0200] rev 8583
ignore_stuff;
P.!!!!;
wenzelm [Sun, 26 Mar 2000 20:12:28 +0200] rev 8582
tuned output;
wenzelm [Sun, 26 Mar 2000 20:11:12 +0200] rev 8581
!!!! = cut "Corrupted outer syntax in presentation";
wenzelm [Sun, 26 Mar 2000 20:10:31 +0200] rev 8580
added is_begin/end_ignore;
wenzelm [Sun, 26 Mar 2000 20:08:03 +0200] rev 8579
tuned targets;
wenzelm [Sat, 25 Mar 2000 18:01:27 +0100] rev 8578
tuned;
wenzelm [Sat, 25 Mar 2000 17:59:52 +0100] rev 8577
improved (anti)quote_tr(');
wenzelm [Sat, 25 Mar 2000 13:00:44 +0100] rev 8576
addsimprocs [record_simproc];