wenzelm [Mon, 06 Oct 1997 18:43:32 +0200] rev 3787
new internal forms: add_classes_i, add_classrel_i, add_defsort_i, add_arities_i
added add_path, add_space;
eliminated raise_term;
wenzelm [Mon, 06 Oct 1997 18:41:39 +0200] rev 3786
tuned;
wenzelm [Mon, 06 Oct 1997 18:41:09 +0200] rev 3785
now uses new Sign.pretty_sort;
wenzelm [Mon, 06 Oct 1997 18:40:24 +0200] rev 3784
eliminated raise_term, raise_typ;
wenzelm [Mon, 06 Oct 1997 18:39:54 +0200] rev 3783
now uses Syntax.simple_str_of_sort;
wenzelm [Mon, 06 Oct 1997 18:39:25 +0200] rev 3782
added simple_str_of_sort;
wenzelm [Mon, 06 Oct 1997 18:29:43 +0200] rev 3781
eliminated raise_term;
wenzelm [Mon, 06 Oct 1997 18:29:11 +0200] rev 3780
added 'path' section;
root path at end;
wenzelm [Mon, 06 Oct 1997 18:27:55 +0200] rev 3779
added pretty_sort;
tuned read_typ;
tuned pretty_term;
removed string_of_term, string_of_typ;
wenzelm [Mon, 06 Oct 1997 18:25:04 +0200] rev 3778
fixed raw_term_sorts (again!);
eliminated raise_ast;
wenzelm [Mon, 06 Oct 1997 18:23:13 +0200] rev 3777
eliminated raise_ast, raise_term, raise_typ;
wenzelm [Mon, 06 Oct 1997 18:22:22 +0200] rev 3776
added sort_to_ast;
eliminated raise_ast;
wenzelm [Mon, 06 Oct 1997 18:21:00 +0200] rev 3775
eliminated raise_ast;
wenzelm [Mon, 06 Oct 1997 18:20:15 +0200] rev 3774
RAW target;
wenzelm [Mon, 06 Oct 1997 09:26:00 +0200] rev 3773
syntactic constants;
paulson [Fri, 03 Oct 1997 10:32:50 +0200] rev 3772
Routine tidying up
wenzelm [Thu, 02 Oct 1997 22:54:00 +0200] rev 3771
fully qualified names: Theory.add_XXX;
wenzelm [Wed, 01 Oct 1997 18:19:44 +0200] rev 3770
fully qualified name: Theory.set_oracle;
wenzelm [Wed, 01 Oct 1997 18:19:18 +0200] rev 3769
exported separator;
wenzelm [Wed, 01 Oct 1997 18:13:41 +0200] rev 3768
fully qualified names: Theory.add_XXX;
wenzelm [Wed, 01 Oct 1997 17:43:42 +0200] rev 3767
moved theory stuff (add_defs etc.) here from drule.ML;
only BasicTheory opened;
wenzelm [Wed, 01 Oct 1997 17:42:32 +0200] rev 3766
moved theory stuff (add_defs etc.) to theory.ML;
wenzelm [Wed, 01 Oct 1997 17:41:20 +0200] rev 3765
fully qualified name: Theory.merge_thy_list;
wenzelm [Wed, 01 Oct 1997 17:40:09 +0200] rev 3764
fully qualified names: Theory.add_XXX;
wenzelm [Wed, 01 Oct 1997 17:36:51 +0200] rev 3763
added name_space.ML;
wenzelm [Wed, 01 Oct 1997 17:32:38 +0200] rev 3762
added split_last;
wenzelm [Wed, 01 Oct 1997 14:30:38 +0200] rev 3761
Hierarchically structured name spaces.
paulson [Wed, 01 Oct 1997 13:42:18 +0200] rev 3760
Strengthened the possibility property for resumption so that it could have
detected the problem with ServerResume
paulson [Wed, 01 Oct 1997 13:41:38 +0200] rev 3759
Fixed ServerResume to check for ServerHello instead of making a new NB
paulson [Wed, 01 Oct 1997 12:07:24 +0200] rev 3758
Exchanged the M and SID fields of the FINISHED messages to simplify proofs;
deleted unused theorems
paulson [Wed, 01 Oct 1997 12:07:07 +0200] rev 3757
Exchanged the M and SID fields of the FINISHED messages to simplify proofs
paulson [Wed, 01 Oct 1997 11:30:55 +0200] rev 3756
Auto update
berghofe [Tue, 30 Sep 1997 17:33:16 +0200] rev 3755
SYNC
berghofe [Tue, 30 Sep 1997 17:32:33 +0200] rev 3754
Removed "browse.tex".
berghofe [Tue, 30 Sep 1997 17:31:19 +0200] rev 3753
Added section describing the theory browser.
berghofe [Tue, 30 Sep 1997 17:29:32 +0200] rev 3752
Updated usage information for tool "usedir".
berghofe [Tue, 30 Sep 1997 17:28:54 +0200] rev 3751
Theory browser stuff has been moved to "present.tex".
wenzelm [Tue, 30 Sep 1997 16:19:27 +0200] rev 3750
obsolete;
wenzelm [Tue, 30 Sep 1997 16:12:38 +0200] rev 3749
ISABELLE_USEDIR_OPTIONS="-i true"
berghofe [Tue, 30 Sep 1997 12:53:54 +0200] rev 3748
Changed html data directory and names of graph files.
berghofe [Tue, 30 Sep 1997 12:52:15 +0200] rev 3747
There is now one single option -i for generating theory browsing
information instead of the two options -h and -g .
berghofe [Tue, 30 Sep 1997 12:49:16 +0200] rev 3746
Modified some links.
paulson [Tue, 30 Sep 1997 11:03:55 +0200] rev 3745
Client, Server certificates now sent using the separate Certificate rule,
simplifying ServerHello and ClientKeyExch. Resumption no longer needs its
own version of ServerHello. Proofs run nearly three minutes faster.
wenzelm [Mon, 29 Sep 1997 15:39:28 +0200] rev 3744
tuned;
wenzelm [Mon, 29 Sep 1997 15:16:22 +0200] rev 3743
superficial;
wenzelm [Mon, 29 Sep 1997 15:11:27 +0200] rev 3742
obsolete;
wenzelm [Mon, 29 Sep 1997 15:08:47 +0200] rev 3741
margin 76 (2nd try :-);
wenzelm [Mon, 29 Sep 1997 14:12:02 +0200] rev 3740
fixed href to html library;
wenzelm [Mon, 29 Sep 1997 14:11:18 +0200] rev 3739
improved warning;
wenzelm [Mon, 29 Sep 1997 14:10:52 +0200] rev 3738
default margin 76 (to accomodate warning and error default output);
paulson [Mon, 29 Sep 1997 12:13:43 +0200] rev 3737
Step_tac -> Safe_tac
paulson [Mon, 29 Sep 1997 11:56:04 +0200] rev 3736
Much tidying including step_tac -> clarify_tac or safe_tac; sometimes
used qed_spec_mp
paulson [Mon, 29 Sep 1997 11:52:25 +0200] rev 3735
Step_tac -> Safe_tac
paulson [Mon, 29 Sep 1997 11:51:52 +0200] rev 3734
Much tidying including "qed" instead of result(), and even qed_spec_mp,
and Safe_tac instead of step_tac
paulson [Mon, 29 Sep 1997 11:51:09 +0200] rev 3733
Previously loaded the WRONG THEORY, ignoring Confluence...
paulson [Mon, 29 Sep 1997 11:49:33 +0200] rev 3732
Now using qed_spec_mp