Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. HTML preview via builtin HTTP server;
  2. permissive output of XML.Text, e.g. relevant for embedded <style>;
  3. avoid Local_Theory.reset in application space
  4. tuned
  5. specific output setup is not supposed to intrude regular import theory
  6. avoid duplicate
  7. streamlined code setup for fake terms
  8. modernized (code) setup for enumeration predicates
  9. simplified setup
  10. executable domain membership checks
  11. more tests;
  12. cover more history;
  13. cover more history;
  14. uniform notion of Symbol.is_controllable (see also 265d9300d523);
Changeset 66019:69b5ef78fb07 by wenzelm:
HTML preview via builtin HTTP server;
The file was modified NEWS (diff)
The file was modified src/Tools/jEdit/src/actions.xml (diff)
The file was modified src/Tools/jEdit/src/document_model.scala (diff)
The file was modified src/Tools/jEdit/src/plugin.scala (diff)
Changeset 66018:9ce3720976dc by wenzelm:
permissive output of XML.Text, e.g. relevant for embedded &lt;style&gt;;
The file was modified src/Pure/Thy/html.scala (diff)
Changeset 66017:57acac0fd29b by haftmann:
avoid Local_Theory.reset in application space
The file was modified src/HOL/Tools/Lifting/lifting_def.ML (diff)
The file was modified src/HOL/Tools/Lifting/lifting_def_code_dt.ML (diff)
Changeset 66016:39d9a59d8d94 by haftmann:
tuned
The file was modified src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy (diff)
Changeset 66015:70643edecb7a by haftmann:
specific output setup is not supposed to intrude regular import theory
The file was modified src/HOL/Library/Library.thy (diff)
The file was modified src/HOL/ROOT (diff)
Changeset 66014:2f45f4abf0a9 by haftmann:
avoid duplicate
The file was modified src/HOL/Codegenerator_Test/Candidates.thy (diff)
The file was modified src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy (diff)
Changeset 66013:03002d10bf1d by haftmann:
streamlined code setup for fake terms
The file was modified src/HOL/Code_Evaluation.thy (diff)
Changeset 66012:59bf29d2b3a1 by haftmann:
modernized (code) setup for enumeration predicates
The file was modified src/HOL/Predicate.thy (diff)
The file was modified src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML (diff)
The file was modified src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML (diff)
Changeset 66011:f10bbfe07c41 by haftmann:
simplified setup
The file was modified src/HOL/Nitpick.thy (diff)
Changeset 66010:2f7d39285a1a by haftmann:
executable domain membership checks
The file was modified src/HOL/Map.thy (diff)
Changeset 66009:4fe8e0b2590a by wenzelm:
more tests;
The file was modified src/Pure/Admin/isabelle_cronjob.scala (diff)
Changeset 66008:010698325e36 by wenzelm:
cover more history;
The file was modified src/Pure/Admin/isabelle_cronjob.scala (diff)
Changeset 66007:6706d6f0afda by wenzelm:
cover more history;
The file was modified src/Pure/Admin/isabelle_cronjob.scala (diff)
Changeset 66006:cec184536dfd by wenzelm:
uniform notion of Symbol.is_controllable (see also 265d9300d523);
The file was modified src/Pure/General/symbol.scala (diff)
The file was modified src/Pure/Thy/html.scala (diff)
The file was modified src/Tools/jEdit/src/syntax_style.scala (diff)