isabelle: doc-src/Intro/bool.thy@e628da370072 (annotated)

more efficient Markup_Tree, based on branches sorted by quasi-order; renamed markup_node.scala to markup_tree.scala and classes/objects accordingly; Position.Range: produce actual Text.Range; Symbol.Index.decode: convert 1-based Isabelle offsets here; added static Command.range; simplified Command.markup; Document_Model.token_marker: flatten markup at most once; tuned;

105 216d6ed87399 Initial revision lcp parents: diff changeset	1	Bool = FOL +
32960 69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width; wenzelm parents: 105 diff changeset	2	types bool 0
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width; wenzelm parents: 105 diff changeset	3	arities bool :: term
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width; wenzelm parents: 105 diff changeset	4	consts tt,ff :: "bool"
105 216d6ed87399 Initial revision lcp parents: diff changeset	5	end

author	wenzelm
	Wed, 18 Aug 2010 23:44:50 +0200
changeset 38479	e628da370072
parent 32960	69916a850301
permissions	-rw-r--r--