Skip to content
Jenkins
log in
Dashboard
Benedikt Seidl <benedikt.seidl@tum.de>
My Views
All
isabelle-repo
#146
Changes
Status
Changes
Console Output
View Build Information
Polling Log
Environment Variables
Mercurial Build Data
Embeddable Build Status
Previous Build
Next Build
Success
Changes
Summary
merged
eliminated "xname" and variants;
clarified syntax;
more completions, independently on accidental external form (e.g. "Map.empty" with its redundant prefix);
tuned;
clarified syntax;
avoid quotes for qualified names;
Changeset
62970:f78cf782bd33
by
wenzelm
:
merged
Changeset
62969:9f394a16c557
by
wenzelm
:
eliminated "xname" and variants;
The file was modified
NEWS
(diff)
The file was modified
src/Doc/Datatypes/Datatypes.thy
(diff)
The file was modified
src/Doc/Eisbach/Manual.thy
(diff)
The file was modified
src/Doc/Implementation/Isar.thy
(diff)
The file was modified
src/Doc/Implementation/Logic.thy
(diff)
The file was modified
src/Doc/Implementation/ML.thy
(diff)
The file was modified
src/Doc/Implementation/Prelim.thy
(diff)
The file was modified
src/Doc/Isar_Ref/Document_Preparation.thy
(diff)
The file was modified
src/Doc/Isar_Ref/Generic.thy
(diff)
The file was modified
src/Doc/Isar_Ref/HOL_Specific.thy
(diff)
The file was modified
src/Doc/Isar_Ref/Inner_Syntax.thy
(diff)
The file was modified
src/Doc/Isar_Ref/Outer_Syntax.thy
(diff)
The file was modified
src/Doc/Isar_Ref/Proof.thy
(diff)
The file was modified
src/Doc/Isar_Ref/Proof_Script.thy
(diff)
The file was modified
src/Doc/Isar_Ref/Spec.thy
(diff)
The file was modified
src/Doc/JEdit/JEdit.thy
(diff)
The file was modified
src/Doc/Logics_ZF/ZF_Isar.thy
(diff)
The file was modified
src/HOL/Decision_Procs/approximation.ML
(diff)
The file was modified
src/HOL/Library/rewrite.ML
(diff)
The file was modified
src/HOL/Library/simps_case_conv.ML
(diff)
The file was modified
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
(diff)
The file was modified
src/HOL/Nominal/nominal_inductive.ML
(diff)
The file was modified
src/HOL/Nominal/nominal_inductive2.ML
(diff)
The file was modified
src/HOL/SPARK/Manual/Reference.thy
(diff)
The file was modified
src/HOL/SPARK/Tools/spark_commands.ML
(diff)
The file was modified
src/HOL/Statespace/state_space.ML
(diff)
The file was modified
src/HOL/Tools/BNF/bnf_lift.ML
(diff)
The file was modified
src/HOL/Tools/Function/partial_function.ML
(diff)
The file was modified
src/HOL/Tools/Lifting/lifting_def_code_dt.ML
(diff)
The file was modified
src/HOL/Tools/Lifting/lifting_setup.ML
(diff)
The file was modified
src/HOL/Tools/Predicate_Compile/code_prolog.ML
(diff)
The file was modified
src/HOL/Tools/Predicate_Compile/predicate_compile.ML
(diff)
The file was modified
src/HOL/Tools/Quotient/quotient_type.ML
(diff)
The file was modified
src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
(diff)
The file was modified
src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
(diff)
The file was modified
src/HOL/Tools/inductive.ML
(diff)
The file was modified
src/HOL/Tools/record.ML
(diff)
The file was modified
src/HOL/Tools/try0.ML
(diff)
The file was modified
src/HOL/Tools/value.ML
(diff)
The file was modified
src/Pure/General/completion.scala
(diff)
The file was modified
src/Pure/Isar/method.ML
(diff)
The file was modified
src/Pure/Isar/parse.ML
(diff)
The file was modified
src/Pure/Isar/parse.scala
(diff)
The file was modified
src/Pure/Isar/parse_spec.ML
(diff)
The file was modified
src/Pure/Isar/token.ML
(diff)
The file was modified
src/Pure/Isar/token.scala
(diff)
The file was modified
src/Pure/ML/ml_context.ML
(diff)
The file was modified
src/Pure/PIDE/command.scala
(diff)
The file was modified
src/Pure/Pure.thy
(diff)
The file was modified
src/Pure/Thy/sessions.scala
(diff)
The file was modified
src/Pure/Thy/term_style.ML
(diff)
The file was modified
src/Pure/Thy/thy_header.ML
(diff)
The file was modified
src/Pure/Thy/thy_header.scala
(diff)
The file was modified
src/Pure/Thy/thy_output.ML
(diff)
The file was modified
src/Pure/Tools/find_consts.ML
(diff)
The file was modified
src/Pure/Tools/find_theorems.ML
(diff)
The file was modified
src/Tools/Code/code_target.ML
(diff)
The file was modified
src/ZF/Tools/datatype_package.ML
(diff)
The file was modified
src/ZF/Tools/induct_tacs.ML
(diff)
The file was modified
src/ZF/Tools/inductive_package.ML
(diff)
Changeset
62968:4e4738698db4
by
wenzelm
:
clarified syntax;
The file was modified
src/Pure/System/options.scala
(diff)
The file was modified
src/Pure/Thy/sessions.scala
(diff)
Changeset
62967:5e8b1aead28f
by
wenzelm
:
more completions, independently on accidental external form (e.g. "Map.empty" with its redundant prefix);
The file was modified
src/Pure/General/name_space.ML
(diff)
Changeset
62966:771b8ad5c7fc
by
wenzelm
:
tuned;
The file was modified
src/Tools/Code/code_ml.ML
(diff)
Changeset
62965:5bf08c9aa036
by
wenzelm
:
clarified syntax;
The file was modified
src/Doc/Isar_Ref/Document_Preparation.thy
(diff)
The file was modified
src/Doc/Isar_Ref/Spec.thy
(diff)
The file was modified
src/Pure/Isar/parse.ML
(diff)
The file was modified
src/Pure/Isar/parse.scala
(diff)
The file was modified
src/Pure/PIDE/command.scala
(diff)
Changeset
62964:d0c1b2dbca5b
by
wenzelm
:
avoid quotes for qualified names;
The file was modified
src/Pure/General/completion.scala
(diff)