tuned comments
authorwenzelm
Sun Jan 21 16:43:47 2007 +0100 (2007-01-21)
changeset 221483b99944136ef
parent 22147 f4ed4d940d44
child 22149 7a8c2a556d28
tuned comments
etc/settings
src/HOL/ex/Binary.thy
src/Pure/Thy/thy_info.ML
src/Pure/context.ML
     1.1 --- a/etc/settings	Sun Jan 21 16:43:46 2007 +0100
     1.2 +++ b/etc/settings	Sun Jan 21 16:43:47 2007 +0100
     1.3 @@ -62,6 +62,12 @@
     1.4  #ML_SUFFIX=".psv"
     1.5  #ML_PLATFORM=""
     1.6  
     1.7 +# Alice 1.3 (experimental!)
     1.8 +#ML_SYSTEM=alice
     1.9 +#ML_HOME="/usr/local/alice/bin"
    1.10 +#ML_OPTIONS=""
    1.11 +#ML_PLATFORM=""
    1.12 +
    1.13  
    1.14  ###
    1.15  ### Compilation options (cf. isatool usedir)
     2.1 --- a/src/HOL/ex/Binary.thy	Sun Jan 21 16:43:46 2007 +0100
     2.2 +++ b/src/HOL/ex/Binary.thy	Sun Jan 21 16:43:47 2007 +0100
     2.3 @@ -127,7 +127,7 @@
     2.4    val plus = nat_op "HOL.plus";
     2.5    val mult = nat_op "HOL.times";
     2.6  
     2.7 -  fun prove ctxt prop =  (* FIXME avoid re-certification *)
     2.8 +  fun prove ctxt prop =
     2.9      Goal.prove ctxt [] [] prop (fn _ => ALLGOALS (full_simp_tac binary_ss));
    2.10  
    2.11  
     3.1 --- a/src/Pure/Thy/thy_info.ML	Sun Jan 21 16:43:46 2007 +0100
     3.2 +++ b/src/Pure/Thy/thy_info.ML	Sun Jan 21 16:43:47 2007 +0100
     3.3 @@ -205,7 +205,7 @@
     3.4  val _ = ML_Context.value_antiq "theory"
     3.5    (Scan.lift Args.name
     3.6      >> (fn name => (name ^ "_thy", "ThyInfo.theory " ^ ML_Syntax.print_string name))
     3.7 -  || Scan.succeed ("thy", "ML_Context.the_context_finished ()"));
     3.8 +  || Scan.succeed ("thy", "ML_Context.the_context ()"));
     3.9  
    3.10  
    3.11  
     4.1 --- a/src/Pure/context.ML	Sun Jan 21 16:43:46 2007 +0100
     4.2 +++ b/src/Pure/context.ML	Sun Jan 21 16:43:47 2007 +0100
     4.3 @@ -44,7 +44,6 @@
     4.4    val copy_thy: theory -> theory
     4.5    val checkpoint_thy: theory -> theory
     4.6    val finish_thy: theory -> theory
     4.7 -  val is_finished_thy: theory -> bool
     4.8    val theory_data_of: theory -> string list
     4.9    val pre_pure_thy: theory
    4.10    val begin_thy: (theory -> Pretty.pp) -> string -> theory list -> theory
    4.11 @@ -406,9 +405,6 @@
    4.12      val _ = List.app (fn r => r := thy'') rs;
    4.13    in thy'' end;
    4.14  
    4.15 -fun is_finished_thy thy =
    4.16 -  (check_thy thy; not (is_draft thy) andalso #version (history_of thy) = 0);
    4.17 -
    4.18  
    4.19  (* theory data *)
    4.20