Mercurialisabelle / changelog
summary | shortlog | changelog | graph | tags | branches | files | gz
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 +10 +30 +100 +300 +1000 tip
11 months ago wenzelm [Sun, 12 Nov 2017 19:46:19 +0100] rev 67059
tuned signature;
src/Pure/PIDE/resources.scala src/Pure/Thy/sessions.scala src/Pure/Thy/thy_resources.scala src/Tools/VSCode/src/vscode_resources.scala src/Tools/jEdit/src/document_model.scala src/Tools/jEdit/src/plugin.scala

11 months ago wenzelm [Sun, 12 Nov 2017 19:42:22 +0100] rev 67058
simplified: eliminated pointless Thy_Document_Model;
src/Pure/Thy/thy_document_model.scala src/Pure/Thy/thy_resources.scala src/Pure/build-jars

11 months ago wenzelm [Sun, 12 Nov 2017 16:56:39 +0100] rev 67057
theory nodes are never visible: avoid prints, which are not covered by node_consolidated;
src/Pure/Thy/thy_document_model.scala src/Pure/Thy/thy_resources.scala

11 months ago wenzelm [Sun, 12 Nov 2017 16:38:13 +0100] rev 67056
load theories via PIDE document update;
theory nodes are always required;
src/Pure/PIDE/resources.scala src/Pure/Thy/thy_document_model.scala src/Pure/Thy/thy_resources.scala

11 months ago wenzelm [Sun, 12 Nov 2017 13:22:00 +0100] rev 67055
tuned signature;
src/Pure/Thy/thy_document_model.scala

11 months ago wenzelm [Sun, 12 Nov 2017 13:19:00 +0100] rev 67054
PIDE resources for theory files;
src/Pure/Thy/thy_resources.scala src/Pure/build-jars

11 months ago wenzelm [Sun, 12 Nov 2017 12:55:10 +0100] rev 67053
tuned;
src/Pure/PIDE/resources.scala src/Pure/Thy/sessions.scala

11 months ago wenzelm [Sun, 12 Nov 2017 12:41:05 +0100] rev 67052
tuned signature;
src/Pure/Admin/afp.scala src/Pure/ML/ml_process.scala src/Pure/System/isabelle_process.scala src/Pure/Thy/sessions.scala src/Pure/Tools/build.scala

11 months ago haftmann [Sat, 11 Nov 2017 18:41:08 +0000] rev 67051
dedicated definition for coprimality
NEWS src/Doc/Corec/Corec.thy src/HOL/Algebra/Multiplicative_Group.thy src/HOL/Computational_Algebra/Factorial_Ring.thy src/HOL/Computational_Algebra/Normalized_Fraction.thy src/HOL/Computational_Algebra/Nth_Powers.thy src/HOL/Computational_Algebra/Polynomial_Factorial.thy src/HOL/Computational_Algebra/Primes.thy src/HOL/Computational_Algebra/Squarefree.thy src/HOL/Corec_Examples/Paper_Examples.thy src/HOL/Decision_Procs/Rat_Pair.thy src/HOL/Euclidean_Division.thy src/HOL/GCD.thy src/HOL/Isar_Examples/Fibonacci.thy src/HOL/Library/Multiset.thy src/HOL/Map.thy src/HOL/Nitpick.thy src/HOL/Number_Theory/Cong.thy src/HOL/Number_Theory/Euler_Criterion.thy src/HOL/Number_Theory/Fib.thy src/HOL/Number_Theory/Gauss.thy src/HOL/Number_Theory/Pocklington.thy src/HOL/Number_Theory/Residues.thy src/HOL/Number_Theory/Totient.thy src/HOL/Parity.thy src/HOL/Rat.thy src/HOL/Real.thy src/HOL/Rings.thy src/HOL/Set.thy

11 months ago haftmann [Sat, 11 Nov 2017 18:33:35 +0000] rev 67050
more induct rules on nat
src/HOL/Nat.thy

(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 +10 +30 +100 +300 +1000 tip
isabelle