Changes

Summary

option "-o" for "isabelle jedit";
eliminated unused simproc identifier;

Changeset 62914:930a30c1a9af by wenzelm: option "-o" for "isabelle jedit";
The file was modified	`src/Doc/JEdit/JEdit.thy` (diff)
The file was modified	`src/Tools/jEdit/lib/Tools/jedit` (diff)
The file was modified	`src/Tools/jEdit/src/plugin.scala` (diff)
Changeset 62913:13252110a6fe by wenzelm: eliminated unused simproc identifier;
The file was modified	`src/Doc/Isar_Ref/Generic.thy` (diff)
The file was modified	`src/HOL/Decision_Procs/langford.ML` (diff)
The file was modified	`src/HOL/HOL.thy` (diff)
The file was modified	`src/HOL/HOLCF/Tools/cont_proc.ML` (diff)
The file was modified	`src/HOL/Library/Old_SMT/old_smt_real.ML` (diff)
The file was modified	`src/HOL/Library/Old_SMT/old_z3_proof_tools.ML` (diff)
The file was modified	`src/HOL/Nominal/nominal_datatype.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/Nominal/nominal_permeq.ML` (diff)
The file was modified	`src/HOL/Product_Type.thy` (diff)
The file was modified	`src/HOL/Statespace/distinct_tree_prover.ML` (diff)
The file was modified	`src/HOL/Statespace/state_fun.ML` (diff)
The file was modified	`src/HOL/Statespace/state_space.ML` (diff)
The file was modified	`src/HOL/Tools/Quotient/quotient_tacs.ML` (diff)
The file was modified	`src/HOL/Tools/SMT/smt_real.ML` (diff)
The file was modified	`src/HOL/Tools/SMT/z3_replay_util.ML` (diff)
The file was modified	`src/HOL/Tools/groebner.ML` (diff)
The file was modified	`src/HOL/Tools/inductive_set.ML` (diff)
The file was modified	`src/HOL/Tools/int_arith.ML` (diff)
The file was modified	`src/HOL/Tools/numeral_simprocs.ML` (diff)
The file was modified	`src/HOL/Tools/record.ML` (diff)
The file was modified	`src/HOL/Word/WordBitwise.thy` (diff)
The file was modified	`src/Pure/Isar/isar_cmd.ML` (diff)
The file was modified	`src/Pure/ML/ml_context.ML` (diff)
The file was modified	`src/Pure/Pure.thy` (diff)
The file was modified	`src/Pure/raw_simplifier.ML` (diff)
The file was modified	`src/Pure/simplifier.ML` (diff)
The file was modified	`src/Tools/induct.ML` (diff)
The file was modified	`src/ZF/Datatype_ZF.thy` (diff)
The file was modified	`src/ZF/arith_data.ML` (diff)
The file was modified	`src/ZF/int_arith.ML` (diff)